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>

6 files changed, 793 insertions, 591 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);
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 6e5dc664e..6abaa30c6 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -129,75 +129,93 @@ static DoubleOption  opt_garbage_frac      (_cat, "gc-frac",     "The fraction o
 CRef Solver::TCRef_Undef = CRef_Undef;
 CRef Solver::TCRef_Lazy = CRef_Lazy;
 
-class ScopedBool {
-  bool& watch;
-  bool oldValue;
-public:
-  ScopedBool(bool& watch, bool newValue)
-  : watch(watch), oldValue(watch) {
+class ScopedBool
+{
+  bool& d_watch;
+  bool d_oldValue;
+
+ public:
+  ScopedBool(bool& watch, bool newValue) : d_watch(watch), d_oldValue(watch)
+  {
     watch = newValue;
   }
-  ~ScopedBool() {
-    watch = oldValue;
-  }
+  ~ScopedBool() { d_watch = d_oldValue; }
 };
 
-
 //=================================================================================================
 // Constructor/Destructor:
 
-Solver::Solver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* context, bool enable_incremental) :
-    proxy(proxy)
-  , context(context)
-  , assertionLevel(0)
-  , enable_incremental(enable_incremental)
-  , minisat_busy(false)
-    // Parameters (user settable):
-    //
-  , 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(1), 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), resources_consumed(0)
-  , dec_vars(0), clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0)
-
-  , 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   (!enable_incremental)
-
-    // Resource constraints:
-    //
-  , conflict_budget    (-1)
-  , propagation_budget (-1)
-  , asynch_interrupt   (false)
+Solver::Solver(CVC4::prop::TheoryProxy* proxy,
+               CVC4::context::Context* context,
+               bool enable_incremental)
+    : d_proxy(proxy),
+      d_context(context),
+      assertionLevel(0),
+      d_enable_incremental(enable_incremental),
+      minisat_busy(false)
+      // Parameters (user settable):
+      //
+      ,
+      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(1),
+      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),
+      resources_consumed(0),
+      dec_vars(0),
+      clauses_literals(0),
+      learnts_literals(0),
+      max_literals(0),
+      tot_literals(0)
+
+      ,
+      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(!enable_incremental)
+
+      // Resource constraints:
+      //
+      ,
+      conflict_budget(-1),
+      propagation_budget(-1),
+      asynch_interrupt(false)
 {
   PROOF(ProofManager::currentPM()->initSatProof(this);)
 
@@ -257,7 +275,7 @@ Var Solver::newVar(bool sign, bool dvar, bool isTheoryAtom, bool preRegister, bo
 }
 
 void Solver::resizeVars(int newSize) {
-  assert(enable_incremental);
+  assert(d_enable_incremental);
   assert(decisionLevel() == 0);
   Assert(newSize >= 2) << "always keep true/false";
   if (newSize < nVars()) {
@@ -288,7 +306,7 @@ CRef Solver::reason(Var x) {
   Debug("pf::sat") << "Solver::reason(" << x << ")" << std::endl;
 
   // If we already have a reason, just return it
-  if (vardata[x].reason != CRef_Lazy) return vardata[x].reason;
+  if (vardata[x].d_reason != CRef_Lazy) return vardata[x].d_reason;
 
   // What's the literal we are trying to explain
   Lit l = mkLit(x, value(x) != l_True);
@@ -296,7 +314,8 @@ CRef Solver::reason(Var x) {
   // Get the explanation from the theory
   SatClause explanation_cl;
   // FIXME: at some point return a tag with the theory that spawned you
-  proxy->explainPropagation(MinisatSatSolver::toSatLiteral(l), explanation_cl);
+  d_proxy->explainPropagation(MinisatSatSolver::toSatLiteral(l),
+                              explanation_cl);
   vec<Lit> explanation;
   MinisatSatSolver::toMinisatClause(explanation_cl, explanation);
 
@@ -352,9 +371,9 @@ CRef Solver::reason(Var x) {
       explanation.shrink(i - j);
 
       Debug("pf::sat") << "Solver::reason: explanation = ";
-      for (int i = 0; i < explanation.size(); ++i)
+      for (int k = 0; k < explanation.size(); ++k)
       {
-        Debug("pf::sat") << explanation[i] << " ";
+        Debug("pf::sat") << explanation[k] << " ";
       }
       Debug("pf::sat") << std::endl;
 
@@ -578,7 +597,7 @@ void Solver::removeClause(CRef cr) {
     Debug("minisat::remove-clause") << "Solver::removeClause(" << c << ")" << std::endl;
     detachClause(cr);
     // Don't leave pointers to free'd memory!
-    if (locked(c)) vardata[var(c[0])].reason = CRef_Undef;
+    if (locked(c)) vardata[var(c[0])].d_reason = CRef_Undef;
     c.mark(1);
     ca.free(cr);
 }
@@ -599,15 +618,15 @@ void Solver::cancelUntil(int level) {
     if (decisionLevel() > level){
         // Pop the SMT context
         for (int l = trail_lim.size() - level; l > 0; --l) {
-          context->pop();
+          d_context->pop();
           if(Dump.isOn("state")) {
-            proxy->dumpStatePop();
+            d_proxy->dumpStatePop();
           }
         }
         for (int c = trail.size()-1; c >= trail_lim[level]; c--){
             Var      x  = var(trail[c]);
             assigns [x] = l_Undef;
-            vardata[x].trail_index = -1;
+            vardata[x].d_trail_index = -1;
             if ((phase_saving > 1 ||
                  ((phase_saving == 1) && c > trail_lim.last())
                  ) && ((polarity[x] & 0x2) == 0)) {
@@ -622,9 +641,13 @@ void Solver::cancelUntil(int level) {
 
         // Register variables that have not been registered yet
         int currentLevel = decisionLevel();
-        for(int i = variables_to_register.size() - 1; i >= 0 && variables_to_register[i].level > currentLevel; --i) {
-          variables_to_register[i].level = currentLevel;
-          proxy->variableNotify(MinisatSatSolver::toSatVariable(variables_to_register[i].var));
+        for (int i = variables_to_register.size() - 1;
+             i >= 0 && variables_to_register[i].d_level > currentLevel;
+             --i)
+        {
+          variables_to_register[i].d_level = currentLevel;
+          d_proxy->variableNotify(
+              MinisatSatSolver::toSatVariable(variables_to_register[i].d_var));
         }
     }
 }
@@ -641,7 +664,7 @@ Lit Solver::pickBranchLit()
 
 #ifdef CVC4_REPLAY
 
-    nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextReplayDecision());
+    nextLit = MinisatSatSolver::toMinisatLit(d_proxy->getNextReplayDecision());
 
     if (nextLit != lit_Undef) {
       return nextLit;
@@ -649,7 +672,8 @@ Lit Solver::pickBranchLit()
 #endif /* CVC4_REPLAY */
 
     // Theory requests
-    nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextTheoryDecisionRequest());
+    nextLit =
+        MinisatSatSolver::toMinisatLit(d_proxy->getNextTheoryDecisionRequest());
     while (nextLit != lit_Undef) {
       if(value(var(nextLit)) == l_Undef) {
         Debug("theoryDecision")
@@ -660,14 +684,15 @@ Lit Solver::pickBranchLit()
         // org-mode tracing -- theory decision
         if (Trace.isOn("dtview"))
         {
-          dtviewDecisionHelper(context->getLevel(),
-                               proxy->getNode(MinisatSatSolver::toSatLiteral(nextLit)),
-                               "THEORY");
+          dtviewDecisionHelper(
+              d_context->getLevel(),
+              d_proxy->getNode(MinisatSatSolver::toSatLiteral(nextLit)),
+              "THEORY");
         }
 
         if (Trace.isOn("dtview::prop"))
         {
-          dtviewPropagationHeaderHelper(context->getLevel());
+          dtviewPropagationHeaderHelper(d_context->getLevel());
         }
 
         return nextLit;
@@ -676,7 +701,8 @@ Lit Solver::pickBranchLit()
             << "getNextTheoryDecisionRequest(): would decide on " << nextLit
             << " but it already has an assignment" << std::endl;
       }
-      nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextTheoryDecisionRequest());
+      nextLit = MinisatSatSolver::toMinisatLit(
+          d_proxy->getNextTheoryDecisionRequest());
     }
     Debug("theoryDecision")
         << "getNextTheoryDecisionRequest(): decide on another literal"
@@ -684,7 +710,8 @@ Lit Solver::pickBranchLit()
 
     // DE requests
     bool stopSearch = false;
-    nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextDecisionEngineRequest(stopSearch));
+    nextLit = MinisatSatSolver::toMinisatLit(
+        d_proxy->getNextDecisionEngineRequest(stopSearch));
     if(stopSearch) {
       return lit_Undef;
     }
@@ -700,14 +727,15 @@ Lit Solver::pickBranchLit()
       // org-mode tracing -- decision engine decision
       if (Trace.isOn("dtview"))
       {
-        dtviewDecisionHelper(context->getLevel(),
-                             proxy->getNode(MinisatSatSolver::toSatLiteral(nextLit)),
-                             "DE");
+        dtviewDecisionHelper(
+            d_context->getLevel(),
+            d_proxy->getNode(MinisatSatSolver::toSatLiteral(nextLit)),
+            "DE");
       }
 
       if (Trace.isOn("dtview::prop"))
       {
-        dtviewPropagationHeaderHelper(context->getLevel());
+        dtviewPropagationHeaderHelper(d_context->getLevel());
       }
 
       return nextLit;
@@ -732,7 +760,9 @@ Lit Solver::pickBranchLit()
 
         if(!decision[next]) continue;
         // Check with decision engine about relevancy
-        if(proxy->isDecisionRelevant(MinisatSatSolver::toSatVariable(next)) == false ) {
+        if (d_proxy->isDecisionRelevant(MinisatSatSolver::toSatVariable(next))
+            == false)
+        {
           next = var_Undef;
         }
     }
@@ -742,8 +772,8 @@ Lit Solver::pickBranchLit()
     } else {
       decisions++;
       // Check with decision engine if it can tell polarity
-      lbool dec_pol = MinisatSatSolver::toMinisatlbool
-        (proxy->getDecisionPolarity(MinisatSatSolver::toSatVariable(next)));
+      lbool dec_pol = MinisatSatSolver::toMinisatlbool(
+          d_proxy->getDecisionPolarity(MinisatSatSolver::toSatVariable(next)));
       Lit decisionLit;
       if(dec_pol != l_Undef) {
         Assert(dec_pol == l_True || dec_pol == l_False);
@@ -759,14 +789,15 @@ Lit Solver::pickBranchLit()
       // org-mode tracing -- decision engine decision
       if (Trace.isOn("dtview"))
       {
-        dtviewDecisionHelper(context->getLevel(),
-                             proxy->getNode(MinisatSatSolver::toSatLiteral(decisionLit)),
-                             "DE");
+        dtviewDecisionHelper(
+            d_context->getLevel(),
+            d_proxy->getNode(MinisatSatSolver::toSatLiteral(decisionLit)),
+            "DE");
       }
 
       if (Trace.isOn("dtview::prop"))
       {
-        dtviewPropagationHeaderHelper(context->getLevel());
+        dtviewPropagationHeaderHelper(d_context->getLevel());
       }
 
       return decisionLit;
@@ -920,17 +951,18 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
     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;
+        for (int k = 2; k < out_learnt.size(); k++)
+          if (level(var(out_learnt[k])) > level(var(out_learnt[max_i])))
+            max_i = k;
         // Swap-in this literal at index 1:
-        Lit p             = out_learnt[max_i];
+        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 k = 0; k < analyze_toclear.size(); k++)
+      seen[var(analyze_toclear[k])] = 0;  // ('seen[]' is now cleared)
 
     // Return the maximal resolution level
     return max_resolution_level;
@@ -953,19 +985,24 @@ bool Solver::litRedundant(Lit p, uint32_t abstract_levels)
         // Since calling reason might relocate to resize, c is not necesserily the right reference, we must
         // use the allocator each time
         for (int i = 1; i < c_size; i++){
-            Lit p  = ca[c_reason][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 = ca[c_reason][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;
+            }
+          }
         }
     }
 
@@ -1022,7 +1059,7 @@ void Solver::uncheckedEnqueue(Lit p, CRef from)
     trail.push_(p);
     if (theory[var(p)]) {
       // Enqueue to the theory
-      proxy->enqueueTheoryLiteral(MinisatSatSolver::toSatLiteral(p));
+      d_proxy->enqueueTheoryLiteral(MinisatSatSolver::toSatLiteral(p));
     }
 }
 
@@ -1057,7 +1094,7 @@ CRef Solver::propagate(TheoryCheckType type)
         confl = updateLemmas();
         return confl;
       } else {
-        recheck = proxy->theoryNeedCheck();
+        recheck = d_proxy->theoryNeedCheck();
         return confl;
       }
     }
@@ -1087,7 +1124,7 @@ CRef Solver::propagate(TheoryCheckType type)
           {
             if (confl != CRef_Undef)
             {
-              dtviewPropConflictHelper(decisionLevel(), ca[confl], proxy);
+              dtviewPropConflictHelper(decisionLevel(), ca[confl], d_proxy);
             }
           }
           // Even though in conflict, we still need to discharge the lemmas
@@ -1116,7 +1153,7 @@ void Solver::propagateTheory() {
   SatClause propagatedLiteralsClause;
   // Doesn't actually call propagate(); that's done in theoryCheck() now that combination
   // is online.  This just incorporates those propagations previously discovered.
-  proxy->theoryPropagate(propagatedLiteralsClause);
+  d_proxy->theoryPropagate(propagatedLiteralsClause);
 
   vec<Lit> propagatedLiterals;
   MinisatSatSolver::toMinisatClause(propagatedLiteralsClause, propagatedLiterals);
@@ -1133,7 +1170,8 @@ void Solver::propagateTheory() {
       if (value(p) == l_False) {
         Debug("minisat") << "Conflict in theory propagation" << std::endl;
         SatClause explanation_cl;
-        proxy->explainPropagation(MinisatSatSolver::toSatLiteral(p), explanation_cl);
+        d_proxy->explainPropagation(MinisatSatSolver::toSatLiteral(p),
+                                    explanation_cl);
         vec<Lit> explanation;
         MinisatSatSolver::toMinisatClause(explanation_cl, explanation);
         ClauseId id; // FIXME: mark it as explanation here somehow?
@@ -1158,7 +1196,7 @@ void Solver::propagateTheory() {
 |________________________________________________________________________________________________@*/
 void Solver::theoryCheck(CVC4::theory::Theory::Effort effort)
 {
-  proxy->theoryCheck(effort);
+  d_proxy->theoryCheck(effort);
 }
 
 /*_________________________________________________________________________________________________
@@ -1187,7 +1225,7 @@ CRef Solver::propagateBool()
         // if propagation tracing enabled, print boolean propagation
         if (Trace.isOn("dtview::prop"))
         {
-          dtviewBoolPropagationHelper(decisionLevel(), p, proxy);
+          dtviewBoolPropagationHelper(decisionLevel(), p, d_proxy);
         }
 
         for (i = j = (Watcher*)ws, end = i + ws.size();  i != end;){
@@ -1443,7 +1481,7 @@ lbool Solver::search(int nof_conflicts)
 
 	    // If this was a final check, we are satisfiable
             if (check_type == CHECK_FINAL) {
-	      bool decisionEngineDone = proxy->isDecisionEngineDone();
+              bool decisionEngineDone = d_proxy->isDecisionEngineDone();
               // Unless a lemma has added more stuff to the queues
               if (!decisionEngineDone  &&
 		  (!order_heap.empty() || qhead < trail.size()) ) {
@@ -1468,7 +1506,7 @@ lbool Solver::search(int nof_conflicts)
               cancelUntil(0);
               // [mdeters] notify theory engine of restarts for deferred
               // theory processing
-              proxy->notifyRestart();
+              d_proxy->notifyRestart();
               return l_Undef;
             }
 
@@ -1490,8 +1528,8 @@ lbool Solver::search(int nof_conflicts)
                     // Dummy decision level:
                     newDecisionLevel();
                 } else if (value(p) == l_False) {
-                    analyzeFinal(~p, conflict);
-                    return l_False;
+                  analyzeFinal(~p, d_conflict);
+                  return l_False;
                 } else {
                     next = p;
                     break;
@@ -1511,7 +1549,7 @@ lbool Solver::search(int nof_conflicts)
                 }
 
 #ifdef CVC4_REPLAY
-                proxy->logDecision(MinisatSatSolver::toSatLiteral(next));
+                d_proxy->logDecision(MinisatSatSolver::toSatLiteral(next));
 #endif /* CVC4_REPLAY */
             }
 
@@ -1575,7 +1613,7 @@ lbool Solver::solve_()
     assert(decisionLevel() == 0);
 
     model.clear();
-    conflict.clear();
+    d_conflict.clear();
     if (!ok){
       minisat_busy = false;
       return l_False;
@@ -1619,8 +1657,9 @@ lbool Solver::solve_()
           model[i] = value(i);
           Debug("minisat") << i << " = " << model[i] << std::endl;
         }
-    }else if (status == l_False && conflict.size() == 0)
-        ok = false;
+    }
+    else if (status == l_False && d_conflict.size() == 0)
+      ok = false;
 
     return status;
 }
@@ -1728,7 +1767,7 @@ void Solver::relocAll(ClauseAllocator& to)
 
         if (hasReasonClause(v) && (ca[reason(v)].reloced() || locked(ca[reason(v)])))
           ca.reloc(
-              vardata[v].reason, to, NULLPROOF(ProofManager::getSatProof()));
+              vardata[v].d_reason, to, NULLPROOF(ProofManager::getSatProof()));
     }
     // All learnt:
     //
@@ -1761,7 +1800,7 @@ void Solver::garbageCollect()
 
 void Solver::push()
 {
-  assert(enable_incremental);
+  assert(d_enable_incremental);
   assert(decisionLevel() == 0);
 
   ++assertionLevel;
@@ -1769,14 +1808,14 @@ void Solver::push()
   trail_ok.push(ok);
   assigns_lim.push(assigns.size());
 
-  context->push(); // SAT context for CVC4
+  d_context->push();  // SAT context for CVC4
 
   Debug("minisat") << "MINISAT PUSH assertionLevel is " << assertionLevel << ", trail.size is " << trail.size() << std::endl;
 }
 
 void Solver::pop()
 {
-  assert(enable_incremental);
+  assert(d_enable_incremental);
 
   assert(decisionLevel() == 0);
 
@@ -1804,7 +1843,7 @@ void Solver::pop()
   removeClausesAboveLevel(clauses_removable, assertionLevel);
 
   // Pop the SAT context to notify everyone
-  context->pop(); // SAT context for CVC4
+  d_context->pop();  // SAT context for CVC4
 
   // Pop the created variables
   resizeVars(assigns_lim.last());
@@ -1821,7 +1860,7 @@ CRef Solver::updateLemmas() {
   Debug("minisat::lemmas") << "Solver::updateLemmas() begin" << std::endl;
 
   // Avoid adding lemmas indefinitely without resource-out
-  proxy->spendResource(ResourceManager::Resource::LemmaStep);
+  d_proxy->spendResource(ResourceManager::Resource::LemmaStep);
 
   CRef conflict = CRef_Undef;
 
@@ -1881,11 +1920,11 @@ CRef Solver::updateLemmas() {
   PROOF(Assert(lemmas.size() == (int)lemmas_cnf_assertion.size()););
 
   // Attach all the clauses and enqueue all the propagations
-  for (int i = 0; i < lemmas.size(); ++ i)
+  for (int j = 0; j < lemmas.size(); ++j)
   {
     // The current lemma
-    vec<Lit>& lemma = lemmas[i];
-    bool removable = lemmas_removable[i];
+    vec<Lit>& lemma = lemmas[j];
+    bool removable = lemmas_removable[j];
 
     // Attach it if non-unit
     CRef lemma_ref = CRef_Undef;
@@ -1895,22 +1934,22 @@ CRef Solver::updateLemmas() {
       if (removable && !assertionLevelOnly())
       {
         clauseLevel = 0;
-        for (int i = 0; i < lemma.size(); ++ i) {
-          clauseLevel = std::max(clauseLevel, intro_level(var(lemma[i])));
+        for (int k = 0; k < lemma.size(); ++k)
+        {
+          clauseLevel = std::max(clauseLevel, intro_level(var(lemma[k])));
         }
       }
 
       lemma_ref = ca.alloc(clauseLevel, lemma, removable);
-      PROOF
-        (
-         TNode cnf_assertion = lemmas_cnf_assertion[i].first;
-         TNode cnf_def = lemmas_cnf_assertion[i].second;
-
-         Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (2)" << std::endl;
-         ClauseId id = ProofManager::getSatProof()->registerClause(lemma_ref, THEORY_LEMMA);
-         ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion);
-         ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def);
-         );
+      PROOF(TNode cnf_assertion = lemmas_cnf_assertion[j].first;
+            TNode cnf_def = lemmas_cnf_assertion[j].second;
+
+            Debug("pf::sat")
+            << "Minisat::Solver registering a THEORY_LEMMA (2)" << std::endl;
+            ClauseId id = ProofManager::getSatProof()->registerClause(
+                lemma_ref, THEORY_LEMMA);
+            ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion);
+            ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def););
       if (removable) {
         clauses_removable.push(lemma_ref);
       } else {
@@ -1920,8 +1959,8 @@ CRef Solver::updateLemmas() {
     } else {
       PROOF
         (
-         Node cnf_assertion = lemmas_cnf_assertion[i].first;
-         Node cnf_def = lemmas_cnf_assertion[i].second;
+         Node cnf_assertion = lemmas_cnf_assertion[j].first;
+         Node cnf_def = lemmas_cnf_assertion[j].second;
 
          Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (3)" << std::endl;
          ClauseId id = ProofManager::getSatProof()->registerUnitClause(lemma[0], THEORY_LEMMA);
@@ -1993,10 +2032,10 @@ void ClauseAllocator::reloc(CRef& cr,
 
 inline bool Solver::withinBudget(ResourceManager::Resource r) const
 {
-  Assert(proxy);
+  Assert(d_proxy);
   // spendResource sets async_interrupt or throws UnsafeInterruptException
   // depending on whether hard-limit is enabled
-  proxy->spendResource(r);
+  d_proxy->spendResource(r);
 
   bool within_budget =
       !asynch_interrupt
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 0cec30d24..508947456 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -66,14 +66,13 @@ public:
   typedef Clause TClause; 
   typedef CRef TCRef;
   typedef vec<Lit> TLitVec;
-  
-protected:
 
+ protected:
   /** The pointer to the proxy that provides interfaces to the SMT engine */
-  CVC4::prop::TheoryProxy* proxy;
+  CVC4::prop::TheoryProxy* d_proxy;
 
   /** The context from the SMT solver */
-  CVC4::context::Context* context;
+  CVC4::context::Context* d_context;
 
   /** The current assertion level (user) */
   int assertionLevel;
@@ -84,21 +83,22 @@ protected:
   /** Variable representing false */
   Var varFalse;
 
-public:
+ public:
   /** Returns the current user assertion level */
   int getAssertionLevel() const { return assertionLevel; }
-protected:
+
+ protected:
   /** Do we allow incremental solving */
-  bool enable_incremental;
+  bool d_enable_incremental;
 
   /** Literals propagated by lemmas */
-  vec< vec<Lit> > lemmas;
+  vec<vec<Lit> > lemmas;
 
   /** Is the lemma removable */
   vec<bool> lemmas_removable;
 
   /** Nodes being converted to CNF */
-  std::vector< std::pair<CVC4::Node, CVC4::Node > >lemmas_cnf_assertion;
+  std::vector<std::pair<CVC4::Node, CVC4::Node> > lemmas_cnf_assertion;
 
   /** Do a another check if FULL_EFFORT was the last one */
   bool recheck;
@@ -110,11 +110,11 @@ protected:
   bool minisat_busy;
 
   // Information about registration of variables
-  struct VarIntroInfo {
-    Var var;
-    int level;
-    VarIntroInfo(Var var, int level)
-    : var(var), level(level) {}
+  struct VarIntroInfo
+  {
+    Var d_var;
+    int d_level;
+    VarIntroInfo(Var var, int level) : d_var(var), d_level(level) {}
   };
 
   /** Variables to re-register with theory solvers on backtracks */
@@ -138,30 +138,38 @@ public:
 
     // Less than for literals in a lemma
     struct lemma_lt {
-        Solver& solver;
-        lemma_lt(Solver& solver) : solver(solver) {}
-        bool operator () (Lit x, Lit y) {
-          lbool x_value = solver.value(x);
-          lbool y_value = solver.value(y);
-          // Two unassigned literals are sorted arbitrarily
-          if (x_value == l_Undef && y_value == l_Undef) {
-            return x < y;
+      Solver& d_solver;
+      lemma_lt(Solver& solver) : d_solver(solver) {}
+      bool operator()(Lit x, Lit 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;
+        }
+        // Unassigned literals are put to front
+        if (x_value == l_Undef) return true;
+        if (y_value == l_Undef) return false;
+        // Literals of the same value are sorted by decreasing levels
+        if (x_value == y_value)
+        {
+          return d_solver.trail_index(var(x)) > d_solver.trail_index(var(y));
+        }
+        else
+        {
+          // True literals go up front
+          if (x_value == l_True)
+          {
+            return true;
           }
-          // Unassigned literals are put to front
-          if (x_value == l_Undef) return true;
-          if (y_value == l_Undef) return false;
-          // Literals of the same value are sorted by decreasing levels
-          if (x_value == y_value) {
-            return solver.trail_index(var(x)) > solver.trail_index(var(y));
-          } else {
-            // True literals go up front
-            if (x_value == l_True) {
-              return true;
-            } else {
-              return false;
-            }
+          else
+          {
+            return false;
           }
         }
+      }
     };
 
 
@@ -246,8 +254,9 @@ public:
     // Extra results: (read-only member variable)
     //
     vec<lbool> model;             // If problem is satisfiable, this vector contains the model (if any).
-    vec<Lit>   conflict;          // If problem is unsatisfiable (possibly under assumptions),
-                                  // this vector represent the final conflict clause expressed in the assumptions.
+    vec<Lit> d_conflict;          // If problem is unsatisfiable (possibly under
+                          // assumptions), this vector represent the final
+                          // conflict clause expressed in the assumptions.
 
     // Mode of operation:
     //
@@ -282,22 +291,26 @@ protected:
     //
     struct VarData {
       // Reason for the literal being in the trail
-      CRef reason;
+      CRef d_reason;
       // Sat level when the literal was added to the trail
-      int level;
+      int d_level;
       // User level when the literal was added to the trail
-      int user_level;
+      int d_user_level;
       // User level at which this literal was introduced
-      int intro_level;
+      int d_intro_level;
       // The index in the trail
-      int trail_index;
-
-      VarData(CRef reason, int level, int user_level, int intro_level, int trail_index)
-      : reason(reason)
-      , level(level)
-      , user_level(user_level)
-      , intro_level(intro_level)
-      , trail_index(trail_index)
+      int d_trail_index;
+
+      VarData(CRef reason,
+              int level,
+              int user_level,
+              int intro_level,
+              int trail_index)
+          : d_reason(reason),
+            d_level(level),
+            d_user_level(user_level),
+            d_intro_level(intro_level),
+            d_trail_index(trail_index)
       {}
     };
 
@@ -464,21 +477,53 @@ public:
 //=================================================================================================
 // Implementation of inline methods:
 
-inline bool Solver::hasReasonClause(Var x) const { return vardata[x].reason != CRef_Undef && vardata[x].reason != CRef_Lazy; }
+inline bool Solver::hasReasonClause(Var x) const
+{
+  return vardata[x].d_reason != CRef_Undef && vardata[x].d_reason != CRef_Lazy;
+}
 
-inline bool Solver::isPropagated(Var x) const { return vardata[x].reason != CRef_Undef; }
+inline bool Solver::isPropagated(Var x) const
+{
+  return vardata[x].d_reason != CRef_Undef;
+}
 
-inline bool Solver::isPropagatedBy(Var x, const Clause& c) const { return vardata[x].reason != CRef_Undef && vardata[x].reason != CRef_Lazy && ca.lea(vardata[var(c[0])].reason) == &c; }
+inline bool Solver::isPropagatedBy(Var x, const Clause& c) const
+{
+  return vardata[x].d_reason != CRef_Undef && vardata[x].d_reason != CRef_Lazy
+         && ca.lea(vardata[var(c[0])].d_reason) == &c;
+}
 
-inline bool Solver::isDecision(Var x) const { Debug("minisat") << "var " << x << " is a decision iff " << (vardata[x].reason == CRef_Undef) << " && " << level(x) << " > 0" << std::endl; return vardata[x].reason == CRef_Undef && level(x) > 0; }
+inline bool Solver::isDecision(Var x) const
+{
+  Debug("minisat") << "var " << x << " is a decision iff "
+                   << (vardata[x].d_reason == CRef_Undef) << " && " << level(x)
+                   << " > 0" << std::endl;
+  return vardata[x].d_reason == CRef_Undef && level(x) > 0;
+}
 
-inline int  Solver::level (Var x) const { assert(x < vardata.size()); return vardata[x].level; }
+inline int Solver::level(Var x) const
+{
+  assert(x < vardata.size());
+  return vardata[x].d_level;
+}
 
-inline int  Solver::user_level(Var x) const { assert(x < vardata.size()); return vardata[x].user_level; }
+inline int Solver::user_level(Var x) const
+{
+  assert(x < vardata.size());
+  return vardata[x].d_user_level;
+}
 
-inline int  Solver::intro_level(Var x) const { assert(x < vardata.size()); return vardata[x].intro_level; }
+inline int Solver::intro_level(Var x) const
+{
+  assert(x < vardata.size());
+  return vardata[x].d_intro_level;
+}
 
-inline int  Solver::trail_index(Var x) const { assert(x < vardata.size()); return vardata[x].trail_index; }
+inline int Solver::trail_index(Var x) const
+{
+  assert(x < vardata.size());
+  return vardata[x].d_trail_index;
+}
 
 inline void Solver::insertVarOrder(Var x) {
     assert(x < vardata.size());
@@ -522,7 +567,16 @@ inline bool     Solver::addClause       (Lit p, Lit q, bool removable, ClauseId&
 inline bool     Solver::addClause       (Lit p, Lit q, Lit r, bool removable, ClauseId& id)
                                                                 { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable, id); }
 inline bool     Solver::locked          (const Clause& c) const { return value(c[0]) == l_True && isPropagatedBy(var(c[0]), c); }
-inline void     Solver::newDecisionLevel()                      { trail_lim.push(trail.size()); flipped.push(false); context->push(); if(Dump.isOn("state")) { Dump("state") << CVC4::PushCommand(); } }
+inline void Solver::newDecisionLevel()
+{
+  trail_lim.push(trail.size());
+  flipped.push(false);
+  d_context->push();
+  if (Dump.isOn("state"))
+  {
+    Dump("state") << CVC4::PushCommand();
+  }
+}
 
 inline int      Solver::decisionLevel ()      const   { return trail_lim.size(); }
 inline uint32_t Solver::abstractLevel (Var x) const   { return 1 << (level(x) & 31); }