diff --git a/src/solvers/sat/satcheck_minisat2.cpp b/src/solvers/sat/satcheck_minisat2.cpp
index 3f50091bbb6..43e41ce163d 100644
--- a/src/solvers/sat/satcheck_minisat2.cpp
+++ b/src/solvers/sat/satcheck_minisat2.cpp
@@ -81,6 +81,18 @@ void satcheck_minisat2_baset<T>::set_polarity(literalt a, bool value)
   }
 }
 
+template<typename T>
+void satcheck_minisat2_baset<T>::interrupt()
+{
+  solver->interrupt();
+}
+
+template<typename T>
+void satcheck_minisat2_baset<T>::clear_interrupt()
+{
+  solver->clearInterrupt();
+}
+
 const std::string satcheck_minisat_no_simplifiert::solver_text()
 {
   return "MiniSAT 2.2.1 without simplifier";
diff --git a/src/solvers/sat/satcheck_minisat2.h b/src/solvers/sat/satcheck_minisat2.h
index cda5ab21bac..9834cdb11f8 100644
--- a/src/solvers/sat/satcheck_minisat2.h
+++ b/src/solvers/sat/satcheck_minisat2.h
@@ -42,6 +42,12 @@ class satcheck_minisat2_baset:public cnf_solvert
   // extra MiniSat feature: default branching decision
   void set_polarity(literalt a, bool value);
 
+  // extra MiniSat feature: interrupt running SAT query
+  void interrupt();
+
+  // extra MiniSat feature: permit previously interrupted SAT query to continue
+  void clear_interrupt();
+
   virtual bool is_in_conflict(literalt a) const override;
   virtual bool has_set_assumptions() const final { return true; }
   virtual bool has_is_in_conflict() const final { return true; }