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, 4 insertions, 0 deletions

diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index 4868db6f5..032788806 100644
--- a/src/prop/bvminisat/bvminisat.cpp
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -55,6 +55,10 @@ void BVMinisatSatSolver::addClause(SatClause& clause, bool removable) {
   d_minisat->addClause(minisat_clause);
 }
 
+SatValue BVMinisatSatSolver::propagate() {
+  return toSatLiteralValue(d_minisat->propagateAssumptions());
+}
+
 void BVMinisatSatSolver::addMarkerLiteral(SatLiteral lit) {
   d_minisat->addMarkerLiteral(BVMinisat::var(toMinisatLit(lit)));
 }