added support for interrupting TheoryBV

2 files changed, 5 insertions, 0 deletions

diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp
index 2c45fb603..3beb7c229 100644
--- a/src/theory/bv/bitblaster.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@ -356,6 +356,10 @@ void Bitblaster::MinisatNotify::notify(prop::SatClause& clause) {
   }
 };
 
+void Bitblaster::MinisatNotify::safePoint() {
+  d_bv->d_out->safePoint(); 
+}
+
 EqualityStatus Bitblaster::getEqualityStatus(TNode a, TNode b) {
 
   // We don't want to bit-blast every possibly expensive term for the sake of equality checking
diff --git a/src/theory/bv/bitblaster.h b/src/theory/bv/bitblaster.h
index 2ff12bbdf..ada9802bd 100644
--- a/src/theory/bv/bitblaster.h
+++ b/src/theory/bv/bitblaster.h
@@ -78,6 +78,7 @@ class Bitblaster {
     {}
     bool notify(prop::SatLiteral lit);
     void notify(prop::SatClause& clause);
+    void safePoint();
   };
   
   typedef __gnu_cxx::hash_map <Node, Bits, TNodeHashFunction >              TermDefMap;