1 files changed, 28 insertions, 17 deletions

diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index fa5f53113..46b521e6b 100644
--- a/src/prop/bvminisat/bvminisat.cpp
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -22,14 +22,15 @@
 using namespace CVC4;
 using namespace prop;
 
-BVMinisatSatSolver::BVMinisatSatSolver(context::Context* mainSatContext)
+BVMinisatSatSolver::BVMinisatSatSolver(context::Context* mainSatContext, const std::string& name)
 : context::ContextNotifyObj(mainSatContext, false),
   d_minisat(new BVMinisat::SimpSolver(mainSatContext)),
   d_minisatNotify(0),
   d_solveCount(0),
   d_assertionsCount(0),
   d_assertionsRealCount(mainSatContext, 0),
-  d_lastPropagation(mainSatContext, 0)
+  d_lastPropagation(mainSatContext, 0),
+  d_statistics(name)
 {
   d_statistics.init(d_minisat); 
 }
@@ -61,6 +62,7 @@ SatValue BVMinisatSatSolver::propagate() {
 
 void BVMinisatSatSolver::addMarkerLiteral(SatLiteral lit) {
   d_minisat->addMarkerLiteral(BVMinisat::var(toMinisatLit(lit)));
+  markUnremovable(lit); 
 }
 
 void BVMinisatSatSolver::explain(SatLiteral lit, std::vector<SatLiteral>& explanation) {
@@ -113,9 +115,9 @@ SatValue BVMinisatSatSolver::solve(long unsigned int& resource){
   } else {
     d_minisat->setConfBudget(resource);
   }
-  BVMinisat::vec<BVMinisat::Lit> empty;
+  //  BVMinisat::vec<BVMinisat::Lit> empty;
   unsigned long conflictsBefore = d_minisat->conflicts;
-  SatValue result = toSatLiteralValue(d_minisat->solveLimited(empty));
+  SatValue result = toSatLiteralValue(d_minisat->solveLimited());
   d_minisat->clearInterrupt();
   resource = d_minisat->conflicts - conflictsBefore;
   Trace("limit") << "<MinisatSatSolver::solve(): it took " << resource << " conflicts" << std::endl;
@@ -211,20 +213,24 @@ void BVMinisatSatSolver::toSatClause(BVMinisat::vec<BVMinisat::Lit>& clause,
 
 // Satistics for BVMinisatSatSolver
 
-BVMinisatSatSolver::Statistics::Statistics() :
-  d_statStarts("theory::bv::bvminisat::starts"),
-  d_statDecisions("theory::bv::bvminisat::decisions"),
-  d_statRndDecisions("theory::bv::bvminisat::rnd_decisions"),
-  d_statPropagations("theory::bv::bvminisat::propagations"),
-  d_statConflicts("theory::bv::bvminisat::conflicts"),
-  d_statClausesLiterals("theory::bv::bvminisat::clauses_literals"),
-  d_statLearntsLiterals("theory::bv::bvminisat::learnts_literals"),
-  d_statMaxLiterals("theory::bv::bvminisat::max_literals"),
-  d_statTotLiterals("theory::bv::bvminisat::tot_literals"),
-  d_statEliminatedVars("theory::bv::bvminisat::eliminated_vars"),
-  d_statCallsToSolve("theory::bv::bvminisat::calls_to_solve", 0),
-  d_statSolveTime("theory::bv::bvminisat::solve_time", 0)
+BVMinisatSatSolver::Statistics::Statistics(const std::string& prefix) :
+  d_statStarts("theory::bv::"+prefix+"bvminisat::starts"),
+  d_statDecisions("theory::bv::"+prefix+"bvminisat::decisions"),
+  d_statRndDecisions("theory::bv::"+prefix+"bvminisat::rnd_decisions"),
+  d_statPropagations("theory::bv::"+prefix+"bvminisat::propagations"),
+  d_statConflicts("theory::bv::"+prefix+"bvminisat::conflicts"),
+  d_statClausesLiterals("theory::bv::"+prefix+"bvminisat::clauses_literals"),
+  d_statLearntsLiterals("theory::bv::"+prefix+"bvminisat::learnts_literals"),
+  d_statMaxLiterals("theory::bv::"+prefix+"bvminisat::max_literals"),
+  d_statTotLiterals("theory::bv::"+prefix+"bvminisat::tot_literals"),
+  d_statEliminatedVars("theory::bv::"+prefix+"bvminisat::eliminated_vars"),
+  d_statCallsToSolve("theory::bv::"+prefix+"bvminisat::calls_to_solve", 0),
+  d_statSolveTime("theory::bv::"+prefix+"bvminisat::solve_time", 0),
+  d_registerStats(!prefix.empty())
 {
+  if (!d_registerStats)
+    return;
+
   StatisticsRegistry::registerStat(&d_statStarts);
   StatisticsRegistry::registerStat(&d_statDecisions);
   StatisticsRegistry::registerStat(&d_statRndDecisions);
@@ -240,6 +246,8 @@ BVMinisatSatSolver::Statistics::Statistics() :
 }
 
 BVMinisatSatSolver::Statistics::~Statistics() {
+  if (!d_registerStats)
+    return;
   StatisticsRegistry::unregisterStat(&d_statStarts);
   StatisticsRegistry::unregisterStat(&d_statDecisions);
   StatisticsRegistry::unregisterStat(&d_statRndDecisions);
@@ -255,6 +263,9 @@ BVMinisatSatSolver::Statistics::~Statistics() {
 }
 
 void BVMinisatSatSolver::Statistics::init(BVMinisat::SimpSolver* minisat){
+  if (!d_registerStats)
+    return;
+  
   d_statStarts.setData(minisat->starts);
   d_statDecisions.setData(minisat->decisions);
   d_statRndDecisions.setData(minisat->rnd_decisions);