Fixes for Solver.h (#3851)

1 files changed, 8 insertions, 8 deletions

diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h
index 2197d030f..7324666a1 100644
--- a/src/prop/bvminisat/core/Solver.h
+++ b/src/prop/bvminisat/core/Solver.h
@@ -365,11 +365,11 @@ public:
 
   // Less than for literals in an added clause when proofs are on.
   struct assign_lt {
-    Solver& solver;
-    assign_lt(Solver& solver) : solver(solver) {}
+    Solver& d_solver;
+    assign_lt(Solver& solver) : d_solver(solver) {}
     bool operator () (Lit x, Lit y) {
-      lbool x_value = solver.value(x);
-      lbool y_value = solver.value(y);
+      lbool x_value = d_solver.value(x);
+      lbool y_value = d_solver.value(y);
       // Two unassigned literals are sorted arbitrarily
       if (x_value == l_Undef && y_value == l_Undef) {
         return x < y;
@@ -379,7 +379,7 @@ public:
       if (y_value == l_Undef) return false;
       // Literals of the same value are sorted by decreasing levels
       if (x_value == y_value) {
-        return solver.level(var(x)) > solver.level(var(y));
+        return d_solver.level(var(x)) > d_solver.level(var(y));
       } else {
         // True literals go up front
         if (x_value == l_True) {
@@ -417,8 +417,8 @@ inline void Solver::varBumpActivity(Var v, double inc) {
         order_heap.decrease(v); }
 
 inline void Solver::claDecayActivity() { cla_inc *= (1 / clause_decay); }
-inline void Solver::claBumpActivity (Clause& c) {
-        if ( (c.activity() += cla_inc) > 1e20 ) {
+inline void Solver::claBumpActivity (Clause& clause) {
+        if ( (clause.activity() += cla_inc) > 1e20 ) {
             // Rescale:
             for (int i = 0; i < learnts.size(); i++)
                 ca[learnts[i]].activity() *= 1e-20;
@@ -436,7 +436,7 @@ inline bool     Solver::addEmptyClause  ()                      { add_tmp.clear(
 inline bool     Solver::addClause       (Lit p, ClauseId& id)                 { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, id); }
 inline bool     Solver::addClause       (Lit p, Lit q, ClauseId& id)          { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, id); }
 inline bool     Solver::addClause       (Lit p, Lit q, Lit r, ClauseId& id)   { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, id); }
-inline bool     Solver::locked          (const Clause& c) const { return value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c; }
+inline bool     Solver::locked          (const Clause& clause) const { return value(clause[0]) == l_True && reason(var(clause[0])) != CRef_Undef && ca.lea(reason(var(clause[0]))) == &clause; }
 inline void     Solver::newDecisionLevel()                      { trail_lim.push(trail.size()); }
 
 inline int      Solver::decisionLevel ()      const   { return trail_lim.size(); }