Enable -Wshadow and fix warnings. (#3909)

Fixes all -Wshadow warnings and enables the -Wshadow compile flag globally. 

Co-authored-by: Clark Barrett <barrett@cs.stanford.edu>
Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>
Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
Co-authored-by: Alex Ozdemir <aozdemir@hmc.edu>
Co-authored-by: makaimann <makaim@stanford.edu>
Co-authored-by: yoni206 <yoni206@users.noreply.github.com>
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Co-authored-by: AleksandarZeljic <zeljic@stanford.edu>
Co-authored-by: Caleb Donovick <cdonovick@users.noreply.github.com>
Co-authored-by: Amalee <amaleewilson@gmail.com>
Co-authored-by: Scott Kovach <dskovach@gmail.com>
Co-authored-by: ntsis <nekuna@gmail.com>

4 files changed, 490 insertions, 381 deletions

diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index 25b6a3da2..84ab62fd8 100644
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -86,70 +86,92 @@ CRef Solver::TCRef_Lazy = CRef_Undef - 1; // no real lazy ref here
 //=================================================================================================
 // Constructor/Destructor:
 
-
-Solver::Solver(CVC4::context::Context* c) :
-
-    // Parameters (user settable):
-    //
-    d_notify(nullptr)
-  , c(c)
-  , verbosity        (0)
-  , var_decay        (opt_var_decay)
-  , clause_decay     (opt_clause_decay)
-  , random_var_freq  (opt_random_var_freq)
-  , random_seed      (opt_random_seed)
-  , luby_restart     (opt_luby_restart)
-  , ccmin_mode       (opt_ccmin_mode)
-  , phase_saving     (opt_phase_saving)
-  , rnd_pol          (false)
-  , rnd_init_act     (opt_rnd_init_act)
-  , garbage_frac     (opt_garbage_frac)
-  , restart_first    (opt_restart_first)
-  , restart_inc      (opt_restart_inc)
-
-    // Parameters (the rest):
-    //
-  , learntsize_factor((double)1/(double)3), learntsize_inc(1.5)
-
-    // Parameters (experimental):
-    //
-  , learntsize_adjust_start_confl (100)
-  , learntsize_adjust_inc         (1.5)
-
-    // Statistics: (formerly in 'SolverStats')
-    //
-  , solves(0), starts(0), decisions(0), rnd_decisions(0), propagations(0), conflicts(0)
-  , dec_vars(0), clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0)
-
-  , need_to_propagate(false)
-  , only_bcp(false)
-  , clause_added(false)
-  , ok                 (true)
-  , cla_inc            (1)
-  , var_inc            (1)
-  , watches            (WatcherDeleted(ca))
-  , qhead              (0)
-  , simpDB_assigns     (-1)
-  , simpDB_props       (0)
-  , order_heap         (VarOrderLt(activity))
-  , progress_estimate  (0)
-  , remove_satisfied   (true)
-
-  , ca                 ()
-
-  // even though these are temporaries and technically should be set
-  // before calling, lets initialize them. this will reduces chances of
-  // non-determinism in portfolio (parallel) solver if variables are
-  // being (incorrectly) used without initialization.
-  , seen(),  analyze_stack(), analyze_toclear(), add_tmp()
-  , max_learnts(0.0), learntsize_adjust_confl(0.0), learntsize_adjust_cnt(0)
-
-    // Resource constraints:
-    //
-  , conflict_budget    (-1)
-  , propagation_budget (-1)
-  , asynch_interrupt   (false)
-  , d_bvp              (NULL)
+Solver::Solver(CVC4::context::Context* context)
+    :
+
+      // Parameters (user settable):
+      //
+      d_notify(nullptr),
+      c(context),
+      verbosity(0),
+      var_decay(opt_var_decay),
+      clause_decay(opt_clause_decay),
+      random_var_freq(opt_random_var_freq),
+      random_seed(opt_random_seed),
+      luby_restart(opt_luby_restart),
+      ccmin_mode(opt_ccmin_mode),
+      phase_saving(opt_phase_saving),
+      rnd_pol(false),
+      rnd_init_act(opt_rnd_init_act),
+      garbage_frac(opt_garbage_frac),
+      restart_first(opt_restart_first),
+      restart_inc(opt_restart_inc)
+
+      // Parameters (the rest):
+      //
+      ,
+      learntsize_factor((double)1 / (double)3),
+      learntsize_inc(1.5)
+
+      // Parameters (experimental):
+      //
+      ,
+      learntsize_adjust_start_confl(100),
+      learntsize_adjust_inc(1.5)
+
+      // Statistics: (formerly in 'SolverStats')
+      //
+      ,
+      solves(0),
+      starts(0),
+      decisions(0),
+      rnd_decisions(0),
+      propagations(0),
+      conflicts(0),
+      dec_vars(0),
+      clauses_literals(0),
+      learnts_literals(0),
+      max_literals(0),
+      tot_literals(0)
+
+      ,
+      need_to_propagate(false),
+      only_bcp(false),
+      clause_added(false),
+      ok(true),
+      cla_inc(1),
+      var_inc(1),
+      watches(WatcherDeleted(ca)),
+      qhead(0),
+      simpDB_assigns(-1),
+      simpDB_props(0),
+      order_heap(VarOrderLt(activity)),
+      progress_estimate(0),
+      remove_satisfied(true)
+
+      ,
+      ca()
+
+      // even though these are temporaries and technically should be set
+      // before calling, lets initialize them. this will reduces chances of
+      // non-determinism in portfolio (parallel) solver if variables are
+      // being (incorrectly) used without initialization.
+      ,
+      seen(),
+      analyze_stack(),
+      analyze_toclear(),
+      add_tmp(),
+      max_learnts(0.0),
+      learntsize_adjust_confl(0.0),
+      learntsize_adjust_cnt(0)
+
+      // Resource constraints:
+      //
+      ,
+      conflict_budget(-1),
+      propagation_budget(-1),
+      asynch_interrupt(false),
+      d_bvp(NULL)
 {
   // Create the constant variables
   varTrue = newVar(true, false);
@@ -304,65 +326,73 @@ bool Solver::addClause_(vec<Lit>& ps, ClauseId& id)
 }
 
 void Solver::attachClause(CRef cr) {
-    const Clause& c = ca[cr];
-    assert(c.size() > 1);
-    watches[~c[0]].push(Watcher(cr, c[1]));
-    watches[~c[1]].push(Watcher(cr, c[0]));
-    if (c.learnt()) learnts_literals += c.size();
-    else            clauses_literals += c.size(); }
-
+  const Clause& clause = ca[cr];
+  assert(clause.size() > 1);
+  watches[~clause[0]].push(Watcher(cr, clause[1]));
+  watches[~clause[1]].push(Watcher(cr, clause[0]));
+  if (clause.learnt())
+    learnts_literals += clause.size();
+  else
+    clauses_literals += clause.size();
+}
 
 void Solver::detachClause(CRef cr, bool strict) {
-    const Clause& c = ca[cr];
-    if(d_bvp){ d_bvp->getSatProof()->markDeleted(cr); }
-    
-    assert(c.size() > 1);
-    
-    if (strict){
-        remove(watches[~c[0]], Watcher(cr, c[1]));
-        remove(watches[~c[1]], Watcher(cr, c[0]));
+  const Clause& clause = ca[cr];
+  if (d_bvp)
+  {
+    d_bvp->getSatProof()->markDeleted(cr); }
+
+  assert(clause.size() > 1);
+
+  if (strict)
+  {
+    remove(watches[~clause[0]], Watcher(cr, clause[1]));
+    remove(watches[~clause[1]], Watcher(cr, clause[0]));
     }else{
         // Lazy detaching: (NOTE! Must clean all watcher lists before garbage collecting this clause)
-        watches.smudge(~c[0]);
-        watches.smudge(~c[1]);
+        watches.smudge(~clause[0]);
+        watches.smudge(~clause[1]);
     }
 
-    if (c.learnt()) learnts_literals -= c.size();
-    else            clauses_literals -= c.size(); }
-
+    if (clause.learnt())
+      learnts_literals -= clause.size();
+    else
+      clauses_literals -= clause.size();
+}
 
 void Solver::removeClause(CRef cr) {
-    Clause& c = ca[cr];
-    detachClause(cr);
-    // Don't leave pointers to free'd memory!
-    if (locked(c)) vardata[var(c[0])].reason = CRef_Undef;
-    c.mark(1); 
-    ca.free(cr);
+  Clause& clause = ca[cr];
+  detachClause(cr);
+  // Don't leave pointers to free'd memory!
+  if (locked(clause)) vardata[var(clause[0])].reason = CRef_Undef;
+  clause.mark(1);
+  ca.free(cr);
 }
 
-
-bool Solver::satisfied(const Clause& c) const {
-    for (int i = 0; i < c.size(); i++)
-        if (value(c[i]) == l_True)
-            return true;
-    return false; }
-
+bool Solver::satisfied(const Clause& clause) const
+{
+  for (int i = 0; i < clause.size(); i++)
+    if (value(clause[i]) == l_True) return true;
+  return false;
+}
 
 // Revert to the state at given level (keeping all assignment at 'level' but not beyond).
 //
 void Solver::cancelUntil(int level) {
     if (decisionLevel() > level){
       Debug("bvminisat::explain") << OUTPUT_TAG << " backtracking to " << level << std::endl;
-      for (int c = trail.size()-1; c >= trail_lim[level]; c--){
-            Var      x  = var(trail[c]);
-            assigns [x] = l_Undef;
-            if (marker[x] == 2) marker[x] = 1;
-            if (phase_saving > 1
-                || ((phase_saving == 1) && c > trail_lim.last()))
-            {
-              polarity[x] = sign(trail[c]);
-            }
-            insertVarOrder(x); }
+      for (int clause = trail.size() - 1; clause >= trail_lim[level]; clause--)
+      {
+        Var x = var(trail[clause]);
+        assigns[x] = l_Undef;
+        if (marker[x] == 2) marker[x] = 1;
+        if (phase_saving > 1
+            || ((phase_saving == 1) && clause > trail_lim.last()))
+        {
+          polarity[x] = sign(trail[clause]);
+        }
+        insertVarOrder(x);
+      }
         qhead = trail_lim[level];
         trail.shrink(trail.size() - trail_lim[level]);
         trail_lim.shrink(trail_lim.size() - level);
@@ -429,28 +459,33 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip
 
     do{
         assert(confl != CRef_Undef); // (otherwise should be UIP)
-        Clause& c = ca[confl];
-
-        if (c.learnt())
-            claBumpActivity(c);
-
-        for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){
-            Lit q = c[j];
+        Clause& clause = ca[confl];
+
+        if (clause.learnt()) claBumpActivity(clause);
+
+        for (int j = (p == lit_Undef) ? 0 : 1; j < clause.size(); j++)
+        {
+          Lit q = clause[j];
+
+          if (!seen[var(q)] && level(var(q)) > 0)
+          {
+            varBumpActivity(var(q));
+            seen[var(q)] = 1;
+            if (level(var(q)) >= decisionLevel())
+              pathC++;
+            else
+              out_learnt.push(q);
+          }
 
-            if (!seen[var(q)] && level(var(q)) > 0) {
-                varBumpActivity(var(q));
-                seen[var(q)] = 1;
-                if (level(var(q)) >= decisionLevel())
-                    pathC++;
-                else
-                    out_learnt.push(q);
-            }
-            
-            if (level(var(q)) == 0) {
-              if(d_bvp){ d_bvp->getSatProof()->resolveOutUnit(q); }
+          if (level(var(q)) == 0)
+          {
+            if (d_bvp)
+            {
+              d_bvp->getSatProof()->resolveOutUnit(q);
             }
+          }
         }
-        
+
         // Select next clause to look at:
         while (!seen[var(trail[index--])]);
         p     = trail[index+1];
@@ -478,51 +513,68 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip
 
     // Simplify conflict clause:
     //
-    int i, j;
+    int i1, j;
     out_learnt.copyTo(analyze_toclear);
     if (ccmin_mode == 2){
         uint32_t abstract_level = 0;
-        for (i = 1; i < out_learnt.size(); i++)
-            abstract_level |= abstractLevel(var(out_learnt[i])); // (maintain an abstraction of levels involved in conflict)
-
-        for (i = j = 1; i < out_learnt.size(); i++) {
-            if (reason(var(out_learnt[i])) == CRef_Undef) {
-                out_learnt[j++] = out_learnt[i];
-            } else {
-              // Check if the literal is redundant
-              if (!litRedundant(out_learnt[i], abstract_level)) {
-                // Literal is not redundant
-                out_learnt[j++] = out_learnt[i];
-              } else {
-                if(d_bvp){ d_bvp->getSatProof()->storeLitRedundant(out_learnt[i]); }
+        for (i1 = 1; i1 < out_learnt.size(); i1++)
+          abstract_level |= abstractLevel(
+              var(out_learnt[i1]));  // (maintain an abstraction of levels
+                                     // involved in conflict)
+
+        for (i1 = j = 1; i1 < out_learnt.size(); i1++)
+        {
+          if (reason(var(out_learnt[i1])) == CRef_Undef)
+          {
+            out_learnt[j++] = out_learnt[i1];
+          }
+          else
+          {
+            // Check if the literal is redundant
+            if (!litRedundant(out_learnt[i1], abstract_level))
+            {
+              // Literal is not redundant
+              out_learnt[j++] = out_learnt[i1];
+            }
+            else
+            {
+              if (d_bvp)
+              {
+                d_bvp->getSatProof()->storeLitRedundant(out_learnt[i1]);
               }
             }
+          }
         }
-        
     }else if (ccmin_mode == 1){
         Unreachable();
-        for (i = j = 1; i < out_learnt.size(); i++){
-            Var x = var(out_learnt[i]);
-
-            if (reason(x) == CRef_Undef)
-                out_learnt[j++] = out_learnt[i];
-            else{
-                Clause& c = ca[reason(var(out_learnt[i]))];
-                for (int k = 1; k < c.size(); k++)
-                    if (!seen[var(c[k])] && level(var(c[k])) > 0){
-                        out_learnt[j++] = out_learnt[i];
-                        break; }
-            }
+        for (i1 = j = 1; i1 < out_learnt.size(); i1++)
+        {
+          Var x = var(out_learnt[i1]);
+
+          if (reason(x) == CRef_Undef)
+            out_learnt[j++] = out_learnt[i1];
+          else
+          {
+            Clause& clause = ca[reason(var(out_learnt[i1]))];
+            for (int k = 1; k < clause.size(); k++)
+              if (!seen[var(clause[k])] && level(var(clause[k])) > 0)
+              {
+                out_learnt[j++] = out_learnt[i1];
+                break;
+              }
+          }
         }
     }else
-        i = j = out_learnt.size();
+      i1 = j = out_learnt.size();
 
     max_literals += out_learnt.size();
-    out_learnt.shrink(i - j);
+    out_learnt.shrink(i1 - j);
     tot_literals += out_learnt.size();
 
-    for (int i = 0; i < out_learnt.size(); ++ i) {
-      if (marker[var(out_learnt[i])] == 0) {
+    for (int i2 = 0; i2 < out_learnt.size(); ++i2)
+    {
+      if (marker[var(out_learnt[i2])] == 0)
+      {
         break;
       }
     }
@@ -535,17 +587,18 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip
     else{
         int max_i = 1;
         // 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])))
-                max_i = i;
-        // Swap-in this literal at index 1:
-        Lit p             = out_learnt[max_i];
+        for (int i3 = 2; i3 < out_learnt.size(); i3++)
+          if (level(var(out_learnt[i3])) > level(var(out_learnt[max_i])))
+            max_i = i3;
+        // Swap-in this literal at i1 1:
+        Lit p2 = out_learnt[max_i];
         out_learnt[max_i] = out_learnt[1];
-        out_learnt[1]     = p;
-        out_btlevel       = level(var(p));
+        out_learnt[1] = p2;
+        out_btlevel = level(var(p2));
     }
 
-    for (int j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0;    // ('seen[]' is now cleared)
+    for (int j2 = 0; j2 < analyze_toclear.size(); j2++)
+      seen[var(analyze_toclear[j2])] = 0;  // ('seen[]' is now cleared)
 }
 
 
@@ -558,24 +611,29 @@ bool Solver::litRedundant(Lit p, uint32_t abstract_levels)
     while (analyze_stack.size() > 0){
         CRef c_reason = reason(var(analyze_stack.last()));
         assert(c_reason != CRef_Undef);
-        Clause& c = ca[c_reason];
-        int c_size = c.size();
+        Clause& clause = ca[c_reason];
+        int c_size = clause.size();
         analyze_stack.pop();
 
         for (int i = 1; i < c_size; i++){
-            Lit p  = c[i];
-            if (!seen[var(p)] && level(var(p)) > 0){
-                if (reason(var(p)) != CRef_Undef && (abstractLevel(var(p)) & abstract_levels) != 0){
-                    seen[var(p)] = 1;
-                    analyze_stack.push(p);
-                    analyze_toclear.push(p);
-                }else{
-                    for (int j = top; j < analyze_toclear.size(); j++)
-                        seen[var(analyze_toclear[j])] = 0;
-                    analyze_toclear.shrink(analyze_toclear.size() - top);
-                    return false;
-                }
+          Lit p2 = clause[i];
+          if (!seen[var(p2)] && level(var(p2)) > 0)
+          {
+            if (reason(var(p2)) != CRef_Undef
+                && (abstractLevel(var(p2)) & abstract_levels) != 0)
+            {
+              seen[var(p2)] = 1;
+              analyze_stack.push(p2);
+              analyze_toclear.push(p2);
+            }
+            else
+            {
+              for (int j = top; j < analyze_toclear.size(); j++)
+                seen[var(analyze_toclear[j])] = 0;
+              analyze_toclear.shrink(analyze_toclear.size() - top);
+              return false;
             }
+          }
         }
     }
 
@@ -619,16 +677,18 @@ void Solver::analyzeFinal2(Lit p, CRef confl_clause, vec<Lit>& out_conflict) {
           if(d_bvp){d_bvp->getSatProof()->resolveOutUnit(~p);} 
         }
       } else {
-        Clause& c = ca[reason(x)];
+        Clause& clause = ca[reason(x)];
         if(d_bvp){d_bvp->getSatProof()->addResolutionStep(trail[i],reason(x), sign(trail[i]));}
 
-        for (int j = 1; j < c.size(); j++) {
-          if (level(var(c[j])) > 0)
-            seen[var(c[j])] = 1;
+        for (int j = 1; j < clause.size(); j++)
+        {
+          if (level(var(clause[j])) > 0) seen[var(clause[j])] = 1;
           if(d_bvp){
-            if (level(var(c[j])) == 0) {
-              d_bvp->getSatProof()->resolveOutUnit(c[j]);
-              seen[var(c[j])] = 0; // we don't need to resolve it out again
+            if (level(var(clause[j])) == 0)
+            {
+              d_bvp->getSatProof()->resolveOutUnit(clause[j]);
+              seen[var(clause[j])] =
+                  0;  // we don't need to resolve it out again
             }
           }
         }
@@ -683,7 +743,7 @@ void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict)
                 out_conflict.push(~trail[i]);
               }
             } else {
-              Clause& c = ca[reason(x)];
+              Clause& clause = ca[reason(x)];
               if(d_bvp){
                     if (d_bvp->isAssumptionConflict() &&
                         trail[i] == p) {
@@ -692,13 +752,16 @@ void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict)
                       d_bvp->getSatProof()->addResolutionStep(trail[i], reason(x), sign(trail[i]));
                     }
               }
-              for (int j = 1; j < c.size(); j++) {
-                if (level(var(c[j])) > 0) {
-                  seen[var(c[j])] = 1;
+              for (int j = 1; j < clause.size(); j++)
+              {
+                if (level(var(clause[j])) > 0)
+                {
+                  seen[var(clause[j])] = 1;
                 }
                 if(d_bvp){
-                  if (level(var(c[j])) == 0) {
-                    d_bvp->getSatProof()->resolveOutUnit(c[j]);
+                  if (level(var(clause[j])) == 0)
+                  {
+                    d_bvp->getSatProof()->resolveOutUnit(clause[j]);
                   }
                 }
               }
@@ -813,25 +876,28 @@ CRef Solver::propagate()
 
             // Make sure the false literal is data[1]:
             CRef     cr        = i->cref;
-            Clause&  c         = ca[cr];
+            Clause& clause = ca[cr];
             Lit      false_lit = ~p;
-            if (c[0] == false_lit)
-                c[0] = c[1], c[1] = false_lit;
-            assert(c[1] == false_lit);
+            if (clause[0] == false_lit)
+              clause[0] = clause[1], clause[1] = false_lit;
+            assert(clause[1] == false_lit);
             i++;
 
             // If 0th watch is true, then clause is already satisfied.
-            Lit     first = c[0];
+            Lit first = clause[0];
             Watcher w     = Watcher(cr, first);
             if (first != blocker && value(first) == l_True){
                 *j++ = w; continue; }
 
             // Look for new watch:
-            for (int k = 2; k < c.size(); k++)
-                if (value(c[k]) != l_False){
-                    c[1] = c[k]; c[k] = false_lit;
-                    watches[~c[1]].push(w);
-                    goto NextClause; }
+            for (int k = 2; k < clause.size(); k++)
+              if (value(clause[k]) != l_False)
+              {
+                clause[1] = clause[k];
+                clause[k] = false_lit;
+                watches[~clause[1]].push(w);
+                goto NextClause;
+              }
 
             // Did not find watch -- clause is unit under assignment:
             *j++ = w;
@@ -878,11 +944,12 @@ void Solver::reduceDB()
     // Don't delete binary or locked clauses. From the rest, delete clauses from the first half
     // and clauses with activity smaller than 'extra_lim':
     for (i = j = 0; i < learnts.size(); i++){
-        Clause& c = ca[learnts[i]];
-        if (c.size() > 2 && !locked(c) && (i < learnts.size() / 2 || c.activity() < extra_lim))
-            removeClause(learnts[i]);
-        else
-            learnts[j++] = learnts[i];
+      Clause& clause = ca[learnts[i]];
+      if (clause.size() > 2 && !locked(clause)
+          && (i < learnts.size() / 2 || clause.activity() < extra_lim))
+        removeClause(learnts[i]);
+      else
+        learnts[j++] = learnts[i];
     }
     learnts.shrink(i - j);
     checkGarbage();
@@ -893,14 +960,19 @@ void Solver::removeSatisfied(vec<CRef>& cs)
 {
     int i, j;
     for (i = j = 0; i < cs.size(); i++){
-        Clause& c = ca[cs[i]];
-        if (satisfied(c)) {
-          if (locked(c)) {
-            // store a resolution of the literal c propagated
-            if(d_bvp){ d_bvp->getSatProof()->storeUnitResolution(c[0]); }
+      Clause& clause = ca[cs[i]];
+      if (satisfied(clause))
+      {
+        if (locked(clause))
+        {
+          // store a resolution of the literal clause propagated
+          if (d_bvp)
+          {
+            d_bvp->getSatProof()->storeUnitResolution(clause[0]);
           }
-            removeClause(cs[i]);
         }
+        removeClause(cs[i]);
+      }
         else
             cs[j++] = cs[i];
     }
@@ -1290,7 +1362,7 @@ void Solver::explain(Lit p, std::vector<Lit>& explanation) {
          }
         
       } else {
-        Clause& c = ca[reason(x)];
+        Clause& clause = ca[reason(x)];
         if(d_bvp){
           if (p == trail[i]) {
             d_bvp->startBVConflict(reason(var(p)));
@@ -1298,9 +1370,11 @@ void Solver::explain(Lit p, std::vector<Lit>& explanation) {
             d_bvp->getSatProof()->addResolutionStep(trail[i], reason(x), sign(trail[i]));
           }
         }
-        for (int j = 1; j < c.size(); j++) {
-          if (level(var(c[j])) > 0 || options::proof()) {
-            seen[var(c[j])] = 1;
+        for (int j = 1; j < clause.size(); j++)
+        {
+          if (level(var(clause[j])) > 0 || options::proof())
+          {
+            seen[var(clause[j])] = 1;
           }
         }
       }
@@ -1341,15 +1415,17 @@ static Var mapVar(Var x, vec<Var>& map, Var& max)
     return map[x];
 }
 
-
-void Solver::toDimacs(FILE* f, Clause& c, vec<Var>& map, Var& max)
+void Solver::toDimacs(FILE* f, Clause& clause, vec<Var>& map, Var& max)
 {
-    if (satisfied(c)) return;
-
-    for (int i = 0; i < c.size(); i++)
-        if (value(c[i]) != l_False)
-            fprintf(f, "%s%d ", sign(c[i]) ? "-" : "", mapVar(var(c[i]), map, max)+1);
-    fprintf(f, "0\n");
+  if (satisfied(clause)) return;
+
+  for (int i = 0; i < clause.size(); i++)
+    if (value(clause[i]) != l_False)
+      fprintf(f,
+              "%s%d ",
+              sign(clause[i]) ? "-" : "",
+              mapVar(var(clause[i]), map, max) + 1);
+  fprintf(f, "0\n");
 }
 
 
@@ -1381,10 +1457,9 @@ void Solver::toDimacs(FILE* f, const vec<Lit>& assumps)
         
     for (int i = 0; i < clauses.size(); i++)
         if (!satisfied(ca[clauses[i]])){
-            Clause& c = ca[clauses[i]];
-            for (int j = 0; j < c.size(); j++)
-                if (value(c[j]) != l_False)
-                    mapVar(var(c[j]), map, max);
+          Clause& clause = ca[clauses[i]];
+          for (int j = 0; j < clause.size(); j++)
+            if (value(clause[j]) != l_False) mapVar(var(clause[j]), map, max);
         }
 
     // Assumptions are added as unit clauses:
diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h
index 2197d030f..7fad72d6d 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,12 +417,15 @@ 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 ) {
-            // Rescale:
-            for (int i = 0; i < learnts.size(); i++)
-                ca[learnts[i]].activity() *= 1e-20;
-            cla_inc *= 1e-20; } }
+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;
+    cla_inc *= 1e-20;
+  }
+}
 
 inline void Solver::checkGarbage(void){ return checkGarbage(garbage_frac); }
 inline void Solver::checkGarbage(double gf){
@@ -436,7 +439,11 @@ 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(); }
diff --git a/src/prop/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc
index 9e50433ef..b003342c6 100644
--- a/src/prop/bvminisat/simp/SimpSolver.cc
+++ b/src/prop/bvminisat/simp/SimpSolver.cc
@@ -48,8 +48,8 @@ static DoubleOption opt_simp_garbage_frac(_cat, "simp-gc-frac", "The fraction of
 //=================================================================================================
 // Constructor/Destructor:
 
-SimpSolver::SimpSolver(CVC4::context::Context* c)
-    : Solver(c),
+SimpSolver::SimpSolver(CVC4::context::Context* context)
+    : Solver(context),
       grow(opt_grow),
       clause_lim(opt_clause_lim),
       subsumption_lim(opt_subsumption_lim),
@@ -181,7 +181,7 @@ bool SimpSolver::addClause_(vec<Lit>& ps, ClauseId& id)
 
     if (use_simplification && clauses.size() == nclauses + 1){
         CRef          cr = clauses.last();
-        const Clause& c  = ca[cr];
+        const Clause& clause = ca[cr];
 
         // NOTE: the clause is added to the queue immediately and then
         // again during 'gatherTouchedClauses()'. If nothing happens
@@ -190,13 +190,14 @@ bool SimpSolver::addClause_(vec<Lit>& ps, ClauseId& id)
         // consequence of how backward subsumption is used to mimic
         // forward subsumption.
         subsumption_queue.insert(cr);
-        for (int i = 0; i < c.size(); i++){
-            occurs[var(c[i])].push(cr);
-            n_occ[toInt(c[i])]++;
-            touched[var(c[i])] = 1;
-            n_touched++;
-            if (elim_heap.inHeap(var(c[i])))
-                elim_heap.increase(var(c[i]));
+        for (int i = 0; i < clause.size(); i++)
+        {
+          occurs[var(clause[i])].push(cr);
+          n_occ[toInt(clause[i])]++;
+          touched[var(clause[i])] = 1;
+          n_touched++;
+          if (elim_heap.inHeap(var(clause[i])))
+            elim_heap.increase(var(clause[i]));
         }
     }
 
@@ -206,14 +207,15 @@ bool SimpSolver::addClause_(vec<Lit>& ps, ClauseId& id)
 
 void SimpSolver::removeClause(CRef cr)
 {
-    const Clause& c = ca[cr];
+  const Clause& clause = ca[cr];
 
-    if (use_simplification)
-        for (int i = 0; i < c.size(); i++){
-            n_occ[toInt(c[i])]--;
-            updateElimHeap(var(c[i]));
-            occurs.smudge(var(c[i]));
-        }
+  if (use_simplification)
+    for (int i = 0; i < clause.size(); i++)
+    {
+      n_occ[toInt(clause[i])]--;
+      updateElimHeap(var(clause[i]));
+      occurs.smudge(var(clause[i]));
+    }
 
     Solver::removeClause(cr);
 }
@@ -221,27 +223,31 @@ void SimpSolver::removeClause(CRef cr)
 
 bool SimpSolver::strengthenClause(CRef cr, Lit l)
 {
-    Clause& c = ca[cr];
-    assert(decisionLevel() == 0);
-    assert(use_simplification);
-
-    // FIX: this is too inefficient but would be nice to have (properly implemented)
-    // if (!find(subsumption_queue, &c))
-    subsumption_queue.insert(cr);
-
-    if (c.size() == 2){
-        removeClause(cr);
-        c.strengthen(l);
-    }else{
-        detachClause(cr, true);
-        c.strengthen(l);
-        attachClause(cr);
-        remove(occurs[var(l)], cr);
-        n_occ[toInt(l)]--;
-        updateElimHeap(var(l));
-    }
-
-    return c.size() == 1 ? enqueue(c[0]) && propagate() == CRef_Undef : true;
+  Clause& clause = ca[cr];
+  assert(decisionLevel() == 0);
+  assert(use_simplification);
+
+  // FIX: this is too inefficient but would be nice to have (properly
+  // implemented) if (!find(subsumption_queue, &clause))
+  subsumption_queue.insert(cr);
+
+  if (clause.size() == 2)
+  {
+    removeClause(cr);
+    clause.strengthen(l);
+  }
+  else
+  {
+    detachClause(cr, true);
+    clause.strengthen(l);
+    attachClause(cr);
+    remove(occurs[var(l)], cr);
+    n_occ[toInt(l)]--;
+    updateElimHeap(var(l));
+  }
+
+  return clause.size() == 1 ? enqueue(clause[0]) && propagate() == CRef_Undef
+                            : true;
 }
 
 
@@ -345,20 +351,22 @@ void SimpSolver::gatherTouchedClauses()
     n_touched = 0;
 }
 
-
-bool SimpSolver::implied(const vec<Lit>& c)
+bool SimpSolver::implied(const vec<Lit>& clause)
 {
     assert(decisionLevel() == 0);
 
     trail_lim.push(trail.size());
-    for (int i = 0; i < c.size(); i++)
-        if (value(c[i]) == l_True){
-            cancelUntil(0);
-            return false;
-        }else if (value(c[i]) != l_False){
-            assert(value(c[i]) == l_Undef);
-            uncheckedEnqueue(~c[i]);
-        }
+    for (int i = 0; i < clause.size(); i++)
+      if (value(clause[i]) == l_True)
+      {
+        cancelUntil(0);
+        return false;
+      }
+      else if (value(clause[i]) != l_False)
+      {
+        assert(value(clause[i]) == l_Undef);
+        uncheckedEnqueue(~clause[i]);
+      }
 
     bool result = propagate() != CRef_Undef;
     cancelUntil(0);
@@ -390,44 +398,49 @@ bool SimpSolver::backwardSubsumptionCheck(bool verbose)
             subsumption_queue.insert(bwdsub_tmpunit); }
 
         CRef    cr = subsumption_queue.peek(); subsumption_queue.pop();
-        Clause& c  = ca[cr];
+        Clause& clause = ca[cr];
 
-        if (c.mark()) continue;
+        if (clause.mark()) continue;
 
         if (verbose && verbosity >= 2 && cnt++ % 1000 == 0)
             printf("subsumption left: %10d (%10d subsumed, %10d deleted literals)\r", subsumption_queue.size(), subsumed, deleted_literals);
 
-        assert(c.size() > 1 || value(c[0]) == l_True);    // Unit-clauses should have been propagated before this point.
+        assert(clause.size() > 1
+               || value(clause[0]) == l_True);  // Unit-clauses should have been
+                                                // propagated before this point.
 
         // Find best variable to scan:
-        Var best = var(c[0]);
-        for (int i = 1; i < c.size(); i++)
-            if (occurs[var(c[i])].size() < occurs[best].size())
-                best = var(c[i]);
+        Var best = var(clause[0]);
+        for (int i = 1; i < clause.size(); i++)
+          if (occurs[var(clause[i])].size() < occurs[best].size())
+            best = var(clause[i]);
 
         // Search all candidates:
         vec<CRef>& _cs = occurs.lookup(best);
         CRef*       cs = (CRef*)_cs;
 
         for (int j = 0; j < _cs.size(); j++)
-            if (c.mark())
-                break;
-            else if (!ca[cs[j]].mark() &&  cs[j] != cr && (subsumption_lim == -1 || ca[cs[j]].size() < subsumption_lim)){
-                Lit l = c.subsumes(ca[cs[j]]);
-
-                if (l == lit_Undef)
-                    subsumed++, removeClause(cs[j]);
-                else if (l != lit_Error){
-                    deleted_literals++;
-
-                    if (!strengthenClause(cs[j], ~l))
-                        return false;
-
-                    // Did current candidate get deleted from cs? Then check candidate at index j again:
-                    if (var(l) == best)
-                        j--;
-                }
+          if (clause.mark())
+            break;
+          else if (!ca[cs[j]].mark() && cs[j] != cr
+                   && (subsumption_lim == -1
+                       || ca[cs[j]].size() < subsumption_lim))
+          {
+            Lit l = clause.subsumes(ca[cs[j]]);
+
+            if (l == lit_Undef)
+              subsumed++, removeClause(cs[j]);
+            else if (l != lit_Error)
+            {
+              deleted_literals++;
+
+              if (!strengthenClause(cs[j], ~l)) return false;
+
+              // Did current candidate get deleted from cs? Then check candidate
+              // at index j again:
+              if (var(l) == best) j--;
             }
+          }
     }
 
     return true;
@@ -436,28 +449,29 @@ bool SimpSolver::backwardSubsumptionCheck(bool verbose)
 
 bool SimpSolver::asymm(Var v, CRef cr)
 {
-    Clause& c = ca[cr];
-    assert(decisionLevel() == 0);
+  Clause& clause = ca[cr];
+  assert(decisionLevel() == 0);
 
-    if (c.mark() || satisfied(c)) return true;
+  if (clause.mark() || satisfied(clause)) return true;
 
-    trail_lim.push(trail.size());
-    Lit l = lit_Undef;
-    for (int i = 0; i < c.size(); i++)
-        if (var(c[i]) != v && value(c[i]) != l_False)
-            uncheckedEnqueue(~c[i]);
-        else
-            l = c[i];
-
-    if (propagate() != CRef_Undef){
-        cancelUntil(0);
-        asymm_lits++;
-        if (!strengthenClause(cr, l))
-            return false;
-    }else
-        cancelUntil(0);
+  trail_lim.push(trail.size());
+  Lit l = lit_Undef;
+  for (int i = 0; i < clause.size(); i++)
+    if (var(clause[i]) != v && value(clause[i]) != l_False)
+      uncheckedEnqueue(~clause[i]);
+    else
+      l = clause[i];
 
-    return true;
+  if (propagate() != CRef_Undef)
+  {
+    cancelUntil(0);
+    asymm_lits++;
+    if (!strengthenClause(cr, l)) return false;
+  }
+  else
+    cancelUntil(0);
+
+  return true;
 }
 
 
@@ -484,18 +498,17 @@ static void mkElimClause(vec<uint32_t>& elimclauses, Lit x)
     elimclauses.push(1);
 }
 
-
-static void mkElimClause(vec<uint32_t>& elimclauses, Var v, Clause& c)
+static void mkElimClause(vec<uint32_t>& elimclauses, Var v, Clause& clause)
 {
     int first = elimclauses.size();
     int v_pos = -1;
 
     // Copy clause to elimclauses-vector. Remember position where the
     // variable 'v' occurs:
-    for (int i = 0; i < c.size(); i++){
-        elimclauses.push(toInt(c[i]));
-        if (var(c[i]) == v)
-            v_pos = i + first;
+    for (int i = 0; i < clause.size(); i++)
+    {
+      elimclauses.push(toInt(clause[i]));
+      if (var(clause[i]) == v) v_pos = i + first;
     }
     assert(v_pos != -1);
 
@@ -506,7 +519,7 @@ static void mkElimClause(vec<uint32_t>& elimclauses, Var v, Clause& c)
     elimclauses[first] = tmp;
 
     // Store the length of the clause last:
-    elimclauses.push(c.size());
+    elimclauses.push(clause.size());
 }
 
 
@@ -590,13 +603,14 @@ bool SimpSolver::substitute(Var v, Lit x)
     
     vec<Lit>& subst_clause = add_tmp;
     for (int i = 0; i < cls.size(); i++){
-        Clause& c = ca[cls[i]];
+      Clause& clause = ca[cls[i]];
 
-        subst_clause.clear();
-        for (int j = 0; j < c.size(); j++){
-            Lit p = c[j];
-            subst_clause.push(var(p) == v ? x ^ sign(p) : p);
-        }
+      subst_clause.clear();
+      for (int j = 0; j < clause.size(); j++)
+      {
+        Lit p = clause[j];
+        subst_clause.push(var(p) == v ? x ^ sign(p) : p);
+      }
 
         removeClause(cls[i]);
         ClauseId id;
diff --git a/src/prop/bvminisat/simp/SimpSolver.h b/src/prop/bvminisat/simp/SimpSolver.h
index 246bb7152..9d3a51c02 100644
--- a/src/prop/bvminisat/simp/SimpSolver.h
+++ b/src/prop/bvminisat/simp/SimpSolver.h
@@ -37,42 +37,55 @@ class SimpSolver : public Solver {
  public:
     // Constructor/Destructor:
     //
-    SimpSolver(CVC4::context::Context* c);
-    ~SimpSolver();
-
-    // Problem specification:
-    //
-    Var     newVar    (bool polarity = true, bool dvar = true, bool freeze = false);
-    bool    addClause (const vec<Lit>& ps, ClauseId& id);
-    bool    addEmptyClause();                // Add the empty clause to the solver.
-    bool    addClause (Lit p, ClauseId& id);               // Add a unit clause to the solver.
-    bool    addClause (Lit p, Lit q, ClauseId& id);        // Add a binary clause to the solver.
-    bool    addClause (Lit p, Lit q, Lit r, ClauseId& id); // Add a ternary clause to the solver.
-    bool    addClause_( vec<Lit>& ps, ClauseId& id);
-    bool    substitute(Var v, Lit x);  // Replace all occurences of v with x (may cause a contradiction).
-
-    // Variable mode:
-    // 
-    void    setFrozen (Var v, bool b); // If a variable is frozen it will not be eliminated.
-    bool    isEliminated(Var v) const;
-
-    // Solving:
-    //
-    lbool    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);
-    lbool    solve       (                     bool do_simp = true, bool turn_off_simp = false);
-    lbool    solve       (Lit p       ,        bool do_simp = true, bool turn_off_simp = false);       
-    lbool    solve       (Lit p, Lit q,        bool do_simp = true, bool turn_off_simp = false);
-    lbool    solve       (Lit p, Lit q, Lit r, bool do_simp = true, bool turn_off_simp = false);
-    bool    eliminate   (bool turn_off_elim = false);  // Perform variable elimination based simplification. 
-
-    // Memory managment:
-    //
-    void garbageCollect() override;
-
-    // Generate a (possibly simplified) DIMACS file:
-    //
+  SimpSolver(CVC4::context::Context* context);
+  ~SimpSolver();
+
+  // Problem specification:
+  //
+  Var newVar(bool polarity = true, bool dvar = true, bool freeze = false);
+  bool addClause(const vec<Lit>& ps, ClauseId& id);
+  bool addEmptyClause();                // Add the empty clause to the solver.
+  bool addClause(Lit p, ClauseId& id);  // Add a unit clause to the solver.
+  bool addClause(Lit p,
+                 Lit q,
+                 ClauseId& id);  // Add a binary clause to the solver.
+  bool addClause(Lit p,
+                 Lit q,
+                 Lit r,
+                 ClauseId& id);  // Add a ternary clause to the solver.
+  bool addClause_(vec<Lit>& ps, ClauseId& id);
+  bool substitute(Var v, Lit x);  // Replace all occurences of v with x (may
+                                  // cause a contradiction).
+
+  // Variable mode:
+  //
+  void setFrozen(Var v,
+                 bool b);  // If a variable is frozen it will not be eliminated.
+  bool isEliminated(Var v) const;
+
+  // Solving:
+  //
+  lbool 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);
+  lbool solve(bool do_simp = true, bool turn_off_simp = false);
+  lbool solve(Lit p, bool do_simp = true, bool turn_off_simp = false);
+  lbool solve(Lit p, Lit q, bool do_simp = true, bool turn_off_simp = false);
+  lbool solve(
+      Lit p, Lit q, Lit r, bool do_simp = true, bool turn_off_simp = false);
+  bool eliminate(bool turn_off_elim = false);  // Perform variable elimination
+                                               // based simplification.
+
+  // Memory managment:
+  //
+  void garbageCollect() override;
+
+  // Generate a (possibly simplified) DIMACS file:
+  //
 #if 0
     void    toDimacs  (const char* file, const vec<Lit>& assumps);
     void    toDimacs  (const char* file);