From 83722fdc9072c8bee19c2123176d77bef50bbe0d Mon Sep 17 00:00:00 2001
From: Liana Hadarean <lianahady@gmail.com>
Date: Wed, 3 Oct 2012 19:41:45 +0000
Subject: added support for interrupting TheoryBV

---
 src/prop/sat_solver.h | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'src/prop/sat_solver.h')

diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index a4fdd5b3a..7e3af69cf 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -94,6 +94,8 @@ public:
      * Notify about a learnt clause.
      */
     virtual void notify(SatClause& clause) = 0;
+    virtual void safePoint() = 0;
+    
   };/* class BVSatSolverInterface::Notify */
 
   virtual void setNotify(Notify* notify) = 0;
-- 
cgit v1.2.3