Merging CAV14 paper bit-vector work.

9 files changed, 150 insertions, 70 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);
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index ebf4a44b4..568d89f7f 100644
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -69,9 +69,10 @@ public:
   BVMinisatSatSolver() :
     ContextNotifyObj(NULL, false),
     d_assertionsRealCount(NULL, (unsigned)0),
-    d_lastPropagation(NULL, (unsigned)0)
+    d_lastPropagation(NULL, (unsigned)0),
+    d_statistics("")
   { Unreachable(); }
-  BVMinisatSatSolver(context::Context* mainSatContext);
+  BVMinisatSatSolver(context::Context* mainSatContext, const std::string& name = "");
   ~BVMinisatSatSolver() throw(AssertionException);
 
   void setNotify(Notify* notify);
@@ -91,7 +92,6 @@ public:
   
   SatValue solve();
   SatValue solve(long unsigned int&);
-  SatValue solve(bool quick_solve);
   void getUnsatCore(SatClause& unsatCore);
 
   SatValue value(SatLiteral l);
@@ -129,8 +129,9 @@ public:
     ReferenceStat<uint64_t> d_statTotLiterals;
     ReferenceStat<int> d_statEliminatedVars;
     IntStat d_statCallsToSolve;
-    BackedStat<double> d_statSolveTime; 
-    Statistics();
+    BackedStat<double> d_statSolveTime;
+    bool d_registerStats;
+    Statistics(const std::string& prefix);
     ~Statistics();
     void init(BVMinisat::SimpSolver* minisat);
   };
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index 68969c78b..8833eec78 100644
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -59,19 +59,31 @@ std::ostream& operator << (std::ostream& out, const BVMinisat::Clause& c) {
 
 static const char* _cat = "CORE";
 
+// static DoubleOption  opt_var_decay         (_cat, "var-decay",   "The variable activity decay factor",            0.95,     DoubleRange(0, false, 1, false));
+// static DoubleOption  opt_clause_decay      (_cat, "cla-decay",   "The clause activity decay factor",              0.999,    DoubleRange(0, false, 1, false));
+// static DoubleOption  opt_random_var_freq   (_cat, "rnd-freq",    "The frequency with which the decision heuristic tries to choose a random variable", 0.0, DoubleRange(0, true, 1, true));
+// static DoubleOption  opt_random_seed       (_cat, "rnd-seed",    "Used by the random variable selection",         91648253, DoubleRange(0, false, HUGE_VAL, false));
+// static IntOption     opt_ccmin_mode        (_cat, "ccmin-mode",  "Controls conflict clause minimization (0=none, 1=basic, 2=deep)", 0, IntRange(0, 2));
+// static IntOption     opt_phase_saving      (_cat, "phase-saving", "Controls the level of phase saving (0=none, 1=limited, 2=full)", 2, IntRange(0, 2));
+// static BoolOption    opt_rnd_init_act      (_cat, "rnd-init",    "Randomize the initial activity", false);
+// static BoolOption    opt_luby_restart      (_cat, "luby",        "Use the Luby restart sequence", true);
+// static IntOption     opt_restart_first     (_cat, "rfirst",      "The base restart interval", 100, IntRange(1, INT32_MAX)); 
+// static DoubleOption  opt_restart_inc       (_cat, "rinc",        "Restart interval increase factor", 1.5, DoubleRange(1, false, HUGE_VAL, false));
+// static DoubleOption  opt_garbage_frac      (_cat, "gc-frac",     "The fraction of wasted memory allowed before a garbage collection is triggered",  0.20, DoubleRange(0, false, HUGE_VAL, false));
+
+
 static DoubleOption  opt_var_decay         (_cat, "var-decay",   "The variable activity decay factor",            0.95,     DoubleRange(0, false, 1, false));
 static DoubleOption  opt_clause_decay      (_cat, "cla-decay",   "The clause activity decay factor",              0.999,    DoubleRange(0, false, 1, false));
-static DoubleOption  opt_random_var_freq   (_cat, "rnd-freq",    "The frequency with which the decision heuristic tries to choose a random variable", 0.0, DoubleRange(0, true, 1, true));
+static DoubleOption  opt_random_var_freq   (_cat, "rnd-freq",    "The frequency with which the decision heuristic tries to choose a random variable", 0, DoubleRange(0, true, 1, true));
 static DoubleOption  opt_random_seed       (_cat, "rnd-seed",    "Used by the random variable selection",         91648253, DoubleRange(0, false, HUGE_VAL, false));
-static IntOption     opt_ccmin_mode        (_cat, "ccmin-mode",  "Controls conflict clause minimization (0=none, 1=basic, 2=deep)", 0, IntRange(0, 2));
+static IntOption     opt_ccmin_mode        (_cat, "ccmin-mode",  "Controls conflict clause minimization (0=none, 1=basic, 2=deep)", 2, IntRange(0, 2));
 static IntOption     opt_phase_saving      (_cat, "phase-saving", "Controls the level of phase saving (0=none, 1=limited, 2=full)", 2, IntRange(0, 2));
 static BoolOption    opt_rnd_init_act      (_cat, "rnd-init",    "Randomize the initial activity", false);
 static BoolOption    opt_luby_restart      (_cat, "luby",        "Use the Luby restart sequence", true);
-static IntOption     opt_restart_first     (_cat, "rfirst",      "The base restart interval", 100, IntRange(1, INT32_MAX));
-static DoubleOption  opt_restart_inc       (_cat, "rinc",        "Restart interval increase factor", 1.5, DoubleRange(1, false, HUGE_VAL, false));
+static IntOption     opt_restart_first     (_cat, "rfirst",      "The base restart interval", 25, IntRange(1, INT32_MAX));
+static DoubleOption  opt_restart_inc       (_cat, "rinc",        "Restart interval increase factor", 3, DoubleRange(1, false, HUGE_VAL, false));
 static DoubleOption  opt_garbage_frac      (_cat, "gc-frac",     "The fraction of wasted memory allowed before a garbage collection is triggered",  0.20, DoubleRange(0, false, HUGE_VAL, false));
 
-
 //=================================================================================================
 // Constructor/Destructor:
 
@@ -395,10 +407,8 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip
     out_learnt.shrink(i - j);
     tot_literals += out_learnt.size();
 
-    bool clause_all_marker = true;
     for (int i = 0; i < out_learnt.size(); ++ i) {
       if (marker[var(out_learnt[i])] == 0) {
-        clause_all_marker = false;
         break;
       }
     }
@@ -410,9 +420,6 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip
     }
     else{
         int max_i = 1;
-        if (marker[var(out_learnt[0])] == 0) {
-          clause_all_marker = false;
-        }
         // Find the first literal assigned at the next-highest level:
         for (int i = 2; i < out_learnt.size(); i++)
             if (level(var(out_learnt[i])) > level(var(out_learnt[max_i])))
@@ -424,10 +431,6 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip
         out_btlevel       = level(var(p));
     }
 
-    if (out_learnt.size() > 0 && clause_all_marker && CVC4::options::bitvectorShareLemmas()) {
-      notify->notify(out_learnt);
-    }
-
     for (int j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0;    // ('seen[]' is now cleared)
 }
 
@@ -462,6 +465,48 @@ bool Solver::litRedundant(Lit p, uint32_t abstract_levels)
     return true;
 }
 
+/** 
+ * Specialized analyzeFinal procedure where we test the consistency
+ * of the assumptions before backtracking bellow the assumption level.
+ * 
+ * @param p the original uip (may be unit)
+ * @param confl_clause the conflict clause
+ * @param out_conflict the conflict in terms of assumptions we are building
+ */
+void Solver::analyzeFinal2(Lit p, CRef confl_clause, vec<Lit>& out_conflict) {
+  assert (confl_clause != CRef_Undef);
+  assert (decisionLevel() == assumptions.size());
+  assert (level(var(p)) == assumptions.size());
+
+  out_conflict.clear(); 
+  
+  Clause& cl = ca[confl_clause];
+  for (int i = 0; i < cl.size(); ++i) {
+    seen[var(cl[i])] = 1;
+  }
+
+  for (int i = trail.size() - 1; i >= trail_lim[0]; i--) {
+    Var x = var(trail[i]);
+    if (seen[x]) {
+      if (reason(x) == CRef_Undef) {
+        // this is the case when p was a unit
+        if (x == var(p))
+          continue;
+        
+        assert (marker[x] == 2);
+        assert (level(x) > 0);
+        out_conflict.push(~trail[i]); 
+      } else {
+        Clause& c = ca[reason(x)];
+        for (int j = 1; j < c.size(); j++)
+          if (level(var(c[j])) > 0)
+            seen[var(c[j])] = 1;
+      }
+      seen[x] = 0;
+    }
+  }
+  assert (out_conflict.size()); 
+}
 
 /*_________________________________________________________________________________________________
 |
@@ -475,7 +520,9 @@ bool Solver::litRedundant(Lit p, uint32_t abstract_levels)
 void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict)
 {
     out_conflict.clear();
-    out_conflict.push(p);
+    if (marker[var(p)] == 2) {
+      out_conflict.push(p);
+    }
 
     if (decisionLevel() == 0)
         return;
@@ -500,6 +547,7 @@ void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict)
     }
 
     seen[var(p)] = 0;
+    assert (out_conflict.size());
 }
 
 
@@ -755,28 +803,46 @@ lbool Solver::search(int nof_conflicts, UIP uip)
             analyze(confl, learnt_clause, backtrack_level, uip);
 
             Lit p = learnt_clause[0];
-            bool assumption = marker[var(p)] == 2;
-
-            cancelUntil(backtrack_level);
-
-            if (learnt_clause.size() == 1){
-                uncheckedEnqueue(p);
-            }else{
-                CRef cr = ca.alloc(learnt_clause, true);
-                learnts.push(cr);
-                attachClause(cr);
-                claBumpActivity(ca[cr]);
-                uncheckedEnqueue(p, cr);
+            //bool assumption = marker[var(p)] == 2;
+
+            CRef cr = CRef_Undef;
+            if (learnt_clause.size() > 1) {
+              cr = ca.alloc(learnt_clause, true);
+              learnts.push(cr);
+              attachClause(cr);
+              claBumpActivity(ca[cr]);
             }
 
-            // if an assumption, we're done
-            if (assumption) {
-              assert(decisionLevel() < assumptions.size());
+            //  if the uip was an assumption we are unsat
+            if (level(var(p)) <= assumptions.size()) {
+              for (int i = 0; i < learnt_clause.size(); ++i) {
+                assert (level(var(learnt_clause[i])) <= decisionLevel()); 
+                seen[var(learnt_clause[i])] = 1;
+              }
               analyzeFinal(p, conflict);
               Debug("bvminisat::search") << OUTPUT_TAG << " conflict on assumptions " << std::endl;
               return l_False;
             }
-            
+
+            if (!CVC4::options::bvEagerExplanations()) {
+              // check if uip leads to a conflict 
+              if (backtrack_level < assumptions.size()) {
+                cancelUntil(assumptions.size());
+                uncheckedEnqueue(p, cr);
+              
+                CRef new_confl = propagate();
+                if (new_confl != CRef_Undef) {
+                  // we have a conflict we now need to explain it
+                  analyzeFinal2(p, new_confl, conflict); 
+                  return l_False;
+                }
+              }
+            }
+
+            cancelUntil(backtrack_level);
+            uncheckedEnqueue(p, cr);
+    
+         
             varDecayActivity();
             claDecayActivity();
 
@@ -835,6 +901,7 @@ lbool Solver::search(int nof_conflicts, UIP uip)
                     // Dummy decision level:
                     newDecisionLevel();
                 }else if (value(p) == l_False){
+                    marker[var(p)] = 2;
                     analyzeFinal(~p, conflict);
                     Debug("bvminisat::search") << OUTPUT_TAG << " assumption false, we're unsat" << std::endl;
                     return l_False;
diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h
index 53d92ac39..882f23ef7 100644
--- a/src/prop/bvminisat/core/Solver.h
+++ b/src/prop/bvminisat/core/Solver.h
@@ -290,6 +290,7 @@ protected:
 
     void     analyze          (CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip = UIP_FIRST);    // (bt = backtrack)
     void     analyzeFinal     (Lit p, vec<Lit>& out_conflict);                         // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION?
+    void     analyzeFinal2(Lit p, CRef confl_clause, vec<Lit>& out_conflict);
     bool     litRedundant     (Lit p, uint32_t abstract_levels);                       // (helper method for 'analyze()')
     lbool    search           (int nof_conflicts, UIP uip = UIP_FIRST);                // Search for a given number of conflicts.
     lbool    solve_           ();                                                      // Main solve method (assumptions given in 'assumptions').
diff --git a/src/prop/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc
index 59820e9e3..c65189985 100644
--- a/src/prop/bvminisat/simp/SimpSolver.cc
+++ b/src/prop/bvminisat/simp/SimpSolver.cc
@@ -21,7 +21,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "mtl/Sort.h"
 #include "simp/SimpSolver.h"
 #include "utils/System.h"
-
+#include "theory/bv/options.h"
+#include "smt/options.h"
 using namespace BVMinisat;
 
 //=================================================================================================
@@ -32,7 +33,7 @@ static const char* _cat = "SIMP";
 
 static BoolOption   opt_use_asymm        (_cat, "asymm",        "Shrink clauses by asymmetric branching.", false);
 static BoolOption   opt_use_rcheck       (_cat, "rcheck",       "Check if a clause is already implied. (costly)", false);
-static BoolOption   opt_use_elim         (_cat, "elim",         "Perform variable elimination.", false);
+static BoolOption   opt_use_elim         (_cat, "elim",         "Perform variable elimination.", true);
 static IntOption    opt_grow             (_cat, "grow",         "Allow a variable elimination step to grow by a number of clauses.", 0);
 static IntOption    opt_clause_lim       (_cat, "cl-lim",       "Variables are not eliminated if it produces a resolvent with a length above this limit. -1 means no limit", 20,   IntRange(-1, INT32_MAX));
 static IntOption    opt_subsumption_lim  (_cat, "sub-lim",      "Do not check if subsumption against a clause larger than this. -1 means no limit.", 1000, IntRange(-1, INT32_MAX));
@@ -51,11 +52,12 @@ SimpSolver::SimpSolver(CVC4::context::Context* c) :
   , simp_garbage_frac  (opt_simp_garbage_frac)
   , use_asymm          (opt_use_asymm)
   , use_rcheck         (opt_use_rcheck)
-  , use_elim           (opt_use_elim)
+  , use_elim           (opt_use_elim &&
+                        CVC4::options::bitblastMode() == CVC4::theory::bv::BITBLAST_MODE_EAGER &&
+                        !CVC4::options::produceModels())
   , merges             (0)
   , asymm_lits         (0)
   , eliminated_vars    (0)
-  , total_eliminate_time("theory::bv::bvminisat::TotalVariableEliminationTime")
   , elimorder          (1)
   , use_simplification (true)
   , occurs             (ClauseDeleted(ca))
@@ -63,7 +65,7 @@ SimpSolver::SimpSolver(CVC4::context::Context* c) :
   , bwdsub_assigns     (0)
   , n_touched          (0)
 {
-    CVC4::StatisticsRegistry::registerStat(&total_eliminate_time);
+
     vec<Lit> dummy(1,lit_Undef);
     ca.extra_clause_field = true; // NOTE: must happen before allocating the dummy clause below.
     bwdsub_tmpunit        = ca.alloc(dummy);
@@ -87,7 +89,7 @@ SimpSolver::SimpSolver(CVC4::context::Context* c) :
 
 SimpSolver::~SimpSolver()
 {
-  CVC4::StatisticsRegistry::unregisterStat(&total_eliminate_time); 
+  //  CVC4::StatisticsRegistry::unregisterStat(&total_eliminate_time); 
 }
 
 
@@ -606,7 +608,7 @@ void SimpSolver::extendModel()
 bool SimpSolver::eliminate(bool turn_off_elim)
 {
 
-  CVC4::TimerStat::CodeTimer codeTimer(total_eliminate_time);
+  //  CVC4::TimerStat::CodeTimer codeTimer(total_eliminate_time);
   
     if (!simplify())
         return false;
diff --git a/src/prop/bvminisat/simp/SimpSolver.h b/src/prop/bvminisat/simp/SimpSolver.h
index 4af82b02d..d808daa22 100644
--- a/src/prop/bvminisat/simp/SimpSolver.h
+++ b/src/prop/bvminisat/simp/SimpSolver.h
@@ -58,6 +58,7 @@ class SimpSolver : public Solver {
     //
     bool    solve       (const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false);
     lbool   solveLimited(const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false);
+    lbool   solveLimited(bool do_simp = true, bool turn_off_simp = false);
     bool    solve       (                     bool do_simp = true, bool turn_off_simp = false);
     bool    solve       (Lit p       ,        bool do_simp = true, bool turn_off_simp = false);       
     bool    solve       (Lit p, Lit q,        bool do_simp = true, bool turn_off_simp = false);
@@ -96,7 +97,7 @@ class SimpSolver : public Solver {
     int     merges;
     int     asymm_lits;
     int     eliminated_vars;
-    CVC4::TimerStat total_eliminate_time;
+  //    CVC4::TimerStat total_eliminate_time;
 
  protected:
 
@@ -195,6 +196,9 @@ inline bool SimpSolver::solve        (const vec<Lit>& assumps, bool do_simp, boo
 inline lbool SimpSolver::solveLimited (const vec<Lit>& assumps, bool do_simp, bool turn_off_simp){ 
     assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp); }
 
+inline lbool SimpSolver::solveLimited (bool do_simp, bool turn_off_simp){ 
+    return solve_(do_simp, turn_off_simp); }
+
 //=================================================================================================
 }
 
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 47d352949..3d2c29798 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -228,12 +228,6 @@ SatLiteral CnfStream::convertAtom(TNode node) {
     theoryLiteral = true;
     canEliminate = false;
     preRegister = true;
-
-    if (options::bitvectorEagerBitblast() && theory::Theory::theoryOf(node) == theory::THEORY_BV) {
-      // All BV atoms are treated as boolean except for equality
-      theoryLiteral = false;
-      canEliminate = true;
-    }
   }
 
   // Make a new literal (variables are not considered theory literals)
diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp
index 6cda02c00..e937c718c 100644
--- a/src/prop/sat_solver_factory.cpp
+++ b/src/prop/sat_solver_factory.cpp
@@ -25,8 +25,8 @@ namespace prop {
 template class SatSolverConstructor<MinisatSatSolver>;
 template class SatSolverConstructor<BVMinisatSatSolver>;
 
-BVSatSolverInterface* SatSolverFactory::createMinisat(context::Context* mainSatContext) {
-  return new BVMinisatSatSolver(mainSatContext);
+BVSatSolverInterface* SatSolverFactory::createMinisat(context::Context* mainSatContext, const std::string& name) {
+  return new BVMinisatSatSolver(mainSatContext, name);
 }
 
 DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat() {
diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h
index 7d3a45c59..291609de7 100644
--- a/src/prop/sat_solver_factory.h
+++ b/src/prop/sat_solver_factory.h
@@ -28,7 +28,7 @@ namespace prop {
 class SatSolverFactory {
 public:
 
-  static BVSatSolverInterface* createMinisat(context::Context* mainSatContext);
+  static BVSatSolverInterface* createMinisat(context::Context* mainSatContext, const std::string& name = "");
   static DPLLSatSolverInterface* createDPLLMinisat();
 
   static SatSolver* create(const char* id);