Use Assert instead of assert. (#6095)

This commit replaces all uses of assert with Assert from base/check.h to ensure that all assertions get checked in production builds with enabled assertions.

11 files changed, 533 insertions, 395 deletions

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index d597ac934..b36fe9517 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -25,6 +25,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <iostream>
 #include <unordered_set>
 
+#include "base/check.h"
 #include "base/output.h"
 #include "options/main_options.h"
 #include "options/prop_options.h"
@@ -292,8 +293,8 @@ Var Solver::newVar(bool sign, bool dvar, bool isTheoryAtom, bool preRegister, bo
 }
 
 void Solver::resizeVars(int newSize) {
-  assert(d_enable_incremental);
-  assert(decisionLevel() == 0);
+  Assert(d_enable_incremental);
+  Assert(decisionLevel() == 0);
   Assert(newSize >= 2) << "always keep true/false";
   if (newSize < nVars()) {
     int shrinkSize = nVars() - newSize;
@@ -313,7 +314,7 @@ void Solver::resizeVars(int newSize) {
 
   if (Debug.isOn("minisat::pop")) {
     for (int i = 0; i < trail.size(); ++ i) {
-      assert(var(trail[i]) < nVars());
+      Assert(var(trail[i]) < nVars());
     }
   }
 }
@@ -523,7 +524,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
         id = ClauseIdUndef;
       }
     } else {
-      assert(decisionLevel() == 0);
+      Assert(decisionLevel() == 0);
 
       // If all false, we're in conflict
       if (ps.size() == falseLiteralsCount) {
@@ -608,7 +609,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
       // Check if it propagates
       if (ps.size() == falseLiteralsCount + 1) {
         if(assigns[var(ps[0])] == l_Undef) {
-          assert(assigns[var(ps[0])] != l_False);
+          Assert(assigns[var(ps[0])] != l_False);
           uncheckedEnqueue(ps[0], cr);
           Debug("cores") << "i'm registering a unit clause, maybe input"
                          << std::endl;
@@ -714,7 +715,7 @@ void Solver::detachClause(CRef cr, bool strict) {
 
       Debug("minisat") << "\n";
     }
-    assert(c.size() > 1);
+    Assert(c.size() > 1);
     if (options::unsatCores() && !isProofEnabled())
     {
       ProofManager::getSatProof()->markDeleted(cr);
@@ -1006,18 +1007,18 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
       d_pfManager->startResChain(ca[confl]);
     }
     do{
-        assert(confl != CRef_Undef); // (otherwise should be UIP)
+      Assert(confl != CRef_Undef);  // (otherwise should be UIP)
 
-        {
-          // ! IMPORTANT !
-          // It is not safe to use c after this block of code because
-          // resolveOutUnit() below may lead to clauses being allocated, which
-          // in turn may lead to reallocations that invalidate c.
-          Clause& c = ca[confl];
-          max_resolution_level = std::max(max_resolution_level, c.level());
-
-          if (c.removable()) claBumpActivity(c);
-        }
+      {
+        // ! IMPORTANT !
+        // It is not safe to use c after this block of code because
+        // resolveOutUnit() below may lead to clauses being allocated, which
+        // in turn may lead to reallocations that invalidate c.
+        Clause& c = ca[confl];
+        max_resolution_level = std::max(max_resolution_level, c.level());
+
+        if (c.removable()) claBumpActivity(c);
+      }
 
         if (Trace.isOn("pf::sat"))
         {
@@ -1196,7 +1197,7 @@ bool Solver::litRedundant(Lit p, uint32_t abstract_levels)
     int top = analyze_toclear.size();
     while (analyze_stack.size() > 0){
         CRef c_reason = reason(var(analyze_stack.last()));
-        assert(c_reason != CRef_Undef);
+        Assert(c_reason != CRef_Undef);
         Clause& c = ca[c_reason];
         int c_size = c.size();
         analyze_stack.pop();
@@ -1252,8 +1253,8 @@ void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict)
         Var x = var(trail[i]);
         if (seen[x]){
             if (reason(x) == CRef_Undef){
-                assert(level(x) > 0);
-                out_conflict.push(~trail[i]);
+              Assert(level(x) > 0);
+              out_conflict.push(~trail[i]);
             }else{
                 Clause& c = ca[reason(x)];
                 for (int j = 1; j < c.size(); j++)
@@ -1292,8 +1293,8 @@ void Solver::uncheckedEnqueue(Lit p, CRef from)
     }
     Debug("minisat") << "\n";
   }
-  assert(value(p) == l_Undef);
-  assert(var(p) < nVars());
+  Assert(value(p) == l_Undef);
+  Assert(var(p) < nVars());
   assigns[var(p)] = lbool(!sign(p));
   vardata[var(p)] = VarData(
       from, decisionLevel(), assertionLevel, intro_level(var(p)), trail.size());
@@ -1484,7 +1485,7 @@ CRef Solver::propagateBool()
             Lit      false_lit = ~p;
             if (c[0] == false_lit)
                 c[0] = c[1], c[1] = false_lit;
-            assert(c[1] == false_lit);
+            Assert(c[1] == false_lit);
             i++;
 
             // If 0th watch is true, then clause is already satisfied.
@@ -1584,8 +1585,8 @@ void Solver::removeClausesAboveLevel(vec<CRef>& cs, int level)
     for (i = j = 0; i < cs.size(); i++){
         Clause& c = ca[cs[i]];
         if (c.level() > level) {
-            assert(!locked(c));
-            removeClause(cs[i]);
+          Assert(!locked(c));
+          removeClause(cs[i]);
         } else {
             cs[j++] = cs[i];
         }
@@ -1613,25 +1614,25 @@ void Solver::rebuildOrderHeap()
 |________________________________________________________________________________________________@*/
 bool Solver::simplify()
 {
-    assert(decisionLevel() == 0);
+  Assert(decisionLevel() == 0);
 
-    if (!ok || propagate(CHECK_WITHOUT_THEORY) != CRef_Undef)
-        return ok = false;
+  if (!ok || propagate(CHECK_WITHOUT_THEORY) != CRef_Undef) return ok = false;
 
-    if (nAssigns() == simpDB_assigns || (simpDB_props > 0))
-        return true;
+  if (nAssigns() == simpDB_assigns || (simpDB_props > 0)) return true;
 
-    // Remove satisfied clauses:
-    removeSatisfied(clauses_removable);
-    if (remove_satisfied)        // Can be turned off.
-        removeSatisfied(clauses_persistent);
-    checkGarbage();
-    rebuildOrderHeap();
+  // Remove satisfied clauses:
+  removeSatisfied(clauses_removable);
+  if (remove_satisfied)  // Can be turned off.
+    removeSatisfied(clauses_persistent);
+  checkGarbage();
+  rebuildOrderHeap();
 
-    simpDB_assigns = nAssigns();
-    simpDB_props   = clauses_literals + learnts_literals;   // (shouldn't depend on stats really, but it will do for now)
+  simpDB_assigns = nAssigns();
+  simpDB_props =
+      clauses_literals + learnts_literals;  // (shouldn't depend on stats
+                                            // really, but it will do for now)
 
-    return true;
+  return true;
 }
 
 
@@ -1650,186 +1651,209 @@ bool Solver::simplify()
 |________________________________________________________________________________________________@*/
 lbool Solver::search(int nof_conflicts)
 {
-    assert(ok);
-    int         backtrack_level;
-    int         conflictC = 0;
-    vec<Lit>    learnt_clause;
-    starts++;
-
-    TheoryCheckType check_type = CHECK_WITH_THEORY;
-    for (;;) {
-
-        // Propagate and call the theory solvers
-        CRef confl = propagate(check_type);
-        Assert(lemmas.size() == 0);
-
-        if (confl != CRef_Undef) {
+  Assert(ok);
+  int backtrack_level;
+  int conflictC = 0;
+  vec<Lit> learnt_clause;
+  starts++;
+
+  TheoryCheckType check_type = CHECK_WITH_THEORY;
+  for (;;)
+  {
+    // Propagate and call the theory solvers
+    CRef confl = propagate(check_type);
+    Assert(lemmas.size() == 0);
 
-            conflicts++; conflictC++;
+    if (confl != CRef_Undef)
+    {
+      conflicts++;
+      conflictC++;
 
-            if (decisionLevel() == 0)
-            {
-              if (options::unsatCores() && !isProofEnabled())
-              {
-                ProofManager::getSatProof()->finalizeProof(confl);
-              }
-              if (isProofEnabled())
-              {
-                if (confl == CRef_Lazy)
-                {
-                  d_pfManager->finalizeProof();
-                }
-                else
-                {
-                  d_pfManager->finalizeProof(ca[confl]);
-                }
-              }
-              return l_False;
-            }
+      if (decisionLevel() == 0)
+      {
+        if (options::unsatCores() && !isProofEnabled())
+        {
+          ProofManager::getSatProof()->finalizeProof(confl);
+        }
+        if (isProofEnabled())
+        {
+          if (confl == CRef_Lazy)
+          {
+            d_pfManager->finalizeProof();
+          }
+          else
+          {
+            d_pfManager->finalizeProof(ca[confl]);
+          }
+        }
+        return l_False;
+      }
 
-            // Analyze the conflict
-            learnt_clause.clear();
-            int max_level = analyze(confl, learnt_clause, backtrack_level);
-            cancelUntil(backtrack_level);
+      // Analyze the conflict
+      learnt_clause.clear();
+      int max_level = analyze(confl, learnt_clause, backtrack_level);
+      cancelUntil(backtrack_level);
 
-            // Assert the conflict clause and the asserting literal
-            if (learnt_clause.size() == 1) {
-                uncheckedEnqueue(learnt_clause[0]);
-                if (options::unsatCores() && !isProofEnabled())
-                {
-                  ProofManager::getSatProof()->endResChain(learnt_clause[0]);
-                }
-                if (isProofEnabled())
-                {
-                  d_pfManager->endResChain(learnt_clause[0]);
-                }
-            } else {
-              CRef cr =
-                  ca.alloc(assertionLevelOnly() ? assertionLevel : max_level,
+      // Assert the conflict clause and the asserting literal
+      if (learnt_clause.size() == 1)
+      {
+        uncheckedEnqueue(learnt_clause[0]);
+        if (options::unsatCores() && !isProofEnabled())
+        {
+          ProofManager::getSatProof()->endResChain(learnt_clause[0]);
+        }
+        if (isProofEnabled())
+        {
+          d_pfManager->endResChain(learnt_clause[0]);
+        }
+      }
+      else
+      {
+        CRef cr = ca.alloc(assertionLevelOnly() ? assertionLevel : max_level,
                            learnt_clause,
                            true);
-              clauses_removable.push(cr);
-              attachClause(cr);
-              claBumpActivity(ca[cr]);
-              uncheckedEnqueue(learnt_clause[0], cr);
-              if (options::unsatCores() && !isProofEnabled())
-              {
-                ClauseId id =
-                    ProofManager::getSatProof()->registerClause(cr, LEARNT);
-                ProofManager::getSatProof()->endResChain(id);
-              }
-              if (isProofEnabled())
-              {
-                d_pfManager->endResChain(ca[cr]);
-              }
-            }
-
-            varDecayActivity();
-            claDecayActivity();
-
-            if (--learntsize_adjust_cnt == 0){
-                learntsize_adjust_confl *= learntsize_adjust_inc;
-                learntsize_adjust_cnt    = (int)learntsize_adjust_confl;
-                max_learnts             *= learntsize_inc;
-
-                if (verbosity >= 1)
-                    printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n",
-                           (int)conflicts,
-                           (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_literals,
-                           (int)max_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progressEstimate()*100);
-            }
+        clauses_removable.push(cr);
+        attachClause(cr);
+        claBumpActivity(ca[cr]);
+        uncheckedEnqueue(learnt_clause[0], cr);
+        if (options::unsatCores() && !isProofEnabled())
+        {
+          ClauseId id = ProofManager::getSatProof()->registerClause(cr, LEARNT);
+          ProofManager::getSatProof()->endResChain(id);
+        }
+        if (isProofEnabled())
+        {
+          d_pfManager->endResChain(ca[cr]);
+        }
+      }
 
-            if (theoryConflict && options::sat_refine_conflicts()) {
-              check_type = CHECK_FINAL_FAKE;
-            } else {
-              check_type = CHECK_WITH_THEORY;
-            }
+      varDecayActivity();
+      claDecayActivity();
 
-        } else {
-          // If this was a final check, we are satisfiable
-          if (check_type == CHECK_FINAL)
-          {
-            bool decisionEngineDone = d_proxy->isDecisionEngineDone();
-            // Unless a lemma has added more stuff to the queues
-            if (!decisionEngineDone
-                && (!order_heap.empty() || qhead < trail.size()))
-            {
-              check_type = CHECK_WITH_THEORY;
-              continue;
-            }
-            else if (recheck)
-            {
-              // There some additional stuff added, so we go for another
-              // full-check
-              continue;
-            }
-            else
-            {
-              // Yes, we're truly satisfiable
-              return l_True;
-            }
-          }
-          else if (check_type == CHECK_FINAL_FAKE)
-          {
-            check_type = CHECK_WITH_THEORY;
-          }
+      if (--learntsize_adjust_cnt == 0)
+      {
+        learntsize_adjust_confl *= learntsize_adjust_inc;
+        learntsize_adjust_cnt = (int)learntsize_adjust_confl;
+        max_learnts *= learntsize_inc;
+
+        if (verbosity >= 1)
+          printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n",
+                 (int)conflicts,
+                 (int)dec_vars
+                     - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]),
+                 nClauses(),
+                 (int)clauses_literals,
+                 (int)max_learnts,
+                 nLearnts(),
+                 (double)learnts_literals / nLearnts(),
+                 progressEstimate() * 100);
+      }
 
-          if ((nof_conflicts >= 0 && conflictC >= nof_conflicts)
-              || !withinBudget(ResourceManager::Resource::SatConflictStep))
-          {
-            // Reached bound on number of conflicts:
-            progress_estimate = progressEstimate();
-            cancelUntil(0);
-            // [mdeters] notify theory engine of restarts for deferred
-            // theory processing
-            d_proxy->notifyRestart();
-            return l_Undef;
-          }
+      if (theoryConflict && options::sat_refine_conflicts())
+      {
+        check_type = CHECK_FINAL_FAKE;
+      }
+      else
+      {
+        check_type = CHECK_WITH_THEORY;
+      }
+    }
+    else
+    {
+      // If this was a final check, we are satisfiable
+      if (check_type == CHECK_FINAL)
+      {
+        bool decisionEngineDone = d_proxy->isDecisionEngineDone();
+        // Unless a lemma has added more stuff to the queues
+        if (!decisionEngineDone
+            && (!order_heap.empty() || qhead < trail.size()))
+        {
+          check_type = CHECK_WITH_THEORY;
+          continue;
+        }
+        else if (recheck)
+        {
+          // There some additional stuff added, so we go for another
+          // full-check
+          continue;
+        }
+        else
+        {
+          // Yes, we're truly satisfiable
+          return l_True;
+        }
+      }
+      else if (check_type == CHECK_FINAL_FAKE)
+      {
+        check_type = CHECK_WITH_THEORY;
+      }
 
-            // Simplify the set of problem clauses:
-            if (decisionLevel() == 0 && !simplify()) {
-                return l_False;
-            }
+      if ((nof_conflicts >= 0 && conflictC >= nof_conflicts)
+          || !withinBudget(ResourceManager::Resource::SatConflictStep))
+      {
+        // Reached bound on number of conflicts:
+        progress_estimate = progressEstimate();
+        cancelUntil(0);
+        // [mdeters] notify theory engine of restarts for deferred
+        // theory processing
+        d_proxy->notifyRestart();
+        return l_Undef;
+      }
 
-            if (clauses_removable.size()-nAssigns() >= max_learnts) {
-                // Reduce the set of learnt clauses:
-                reduceDB();
-            }
+      // Simplify the set of problem clauses:
+      if (decisionLevel() == 0 && !simplify())
+      {
+        return l_False;
+      }
 
-            Lit next = lit_Undef;
-            while (decisionLevel() < assumptions.size()) {
-                // Perform user provided assumption:
-                Lit p = assumptions[decisionLevel()];
-                if (value(p) == l_True) {
-                    // Dummy decision level:
-                    newDecisionLevel();
-                } else if (value(p) == l_False) {
-                  analyzeFinal(~p, d_conflict);
-                  return l_False;
-                } else {
-                    next = p;
-                    break;
-                }
-            }
+      if (clauses_removable.size() - nAssigns() >= max_learnts)
+      {
+        // Reduce the set of learnt clauses:
+        reduceDB();
+      }
 
-            if (next == lit_Undef) {
-                // New variable decision:
-                next = pickBranchLit();
+      Lit next = lit_Undef;
+      while (decisionLevel() < assumptions.size())
+      {
+        // Perform user provided assumption:
+        Lit p = assumptions[decisionLevel()];
+        if (value(p) == l_True)
+        {
+          // Dummy decision level:
+          newDecisionLevel();
+        }
+        else if (value(p) == l_False)
+        {
+          analyzeFinal(~p, d_conflict);
+          return l_False;
+        }
+        else
+        {
+          next = p;
+          break;
+        }
+      }
 
-                if (next == lit_Undef) {
-                    // We need to do a full theory check to confirm
-                  Debug("minisat::search") << "Doing a full theory check..."
-                                           << std::endl;
-                    check_type = CHECK_FINAL;
-                    continue;
-                }
-            }
+      if (next == lit_Undef)
+      {
+        // New variable decision:
+        next = pickBranchLit();
 
-            // Increase decision level and enqueue 'next'
-            newDecisionLevel();
-            uncheckedEnqueue(next);
+        if (next == lit_Undef)
+        {
+          // We need to do a full theory check to confirm
+          Debug("minisat::search")
+              << "Doing a full theory check..." << std::endl;
+          check_type = CHECK_FINAL;
+          continue;
         }
+      }
+
+      // Increase decision level and enqueue 'next'
+      newDecisionLevel();
+      uncheckedEnqueue(next);
     }
+  }
 }
 
 
@@ -1882,7 +1906,7 @@ lbool Solver::solve_()
 
     ScopedBool scoped_bool(minisat_busy, true);
 
-    assert(decisionLevel() == 0);
+    Assert(decisionLevel() == 0);
 
     model.clear();
     d_conflict.clear();
@@ -2002,8 +2026,11 @@ void Solver::toDimacs(FILE* f, const vec<Lit>& assumps)
     fprintf(f, "p cnf %d %d\n", max, cnt);
 
     for (int i = 0; i < assumptions.size(); i++){
-        assert(value(assumptions[i]) != l_False);
-        fprintf(f, "%s%d 0\n", sign(assumptions[i]) ? "-" : "", mapVar(var(assumptions[i]), map, max)+1);
+      Assert(value(assumptions[i]) != l_False);
+      fprintf(f,
+              "%s%d 0\n",
+              sign(assumptions[i]) ? "-" : "",
+              mapVar(var(assumptions[i]), map, max) + 1);
     }
 
     for (int i = 0; i < clauses_persistent.size(); i++)
@@ -2095,8 +2122,8 @@ void Solver::garbageCollect()
 
 void Solver::push()
 {
-  assert(d_enable_incremental);
-  assert(decisionLevel() == 0);
+  Assert(d_enable_incremental);
+  Assert(decisionLevel() == 0);
 
   ++assertionLevel;
   Debug("minisat") << "in user push, increasing assertion level to " << assertionLevel << std::endl;
@@ -2110,9 +2137,9 @@ void Solver::push()
 
 void Solver::pop()
 {
-  assert(d_enable_incremental);
+  Assert(d_enable_incremental);
 
-  assert(decisionLevel() == 0);
+  Assert(decisionLevel() == 0);
 
   // Pop the trail below the user level
   --assertionLevel;
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index f685017a7..b3ed72a4c 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -21,12 +21,12 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef Minisat_Solver_h
 #define Minisat_Solver_h
 
-#include "cvc4_private.h"
-
 #include <iosfwd>
 
+#include "base/check.h"
 #include "base/output.h"
 #include "context/context.h"
+#include "cvc4_private.h"
 #include "expr/proof_node_manager.h"
 #include "proof/clause_id.h"
 #include "prop/minisat/core/SolverTypes.h"
@@ -534,31 +534,32 @@ inline bool Solver::isDecision(Var x) const
 
 inline int Solver::level(Var x) const
 {
-  assert(x < vardata.size());
+  Assert(x < vardata.size());
   return vardata[x].d_level;
 }
 
 inline int Solver::user_level(Var x) const
 {
-  assert(x < vardata.size());
+  Assert(x < vardata.size());
   return vardata[x].d_user_level;
 }
 
 inline int Solver::intro_level(Var x) const
 {
-  assert(x < vardata.size());
+  Assert(x < vardata.size());
   return vardata[x].d_intro_level;
 }
 
 inline int Solver::trail_index(Var x) const
 {
-  assert(x < vardata.size());
+  Assert(x < vardata.size());
   return vardata[x].d_trail_index;
 }
 
 inline void Solver::insertVarOrder(Var x) {
-    assert(x < vardata.size());
-    if (!order_heap.inHeap(x) && decision[x]) order_heap.insert(x); }
+  Assert(x < vardata.size());
+  if (!order_heap.inHeap(x) && decision[x]) order_heap.insert(x);
+}
 
 inline void Solver::varDecayActivity() { var_inc *= (1 / var_decay); }
 inline void Solver::varBumpActivity(Var v) { varBumpActivity(v, var_inc); }
@@ -607,8 +608,16 @@ inline void Solver::newDecisionLevel()
 
 inline int      Solver::decisionLevel ()      const   { return trail_lim.size(); }
 inline uint32_t Solver::abstractLevel (Var x) const   { return 1 << (level(x) & 31); }
-inline lbool    Solver::value         (Var x) const   { assert(x < nVars()); return assigns[x]; }
-inline lbool    Solver::value         (Lit p) const   { assert(var(p) < nVars()); return assigns[var(p)] ^ sign(p); }
+inline lbool Solver::value(Var x) const
+{
+  Assert(x < nVars());
+  return assigns[x];
+}
+inline lbool Solver::value(Lit p) const
+{
+  Assert(var(p) < nVars());
+  return assigns[var(p)] ^ sign(p);
+}
 inline lbool    Solver::modelValue    (Var x) const   { return model[x]; }
 inline lbool    Solver::modelValue    (Lit p) const   { return model[var(p)] ^ sign(p); }
 inline int      Solver::nAssigns      ()      const   { return trail.size(); }
diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h
index b30d97aee..f2d2860c8 100644
--- a/src/prop/minisat/core/SolverTypes.h
+++ b/src/prop/minisat/core/SolverTypes.h
@@ -23,13 +23,13 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef Minisat_SolverTypes_h
 #define Minisat_SolverTypes_h
 
-#include <assert.h>
+#include "base/check.h"
 #include "base/output.h"
-#include "prop/minisat/mtl/IntTypes.h"
 #include "prop/minisat/mtl/Alg.h"
-#include "prop/minisat/mtl/Vec.h"
-#include "prop/minisat/mtl/Map.h"
 #include "prop/minisat/mtl/Alloc.h"
+#include "prop/minisat/mtl/IntTypes.h"
+#include "prop/minisat/mtl/Map.h"
+#include "prop/minisat/mtl/Vec.h"
 
 namespace CVC4 {
 namespace Minisat {
@@ -226,16 +226,21 @@ class Clause {
 
 public:
     void calcAbstraction() {
-        assert(header.has_extra);
-        uint32_t abstraction = 0;
-        for (int i = 0; i < size(); i++)
-            abstraction |= 1 << (var(data[i].lit) & 31);
-        data[header.size].abs = abstraction;  }
-
+      Assert(header.has_extra);
+      uint32_t abstraction = 0;
+      for (int i = 0; i < size(); i++)
+        abstraction |= 1 << (var(data[i].lit) & 31);
+      data[header.size].abs = abstraction;
+    }
 
     int          level       ()      const   { return header.level; }
     int          size        ()      const   { return header.size; }
-    void         shrink      (int i)         { assert(i <= size()); if (header.has_extra) data[header.size-i] = data[header.size]; header.size -= i; }
+    void shrink(int i)
+    {
+      Assert(i <= size());
+      if (header.has_extra) data[header.size - i] = data[header.size];
+      header.size -= i;
+    }
     void         pop         ()              { shrink(1); }
     bool         removable   ()      const   { return header.removable; }
     bool         has_extra   ()      const   { return header.has_extra; }
@@ -253,8 +258,16 @@ public:
     Lit          operator [] (int i) const   { return data[i].lit; }
     operator const Lit* (void) const         { return (Lit*)data; }
 
-    float&       activity    ()              { assert(header.has_extra); return data[header.size].act; }
-    uint32_t     abstraction () const        { assert(header.has_extra); return data[header.size].abs; }
+    float& activity()
+    {
+      Assert(header.has_extra);
+      return data[header.size].act;
+    }
+    uint32_t abstraction() const
+    {
+      Assert(header.has_extra);
+      return data[header.size].abs;
+    }
 
     Lit          subsumes    (const Clause& other) const;
     void         strengthen  (Lit p);
@@ -284,14 +297,15 @@ class ClauseAllocator : public RegionAllocator<uint32_t>
     template<class Lits>
     CRef alloc(int level, const Lits& ps, bool removable = false)
     {
-        assert(sizeof(Lit)      == sizeof(uint32_t));
-        assert(sizeof(float)    == sizeof(uint32_t));
-        bool use_extra = removable | extra_clause_field;
+      Assert(sizeof(Lit) == sizeof(uint32_t));
+      Assert(sizeof(float) == sizeof(uint32_t));
+      bool use_extra = removable | extra_clause_field;
 
-        CRef cid = RegionAllocator<uint32_t>::alloc(clauseWord32Size(ps.size(), use_extra));
-        new (lea(cid)) Clause(ps, use_extra, removable, level);
+      CRef cid = RegionAllocator<uint32_t>::alloc(
+          clauseWord32Size(ps.size(), use_extra));
+      new (lea(cid)) Clause(ps, use_extra, removable, level);
 
-        return cid;
+      return cid;
     }
 
     // Deref, Load Effective Address (LEA), Inverse of LEA (AEL):
@@ -450,8 +464,10 @@ inline Lit Clause::subsumes(const Clause& other) const
 
     //if (other.size() < size() || (extra.abst & ~other.extra.abst) != 0)
     //if (other.size() < size() || (!learnt() && !other.learnt() && (extra.abst & ~other.extra.abst) != 0))
-    assert(!header.removable);   assert(!other.header.removable);
-    assert(header.has_extra); assert(other.header.has_extra);
+    Assert(!header.removable);
+    Assert(!other.header.removable);
+    Assert(header.has_extra);
+    Assert(other.header.has_extra);
     if (other.header.size < header.size || (data[header.size].abs & ~other.data[other.header.size].abs) != 0)
         return lit_Error;
 
diff --git a/src/prop/minisat/mtl/Alg.h b/src/prop/minisat/mtl/Alg.h
index 365b2d5aa..2f8a86c3b 100644
--- a/src/prop/minisat/mtl/Alg.h
+++ b/src/prop/minisat/mtl/Alg.h
@@ -21,6 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef Minisat_Alg_h
 #define Minisat_Alg_h
 
+#include "base/check.h"
 #include "prop/minisat/mtl/Vec.h"
 
 namespace CVC4 {
@@ -38,7 +39,7 @@ static inline void remove(V& ts, const T& t)
 {
     int j = 0;
     for (; j < ts.size() && ts[j] != t; j++);
-    assert(j < ts.size());
+    Assert(j < ts.size());
     for (; j < ts.size()-1; j++) ts[j] = ts[j+1];
     ts.pop();
 }
diff --git a/src/prop/minisat/mtl/Alloc.h b/src/prop/minisat/mtl/Alloc.h
index e5b171bac..98e59e7bf 100644
--- a/src/prop/minisat/mtl/Alloc.h
+++ b/src/prop/minisat/mtl/Alloc.h
@@ -21,8 +21,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef Minisat_Alloc_h
 #define Minisat_Alloc_h
 
-#include "prop/minisat/mtl/XAlloc.h"
+#include "base/check.h"
 #include "prop/minisat/mtl/Vec.h"
+#include "prop/minisat/mtl/XAlloc.h"
 
 namespace CVC4 {
 namespace Minisat {
@@ -61,13 +62,33 @@ class RegionAllocator
     void     free      (int size)    { wasted_ += size; }
 
     // Deref, Load Effective Address (LEA), Inverse of LEA (AEL):
-    T&       operator[](Ref r)       { assert(r >= 0 && r < sz); return memory[r]; }
-    const T& operator[](Ref r) const { assert(r >= 0 && r < sz); return memory[r]; }
+    T& operator[](Ref r)
+    {
+      Assert(r >= 0 && r < sz);
+      return memory[r];
+    }
+    const T& operator[](Ref r) const
+    {
+      Assert(r >= 0 && r < sz);
+      return memory[r];
+    }
 
-    T*       lea       (Ref r)       { assert(r >= 0 && r < sz); return &memory[r]; }
-    const T* lea       (Ref r) const { assert(r >= 0 && r < sz); return &memory[r]; }
-    Ref      ael       (const T* t)  { assert((void*)t >= (void*)&memory[0] && (void*)t < (void*)&memory[sz-1]);
-        return  (Ref)(t - &memory[0]); }
+    T* lea(Ref r)
+    {
+      Assert(r >= 0 && r < sz);
+      return &memory[r];
+    }
+    const T* lea(Ref r) const
+    {
+      Assert(r >= 0 && r < sz);
+      return &memory[r];
+    }
+    Ref ael(const T* t)
+    {
+      Assert((void*)t >= (void*)&memory[0]
+             && (void*)t < (void*)&memory[sz - 1]);
+      return (Ref)(t - &memory[0]);
+    }
 
     void     moveTo(RegionAllocator& to) {
         if (to.memory != NULL) ::free(to.memory);
@@ -102,7 +123,7 @@ void RegionAllocator<T>::capacity(uint32_t min_cap)
     }
     // printf(" .. (%p) cap = %u\n", this, cap);
 
-    assert(cap > 0);
+    Assert(cap > 0);
     memory = (T*)xrealloc(memory, sizeof(T)*cap);
 }
 
@@ -112,7 +133,7 @@ typename RegionAllocator<T>::Ref
 RegionAllocator<T>::alloc(int size)
 { 
     // printf("ALLOC called (this = %p, size = %d)\n", this, size); fflush(stdout);
-    assert(size > 0);
+    Assert(size > 0);
     capacity(sz + size);
 
     uint32_t prev_sz = sz;
diff --git a/src/prop/minisat/mtl/Heap.h b/src/prop/minisat/mtl/Heap.h
index c990f9a99..1e64f6ba5 100644
--- a/src/prop/minisat/mtl/Heap.h
+++ b/src/prop/minisat/mtl/Heap.h
@@ -21,6 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef Minisat_Heap_h
 #define Minisat_Heap_h
 
+#include "base/check.h"
 #include "prop/minisat/mtl/Vec.h"
 
 namespace CVC4 {
@@ -79,12 +80,22 @@ class Heap {
     int  size      ()          const { return heap.size(); }
     bool empty     ()          const { return heap.size() == 0; }
     bool inHeap    (int n)     const { return n < indices.size() && indices[n] >= 0; }
-    int  operator[](int index) const { assert(index < heap.size()); return heap[index]; }
-
-
-    void decrease  (int n) { assert(inHeap(n)); percolateUp  (indices[n]); }
-    void increase  (int n) { assert(inHeap(n)); percolateDown(indices[n]); }
+    int operator[](int index) const
+    {
+      Assert(index < heap.size());
+      return heap[index];
+    }
 
+    void decrease(int n)
+    {
+      Assert(inHeap(n));
+      percolateUp(indices[n]);
+    }
+    void increase(int n)
+    {
+      Assert(inHeap(n));
+      percolateDown(indices[n]);
+    }
 
     // Safe variant of insert/decrease/increase:
     void update(int n)
@@ -100,7 +111,7 @@ class Heap {
     void insert(int n)
     {
         indices.growTo(n+1, -1);
-        assert(!inHeap(n));
+        Assert(!inHeap(n));
 
         indices[n] = heap.size();
         heap.push(n);
diff --git a/src/prop/minisat/mtl/Map.h b/src/prop/minisat/mtl/Map.h
index 17572713f..bf299d55d 100644
--- a/src/prop/minisat/mtl/Map.h
+++ b/src/prop/minisat/mtl/Map.h
@@ -20,6 +20,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef Minisat_Map_h
 #define Minisat_Map_h
 
+#include "base/check.h"
 #include "prop/minisat/mtl/IntTypes.h"
 #include "prop/minisat/mtl/Vec.h"
 
@@ -68,8 +69,8 @@ class Map {
     int        size;
 
     // Don't allow copying (error prone):
-    Map<K,D,H,E>&  operator = (Map<K,D,H,E>& other) { assert(0); }
-                   Map        (Map<K,D,H,E>& other) { assert(0); }
+    Map<K, D, H, E>& operator=(Map<K, D, H, E>& other) { Assert(0); }
+    Map(Map<K, D, H, E>& other) { Assert(0); }
 
     bool    checkCap(int new_size) const { return new_size > cap; }
 
@@ -108,27 +109,25 @@ class Map {
     // PRECONDITION: the key must already exist in the map.
     const D& operator [] (const K& k) const
     {
-        assert(size != 0);
-        const D*         res = NULL;
-        const vec<Pair>& ps  = table[index(k)];
-        for (int i = 0; i < ps.size(); i++)
-            if (equals(ps[i].key, k))
-                res = &ps[i].data;
-        assert(res != NULL);
-        return *res;
+      Assert(size != 0);
+      const D* res = NULL;
+      const vec<Pair>& ps = table[index(k)];
+      for (int i = 0; i < ps.size(); i++)
+        if (equals(ps[i].key, k)) res = &ps[i].data;
+      Assert(res != NULL);
+      return *res;
     }
 
     // PRECONDITION: the key must already exist in the map.
     D& operator [] (const K& k)
     {
-        assert(size != 0);
-        D*         res = NULL;
-        vec<Pair>& ps  = table[index(k)];
-        for (int i = 0; i < ps.size(); i++)
-            if (equals(ps[i].key, k))
-                res = &ps[i].data;
-        assert(res != NULL);
-        return *res;
+      Assert(size != 0);
+      D* res = NULL;
+      vec<Pair>& ps = table[index(k)];
+      for (int i = 0; i < ps.size(); i++)
+        if (equals(ps[i].key, k)) res = &ps[i].data;
+      Assert(res != NULL);
+      return *res;
     }
 
     // PRECONDITION: the key must *NOT* exist in the map.
@@ -154,14 +153,15 @@ class Map {
 
     // PRECONDITION: the key must exist in the map.
     void remove(const K& k) {
-        assert(table != NULL);
-        vec<Pair>& ps = table[index(k)];
-        int j = 0;
-        for (; j < ps.size() && !equals(ps[j].key, k); j++);
-        assert(j < ps.size());
-        ps[j] = ps.last();
-        ps.pop();
-        size--;
+      Assert(table != NULL);
+      vec<Pair>& ps = table[index(k)];
+      int j = 0;
+      for (; j < ps.size() && !equals(ps[j].key, k); j++)
+        ;
+      Assert(j < ps.size());
+      ps[j] = ps.last();
+      ps.pop();
+      size--;
     }
 
     void clear  () {
diff --git a/src/prop/minisat/mtl/Queue.h b/src/prop/minisat/mtl/Queue.h
index ca2014429..242bc9388 100644
--- a/src/prop/minisat/mtl/Queue.h
+++ b/src/prop/minisat/mtl/Queue.h
@@ -21,6 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef Minisat_Queue_h
 #define Minisat_Queue_h
 
+#include "base/check.h"
 #include "prop/minisat/mtl/Vec.h"
 
 namespace CVC4 {
@@ -42,11 +43,30 @@ public:
     void clear (bool dealloc = false) { buf.clear(dealloc); buf.growTo(1); first = end = 0; }
     int  size  () const { return (end >= first) ? end - first : end - first + buf.size(); }
 
-    const T& operator [] (int index) const  { assert(index >= 0); assert(index < size()); return buf[(first + index) % buf.size()]; }
-    T&       operator [] (int index)        { assert(index >= 0); assert(index < size()); return buf[(first + index) % buf.size()]; }
+    const T& operator[](int index) const
+    {
+      Assert(index >= 0);
+      Assert(index < size());
+      return buf[(first + index) % buf.size()];
+    }
+    T& operator[](int index)
+    {
+      Assert(index >= 0);
+      Assert(index < size());
+      return buf[(first + index) % buf.size()];
+    }
 
-    T    peek  () const { assert(first != end); return buf[first]; }
-    void pop   () { assert(first != end); first++; if (first == buf.size()) first = 0; }
+    T peek() const
+    {
+      Assert(first != end);
+      return buf[first];
+    }
+    void pop()
+    {
+      Assert(first != end);
+      first++;
+      if (first == buf.size()) first = 0;
+    }
     void insert(T elem) {   // INVARIANT: buf[end] is always unused
         buf[end++] = elem;
         if (end == buf.size()) end = 0;
diff --git a/src/prop/minisat/mtl/Vec.h b/src/prop/minisat/mtl/Vec.h
index cb81ee580..08e40e8bc 100644
--- a/src/prop/minisat/mtl/Vec.h
+++ b/src/prop/minisat/mtl/Vec.h
@@ -21,9 +21,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef Minisat_Vec_h
 #define Minisat_Vec_h
 
-#include <assert.h>
 #include <new>
 
+#include "base/check.h"
 #include "prop/minisat/mtl/IntTypes.h"
 #include "prop/minisat/mtl/XAlloc.h"
 
@@ -42,9 +42,13 @@ class vec {
     int cap;
 
     // Don't allow copying (error prone):
-    vec<T>&  operator = (vec<T>& other) { assert(0); return *this; }
-             vec        (vec<T>& other) { assert(0); }
-             
+    vec<T>& operator=(vec<T>& other)
+    {
+      Assert(0);
+      return *this;
+    }
+    vec(vec<T>& other) { Assert(0); }
+
     // Helpers for calculating next capacity:
     static inline int  imax   (int x, int y) { int mask = (y-x) >> (sizeof(int)*8-1); return (x&mask) + (y&(~mask)); }
     //static inline void nextCap(int& cap){ cap += ((cap >> 1) + 2) & ~1; }
@@ -62,8 +66,16 @@ public:
 
     // Size operations:
     int      size     (void) const     { return sz; }
-    void     shrink   (int nelems)     { assert(nelems <= sz); for (int i = 0; i < nelems; i++) sz--, data[sz].~T(); }
-    void     shrink_  (int nelems)     { assert(nelems <= sz); sz -= nelems; }
+    void shrink(int nelems)
+    {
+      Assert(nelems <= sz);
+      for (int i = 0; i < nelems; i++) sz--, data[sz].~T();
+    }
+    void shrink_(int nelems)
+    {
+      Assert(nelems <= sz);
+      sz -= nelems;
+    }
     int      capacity (void) const     { return cap; }
     void     capacity (int min_cap);
     void     growTo   (int size);
@@ -73,8 +85,16 @@ public:
     // Stack interface:
     void     push  (void)              { if (sz == cap) capacity(sz+1); new (&data[sz]) T(); sz++; }
     void     push  (const T& elem)     { if (sz == cap) capacity(sz+1); data[sz++] = elem; }
-    void     push_ (const T& elem)     { assert(sz < cap); data[sz++] = elem; }
-    void     pop   (void)              { assert(sz > 0); sz--, data[sz].~T(); }
+    void push_(const T& elem)
+    {
+      Assert(sz < cap);
+      data[sz++] = elem;
+    }
+    void pop(void)
+    {
+      Assert(sz > 0);
+      sz--, data[sz].~T();
+    }
     // NOTE: it seems possible that overflow can happen in the 'sz+1' expression of 'push()', but
     // in fact it can not since it requires that 'cap' is equal to INT_MAX. This in turn can not
     // happen given the way capacities are calculated (below). Essentially, all capacities are
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index 4649a67aa..e925bad09 100644
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -20,6 +20,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include "prop/minisat/simp/SimpSolver.h"
 
+#include "base/check.h"
 #include "options/prop_options.h"
 #include "options/smt_options.h"
 #include "proof/clause_id.h"
@@ -127,7 +128,7 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
       toDimacs();
       return l_Undef;
     }
-    assert(decisionLevel() == 0);
+    Assert(decisionLevel() == 0);
 
     vec<Var> extra_frozen;
     lbool    result = l_True;
@@ -140,7 +141,7 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
             Var v = var(assumptions[i]);
 
             // If an assumption has been eliminated, remember it.
-            assert(!isEliminated(v));
+            Assert(!isEliminated(v));
 
             if (!frozen[v]){
                 // Freeze and store.
@@ -173,8 +174,7 @@ bool SimpSolver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
 {
 #ifndef NDEBUG
     if (use_simplification) {
-      for (int i = 0; i < ps.size(); i++)
-        assert(!isEliminated(var(ps[i])));
+      for (int i = 0; i < ps.size(); i++) Assert(!isEliminated(var(ps[i])));
     }
 #endif
 
@@ -230,8 +230,8 @@ void SimpSolver::removeClause(CRef cr)
 bool SimpSolver::strengthenClause(CRef cr, Lit l)
 {
     Clause& c = ca[cr];
-    assert(decisionLevel() == 0);
-    assert(use_simplification);
+    Assert(decisionLevel() == 0);
+    Assert(use_simplification);
 
     // FIX: this is too inefficient but would be nice to have (properly implemented)
     // if (!find(subsumption_queue, &c))
@@ -356,21 +356,26 @@ void SimpSolver::gatherTouchedClauses()
 
 bool SimpSolver::implied(const vec<Lit>& c)
 {
-    assert(decisionLevel() == 0);
+  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]);
-        }
+  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]);
+    }
+  }
 
-    bool result = propagate(CHECK_WITHOUT_THEORY) != CRef_Undef;
-    cancelUntil(0);
-    return result;
+  bool result = propagate(CHECK_WITHOUT_THEORY) != CRef_Undef;
+  cancelUntil(0);
+  return result;
 }
 
 
@@ -380,7 +385,7 @@ bool SimpSolver::backwardSubsumptionCheck(bool verbose)
     int cnt = 0;
     int subsumed = 0;
     int deleted_literals = 0;
-    assert(decisionLevel() == 0);
+    Assert(decisionLevel() == 0);
 
     while (subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()){
 
@@ -405,7 +410,9 @@ bool SimpSolver::backwardSubsumptionCheck(bool verbose)
         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(c.size() > 1
+               || value(c[0]) == l_True);  // Unit-clauses should have been
+                                           // propagated before this point.
 
         // Find best variable to scan:
         Var best = var(c[0]);
@@ -445,7 +452,7 @@ bool SimpSolver::backwardSubsumptionCheck(bool verbose)
 bool SimpSolver::asymm(Var v, CRef cr)
 {
     Clause& c = ca[cr];
-    assert(decisionLevel() == 0);
+    Assert(decisionLevel() == 0);
 
     if (c.mark() || satisfied(c)) return true;
 
@@ -471,18 +478,16 @@ bool SimpSolver::asymm(Var v, CRef cr)
 
 bool SimpSolver::asymmVar(Var v)
 {
-    assert(use_simplification);
+  Assert(use_simplification);
 
-    const vec<CRef>& cls = occurs.lookup(v);
+  const vec<CRef>& cls = occurs.lookup(v);
 
-    if (value(v) != l_Undef || cls.size() == 0)
-        return true;
+  if (value(v) != l_Undef || cls.size() == 0) return true;
 
-    for (int i = 0; i < cls.size(); i++)
-        if (!asymm(v, cls[i]))
-            return false;
+  for (int i = 0; i < cls.size(); i++)
+    if (!asymm(v, cls[i])) return false;
 
-    return backwardSubsumptionCheck();
+  return backwardSubsumptionCheck();
 }
 
 
@@ -505,7 +510,7 @@ static void mkElimClause(vec<uint32_t>& elimclauses, Var v, Clause& c)
         if (var(c[i]) == v)
             v_pos = i + first;
     }
-    assert(v_pos != -1);
+    Assert(v_pos != -1);
 
     // Swap the first literal with the 'v' literal, so that the literal
     // containing 'v' will occur first in the clause:
@@ -521,44 +526,48 @@ static void mkElimClause(vec<uint32_t>& elimclauses, Var v, Clause& c)
 
 bool SimpSolver::eliminateVar(Var v)
 {
-    assert(!frozen[v]);
-    assert(!isEliminated(v));
-    assert(value(v) == l_Undef);
-
-    // Split the occurrences into positive and negative:
-    //
-    const vec<CRef>& cls = occurs.lookup(v);
-    vec<CRef>        pos, neg;
-    for (int i = 0; i < cls.size(); i++)
-        (find(ca[cls[i]], mkLit(v)) ? pos : neg).push(cls[i]);
-
-    // Check whether the increase in number of clauses stays within the allowed ('grow'). Moreover, no
-    // clause must exceed the limit on the maximal clause size (if it is set):
-    //
-    int cnt         = 0;
-    int clause_size = 0;
+  Assert(!frozen[v]);
+  Assert(!isEliminated(v));
+  Assert(value(v) == l_Undef);
+
+  // Split the occurrences into positive and negative:
+  //
+  const vec<CRef>& cls = occurs.lookup(v);
+  vec<CRef> pos, neg;
+  for (int i = 0; i < cls.size(); i++)
+    (find(ca[cls[i]], mkLit(v)) ? pos : neg).push(cls[i]);
+
+  // Check whether the increase in number of clauses stays within the allowed
+  // ('grow'). Moreover, no clause must exceed the limit on the maximal clause
+  // size (if it is set):
+  //
+  int cnt = 0;
+  int clause_size = 0;
+
+  for (int i = 0; i < pos.size(); i++)
+    for (int j = 0; j < neg.size(); j++)
+      if (merge(ca[pos[i]], ca[neg[j]], v, clause_size)
+          && (++cnt > cls.size() + grow
+              || (clause_lim != -1 && clause_size > clause_lim)))
+        return true;
 
+  // Delete and store old clauses:
+  eliminated[v] = true;
+  setDecisionVar(v, false);
+  eliminated_vars++;
+
+  if (pos.size() > neg.size())
+  {
+    for (int i = 0; i < neg.size(); i++)
+      mkElimClause(elimclauses, v, ca[neg[i]]);
+    mkElimClause(elimclauses, mkLit(v));
+  }
+  else
+  {
     for (int i = 0; i < pos.size(); i++)
-        for (int j = 0; j < neg.size(); j++)
-          if (merge(ca[pos[i]], ca[neg[j]], v, clause_size)
-              && (++cnt > cls.size() + grow
-                  || (clause_lim != -1 && clause_size > clause_lim)))
-            return true;
-
-    // Delete and store old clauses:
-    eliminated[v] = true;
-    setDecisionVar(v, false);
-    eliminated_vars++;
-
-    if (pos.size() > neg.size()){
-        for (int i = 0; i < neg.size(); i++)
-            mkElimClause(elimclauses, v, ca[neg[i]]);
-        mkElimClause(elimclauses, mkLit(v));
-    }else{
-        for (int i = 0; i < pos.size(); i++)
-            mkElimClause(elimclauses, v, ca[pos[i]]);
-        mkElimClause(elimclauses, ~mkLit(v));
-    }
+      mkElimClause(elimclauses, v, ca[pos[i]]);
+    mkElimClause(elimclauses, ~mkLit(v));
+  }
 
     for (int i = 0; i < cls.size(); i++) removeClause(cls[i]);
 
@@ -587,32 +596,35 @@ bool SimpSolver::eliminateVar(Var v)
 
 bool SimpSolver::substitute(Var v, Lit x)
 {
-    assert(!frozen[v]);
-    assert(!isEliminated(v));
-    assert(value(v) == l_Undef);
+  Assert(!frozen[v]);
+  Assert(!isEliminated(v));
+  Assert(value(v) == l_Undef);
 
-    if (!ok) return false;
+  if (!ok) return false;
 
-    eliminated[v] = true;
-    setDecisionVar(v, false);
-    const vec<CRef>& cls = occurs.lookup(v);
+  eliminated[v] = true;
+  setDecisionVar(v, false);
+  const vec<CRef>& cls = occurs.lookup(v);
 
-    vec<Lit>& subst_clause = add_tmp;
-    for (int i = 0; i < cls.size(); i++){
-        Clause& c = ca[cls[i]];
+  vec<Lit>& subst_clause = add_tmp;
+  for (int i = 0; i < cls.size(); i++)
+  {
+    Clause& c = 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 < c.size(); j++)
+    {
+      Lit p = c[j];
+      subst_clause.push(var(p) == v ? x ^ sign(p) : p);
+    }
 
-        removeClause(cls[i]);
-        ClauseId id = ClauseIdUndef;
-        if (!addClause_(subst_clause, c.removable(), id)) {
-            return ok = false;
-        }
+    removeClause(cls[i]);
+    ClauseId id = ClauseIdUndef;
+    if (!addClause_(subst_clause, c.removable(), id))
+    {
+      return ok = false;
     }
+  }
 
     return true;
 }
@@ -657,11 +669,12 @@ bool SimpSolver::eliminate(bool turn_off_elim)
 
         // Empty elim_heap and return immediately on user-interrupt:
         if (asynch_interrupt){
-            assert(bwdsub_assigns == trail.size());
-            assert(subsumption_queue.size() == 0);
-            assert(n_touched == 0);
-            elim_heap.clear();
-            goto cleanup; }
+          Assert(bwdsub_assigns == trail.size());
+          Assert(subsumption_queue.size() == 0);
+          Assert(n_touched == 0);
+          elim_heap.clear();
+          goto cleanup;
+        }
 
         // printf("  ## (time = %6.2f s) ELIM: vars = %d\n", cpuTime(), elim_heap.size());
         for (int cnt = 0; !elim_heap.empty(); cnt++){
@@ -690,7 +703,7 @@ bool SimpSolver::eliminate(bool turn_off_elim)
             checkGarbage(simp_garbage_frac);
         }
 
-        assert(subsumption_queue.size() == 0);
+        Assert(subsumption_queue.size() == 0);
     }
  cleanup:
 
diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h
index f952aee1e..5e348c1e7 100644
--- a/src/prop/minisat/simp/SimpSolver.h
+++ b/src/prop/minisat/simp/SimpSolver.h
@@ -21,12 +21,11 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef Minisat_SimpSolver_h
 #define Minisat_SimpSolver_h
 
+#include "base/check.h"
 #include "cvc4_private.h"
-
 #include "proof/clause_id.h"
-#include "prop/minisat/mtl/Queue.h"
 #include "prop/minisat/core/Solver.h"
-
+#include "prop/minisat/mtl/Queue.h"
 
 namespace CVC4 {
 namespace prop {
@@ -204,11 +203,12 @@ class SimpSolver : public Solver {
 
 inline bool SimpSolver::isEliminated (Var v) const { return eliminated[v]; }
 inline void SimpSolver::updateElimHeap(Var v) {
-    assert(use_simplification);
-    // if (!frozen[v] && !isEliminated(v) && value(v) == l_Undef)
-    if (elim_heap.inHeap(v) || (!frozen[v] && !isEliminated(v) && value(v) == l_Undef))
-        elim_heap.update(v); }
-
+  Assert(use_simplification);
+  // if (!frozen[v] && !isEliminated(v) && value(v) == l_Undef)
+  if (elim_heap.inHeap(v)
+      || (!frozen[v] && !isEliminated(v) && value(v) == l_Undef))
+    elim_heap.update(v);
+}
 
 inline bool SimpSolver::addClause(const vec<Lit>& ps, bool removable, ClauseId& id)
 { ps.copyTo(add_tmp); return addClause_(add_tmp, removable, id); }