fixing the problems with the bvminisat. there was a case when things would get bitblasted, it would restart to add the clauses, and loose propagation information.

1 files changed, 3 insertions, 1 deletions

diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 79e54cac2..102f8051b 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -95,7 +95,7 @@ public:
      * Notify about a learnt clause.
      */
     virtual void notify(SatClause& clause) = 0;
-};
+  };
 
   virtual void setNotify(Notify* notify) = 0; 
   
@@ -105,6 +105,8 @@ public:
 
   virtual void addMarkerLiteral(SatLiteral lit) = 0; 
 
+  virtual SatValue propagate() = 0;
+
   virtual void explain(SatLiteral lit, std::vector<SatLiteral>& explanation) = 0;
 
   virtual SatValue assertAssumption(SatLiteral lit, bool propagate = false) = 0;