Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)

23 files changed, 294 insertions, 293 deletions

diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp
index cb829aba6..d9de9731a 100644
--- a/src/theory/bv/abstraction.cpp
+++ b/src/theory/bv/abstraction.cpp
@@ -140,7 +140,7 @@ Node AbstractionModule::reverseAbstraction(Node assertion, NodeNodeMap& seen) {
   if (isAbstraction(assertion)) {
     Node interp =  getInterpretation(assertion);
     seen[assertion] = interp;
-    Assert (interp.getType() == assertion.getType());
+    Assert(interp.getType() == assertion.getType());
     return interp;
   }
 
@@ -319,7 +319,7 @@ bool AbstractionModule::hasSignature(Node node) {
 
 Node AbstractionModule::getGeneralizedSignature(Node node) {
   NodeNodeMap::const_iterator it = d_assertionToSignature.find(node);
-  Assert (it != d_assertionToSignature.end());
+  Assert(it != d_assertionToSignature.end());
   Node generalized_signature = getGeneralization(it->second);
   return generalized_signature;
 }
@@ -417,14 +417,14 @@ TNode AbstractionModule::getGeneralization(TNode term) {
     return term;
 
   TNode generalization = getGeneralization(it->second);
-  Assert (generalization != term);
+  Assert(generalization != term);
   d_sigToGeneralization[term] = generalization;
   return generalization;
 }
 
 void AbstractionModule::storeGeneralization(TNode s, TNode t) {
-  Assert (s == getGeneralization(s));
-  Assert (t == getGeneralization(t));
+  Assert(s == getGeneralization(s));
+  Assert(t == getGeneralization(t));
   d_sigToGeneralization[s] = t;
 }
 
@@ -559,13 +559,13 @@ void AbstractionModule::collectArguments(TNode node, TNode signature, std::vecto
       args.push_back(node);
       seen.insert(node);
     } else {
-      Assert (signature.getKind() == kind::CONST_BITVECTOR);
+      Assert(signature.getKind() == kind::CONST_BITVECTOR);
     }
     //
     return;
   }
-  Assert (node.getKind() == signature.getKind() &&
-          node.getNumChildren() == signature.getNumChildren());
+  Assert(node.getKind() == signature.getKind()
+         && node.getNumChildren() == signature.getNumChildren());
 
   for (unsigned i = 0; i < node.getNumChildren(); ++i) {
     collectArguments(node[i], signature[i], args, seen);
@@ -618,8 +618,8 @@ bool AbstractionModule::isAbstraction(TNode node) {
 
   TNode constant = node[0].getKind() == kind::CONST_BITVECTOR ? node[0] : node[1];
   TNode func = node[0].getKind() == kind::APPLY_UF ? node[0] : node[1];
-  Assert (constant.getKind() == kind::CONST_BITVECTOR &&
-          func.getKind() == kind::APPLY_UF);
+  Assert(constant.getKind() == kind::CONST_BITVECTOR
+         && func.getKind() == kind::APPLY_UF);
   if (utils::getSize(constant) != 1)
     return false;
   if (constant != utils::mkConst(1, 1u))
@@ -633,14 +633,14 @@ bool AbstractionModule::isAbstraction(TNode node) {
 }
 
 Node AbstractionModule::getInterpretation(TNode node) {
-  Assert (isAbstraction(node));
+  Assert(isAbstraction(node));
   TNode constant = node[0].getKind() == kind::CONST_BITVECTOR ? node[0] : node[1];
   TNode apply = node[0].getKind() == kind::APPLY_UF ? node[0] : node[1];
-  Assert (constant.getKind() == kind::CONST_BITVECTOR &&
-          apply.getKind() == kind::APPLY_UF);
+  Assert(constant.getKind() == kind::CONST_BITVECTOR
+         && apply.getKind() == kind::APPLY_UF);
 
   Node func = apply.getOperator();
-  Assert (d_funcToSignature.find(func) != d_funcToSignature.end());
+  Assert(d_funcToSignature.find(func) != d_funcToSignature.end());
 
   Node sig = d_funcToSignature[func];
 
@@ -648,8 +648,8 @@ Node AbstractionModule::getInterpretation(TNode node) {
   TNodeTNodeMap seen;
   unsigned index = 0;
   Node result = substituteArguments(sig, apply, index, seen);
-  Assert (result.getType().isBoolean());
-  Assert (index == apply.getNumChildren());
+  Assert(result.getType().isBoolean());
+  Assert(index == apply.getNumChildren());
   // Debug("bv-abstraction") << "AbstractionModule::getInterpretation " << node << "\n";
   // Debug("bv-abstraction") << "    => " << result << "\n";
   return result;
@@ -726,10 +726,8 @@ Node AbstractionModule::simplifyConflict(TNode conflict) {
         continue;
       }
 
-      Assert (!subst.hasSubstitution(s));
-      Assert (!t.isNull() &&
-              !s.isNull() &&
-              s!= t);
+      Assert(!subst.hasSubstitution(s));
+      Assert(!t.isNull() && !s.isNull() && s != t);
       subst.addSubstitution(s, t);
 
       for (unsigned k = 0; k < conjuncts.size(); k++) {
@@ -789,14 +787,14 @@ void AbstractionModule::generalizeConflict(TNode conflict, std::vector<Node>& le
   // collect abstract functions
   if (conflict.getKind() != kind::AND) {
     if (isAbstraction(conflict)) {
-      Assert (conflict[0].getKind() == kind::APPLY_UF);
+      Assert(conflict[0].getKind() == kind::APPLY_UF);
       functions.push_back(conflict[0]);
     }
   } else {
     for (unsigned i = 0; i < conflict.getNumChildren(); ++i) {
       TNode conjunct = conflict[i];
       if (isAbstraction(conjunct)) {
-        Assert (conjunct[0].getKind() == kind::APPLY_UF);
+        Assert(conjunct[0].getKind() == kind::APPLY_UF);
         functions.push_back(conjunct[0]);
       }
     }
@@ -871,7 +869,7 @@ bool AbstractionModule::LemmaInstantiatior::isConsistent(const vector<int>& stac
   TNode func = d_functions[current];
   ArgsTableEntry& matches = d_argsTable.getEntry(func.getOperator());
   ArgsVec& args = matches.getEntry(stack[current]);
-  Assert (args.size() == func.getNumChildren());
+  Assert(args.size() == func.getNumChildren());
   for (unsigned k = 0; k < args.size(); ++k) {
     TNode s = func[k];
     TNode t = args[k];
@@ -905,8 +903,8 @@ bool AbstractionModule::LemmaInstantiatior::isConsistent(const vector<int>& stac
       continue;
     }
 
-    Assert (s0.getMetaKind() == kind::metakind::VARIABLE &&
-            t0.getMetaKind() == kind::metakind::VARIABLE);
+    Assert(s0.getMetaKind() == kind::metakind::VARIABLE
+           && t0.getMetaKind() == kind::metakind::VARIABLE);
 
     if (s0 != t0) {
       d_subst.addSubstitution(s0, t0);
@@ -952,7 +950,7 @@ void AbstractionModule::LemmaInstantiatior::generateInstantiations(std::vector<N
 
   std::vector<int> stack;
   backtrack(stack);
-  Assert (d_ctx->getLevel() == 0);
+  Assert(d_ctx->getLevel() == 0);
   Debug("bv-abstraction-gen") << "numLemmas=" << d_lemmas.size() <<"\n";
   lemmas.swap(d_lemmas);
 }
@@ -976,8 +974,8 @@ void AbstractionModule::makeFreshSkolems(TNode node, SubstitutionMap& map, Subst
 }
 
 void AbstractionModule::makeFreshArgs(TNode func, std::vector<Node>& fresh_args) {
-  Assert (fresh_args.size() == 0);
-  Assert (func.getKind() == kind::APPLY_UF);
+  Assert(fresh_args.size() == 0);
+  Assert(func.getKind() == kind::APPLY_UF);
   TNodeNodeMap d_map;
   for (unsigned i = 0; i < func.getNumChildren(); ++i) {
     TNode arg = func[i];
@@ -985,7 +983,7 @@ void AbstractionModule::makeFreshArgs(TNode func, std::vector<Node>& fresh_args)
       fresh_args.push_back(arg);
       continue;
     }
-    Assert (arg.getMetaKind() == kind::metakind::VARIABLE);
+    Assert(arg.getMetaKind() == kind::metakind::VARIABLE);
     TNodeNodeMap::iterator it = d_map.find(arg);
     if (it != d_map.end()) {
       fresh_args.push_back(it->second);
@@ -995,11 +993,11 @@ void AbstractionModule::makeFreshArgs(TNode func, std::vector<Node>& fresh_args)
       fresh_args.push_back(skolem);
     }
   }
-  Assert (fresh_args.size() == func.getNumChildren());
+  Assert(fresh_args.size() == func.getNumChildren());
 }
 
 Node AbstractionModule::tryMatching(const std::vector<Node>& ss, const std::vector<TNode>& tt, TNode conflict) {
-  Assert (ss.size() == tt.size());
+  Assert(ss.size() == tt.size());
 
   Debug("bv-abstraction-dbg") << "AbstractionModule::tryMatching conflict = " << conflict << "\n";
   if (Debug.isOn("bv-abstraction-dbg")) {
@@ -1044,10 +1042,10 @@ Node AbstractionModule::tryMatching(const std::vector<Node>& ss, const std::vect
       continue;
     }
 
-    Assert (s0.getMetaKind() == kind::metakind::VARIABLE &&
-            t0.getMetaKind() == kind::metakind::VARIABLE);
+    Assert(s0.getMetaKind() == kind::metakind::VARIABLE
+           && t0.getMetaKind() == kind::metakind::VARIABLE);
 
-    Assert (s0 != t0);
+    Assert(s0 != t0);
     subst.addSubstitution(s0, t0);
   }
 
@@ -1062,20 +1060,20 @@ void AbstractionModule::storeLemma(TNode lemma) {
     for (unsigned i = 0; i < lemma.getNumChildren(); i++) {
       TNode atom = lemma[i];
       atom = atom.getKind() == kind::NOT ? atom[0] : atom;
-      Assert (atom.getKind() != kind::NOT);
-      Assert (utils::isBVPredicate(atom));
+      Assert(atom.getKind() != kind::NOT);
+      Assert(utils::isBVPredicate(atom));
       d_lemmaAtoms.insert(atom);
     }
   } else {
     lemma = lemma.getKind() == kind::NOT? lemma[0] : lemma;
-    Assert (utils::isBVPredicate(lemma));
+    Assert(utils::isBVPredicate(lemma));
     d_lemmaAtoms.insert(lemma);
   }
 }
 
 
 bool AbstractionModule::isLemmaAtom(TNode node) const {
-  Assert (node.getType().isBoolean());
+  Assert(node.getType().isBoolean());
   node = node.getKind() == kind::NOT? node[0] : node;
 
   return d_inputAtoms.find(node) == d_inputAtoms.end() &&
@@ -1089,7 +1087,7 @@ void AbstractionModule::addInputAtom(TNode atom) {
 }
 
 void AbstractionModule::ArgsTableEntry::addArguments(const ArgsVec& args) {
-  Assert (args.size() == d_arity);
+  Assert(args.size() == d_arity);
   d_data.push_back(args);
 }
 
@@ -1107,7 +1105,7 @@ bool AbstractionModule::ArgsTable::hasEntry(TNode signature) const {
 }
 
 AbstractionModule::ArgsTableEntry& AbstractionModule::ArgsTable::getEntry(TNode signature) {
-  Assert (hasEntry(signature));
+  Assert(hasEntry(signature));
   return d_data.find(signature)->second;
 }
 
diff --git a/src/theory/bv/abstraction.h b/src/theory/bv/abstraction.h
index 5472aa5a2..4895d1818 100644
--- a/src/theory/bv/abstraction.h
+++ b/src/theory/bv/abstraction.h
@@ -60,7 +60,11 @@ class AbstractionModule {
     iterator end() { return d_data.end(); }
     unsigned getArity() { return d_arity; }
     unsigned getNumEntries() { return d_data.size(); }
-    ArgsVec& getEntry(unsigned i ) { Assert (i < d_data.size()); return d_data[i]; }
+    ArgsVec& getEntry(unsigned i)
+    {
+      Assert(i < d_data.size());
+      return d_data[i];
+    }
   };
 
   class ArgsTable {
diff --git a/src/theory/bv/bitblast/aig_bitblaster.cpp b/src/theory/bv/bitblast/aig_bitblaster.cpp
index 3ed926f84..c2bc9e6e8 100644
--- a/src/theory/bv/bitblast/aig_bitblaster.cpp
+++ b/src/theory/bv/bitblast/aig_bitblaster.cpp
@@ -18,7 +18,7 @@
 
 #include "theory/bv/bitblast/aig_bitblaster.h"
 
-#include "base/cvc4_check.h"
+#include "base/check.h"
 #include "options/bv_options.h"
 #include "prop/sat_solver_factory.h"
 #include "smt/smt_statistics_registry.h"
@@ -46,7 +46,7 @@ namespace bv {
 
 template <> inline
 std::string toString<Abc_Obj_t*> (const std::vector<Abc_Obj_t*>& bits) {
-  Unreachable("Don't know how to print AIG");
+  Unreachable() << "Don't know how to print AIG";
 } 
 
 
@@ -72,7 +72,7 @@ Abc_Obj_t* mkOr<Abc_Obj_t*>(Abc_Obj_t* a, Abc_Obj_t* b) {
 
 template <> inline
 Abc_Obj_t* mkOr<Abc_Obj_t*>(const std::vector<Abc_Obj_t*>& children) {
-  Assert (children.size());
+  Assert(children.size());
   if (children.size() == 1)
     return children[0];
   
@@ -91,7 +91,7 @@ Abc_Obj_t* mkAnd<Abc_Obj_t*>(Abc_Obj_t* a, Abc_Obj_t* b) {
 
 template <> inline
 Abc_Obj_t* mkAnd<Abc_Obj_t*>(const std::vector<Abc_Obj_t*>& children) {
-  Assert (children.size());
+  Assert(children.size());
   if (children.size() == 1)
     return children[0];
   
@@ -172,7 +172,7 @@ AigBitblaster::AigBitblaster()
 AigBitblaster::~AigBitblaster() {}
 
 Abc_Obj_t* AigBitblaster::bbFormula(TNode node) {
-  Assert (node.getType().isBoolean());
+  Assert(node.getType().isBoolean());
   Debug("bitvector-bitblast") << "AigBitblaster::bbFormula "<< node << "\n"; 
   
   if (hasAig(node))
@@ -211,7 +211,7 @@ Abc_Obj_t* AigBitblaster::bbFormula(TNode node) {
     }
   case kind::IMPLIES:
     {
-      Assert (node.getNumChildren() == 2); 
+      Assert(node.getNumChildren() == 2);
       Abc_Obj_t* child1 = bbFormula(node[0]);
       Abc_Obj_t* child2 = bbFormula(node[1]);
 
@@ -220,7 +220,7 @@ Abc_Obj_t* AigBitblaster::bbFormula(TNode node) {
     }
   case kind::ITE:
     {
-      Assert (node.getNumChildren() == 3); 
+      Assert(node.getNumChildren() == 3);
       Abc_Obj_t* a = bbFormula(node[0]);
       Abc_Obj_t* b = bbFormula(node[1]);
       Abc_Obj_t* c = bbFormula(node[2]);
@@ -241,7 +241,7 @@ Abc_Obj_t* AigBitblaster::bbFormula(TNode node) {
   case kind::EQUAL:
     {
       if( node[0].getType().isBoolean() ){
-        Assert (node.getNumChildren() == 2); 
+        Assert(node.getNumChildren() == 2);
         Abc_Obj_t* child1 = bbFormula(node[0]);
         Abc_Obj_t* child2 = bbFormula(node[1]);
   
@@ -283,18 +283,18 @@ void AigBitblaster::bbTerm(TNode node, Bits& bits) {
     getBBTerm(node, bits);
     return;
   }
-  Assert( node.getType().isBitVector() );
+  Assert(node.getType().isBitVector());
 
   Debug("bitvector-bitblast") << "Bitblasting term " << node <<"\n";
   d_termBBStrategies[node.getKind()] (node, bits, this);
 
-  Assert (bits.size() == utils::getSize(node));
+  Assert(bits.size() == utils::getSize(node));
   storeBBTerm(node, bits);
 }
 
 
 void AigBitblaster::cacheAig(TNode node, Abc_Obj_t* aig) {
-  Assert (!hasAig(node));
+  Assert(!hasAig(node));
   d_aigCache.insert(std::make_pair(node, aig));
 }
 bool AigBitblaster::hasAig(TNode node) {
@@ -317,9 +317,9 @@ void AigBitblaster::makeVariable(TNode node, Bits& bits) {
 }
 
 Abc_Obj_t* AigBitblaster::mkInput(TNode input) {
-  Assert (!hasInput(input));
-  Assert(input.getKind() == kind::BITVECTOR_BITOF ||
-         (input.getType().isBoolean() && input.isVar()));
+  Assert(!hasInput(input));
+  Assert(input.getKind() == kind::BITVECTOR_BITOF
+         || (input.getType().isBoolean() && input.isVar()));
   Abc_Obj_t* aig_input = Abc_NtkCreatePi(currentAigNtk());
   // d_aigCache.insert(std::make_pair(input, aig_input));
   d_nodeToAigInput.insert(std::make_pair(input, aig_input));
@@ -333,7 +333,7 @@ bool AigBitblaster::hasInput(TNode input) {
 
 bool AigBitblaster::solve(TNode node) {
   // setting output of network to be the query
-  Assert (d_aigOutputNode == NULL);
+  Assert(d_aigOutputNode == NULL);
   Abc_Obj_t* query = bbFormula(node);
   d_aigOutputNode = Abc_NtkCreatePo(currentAigNtk());
   Abc_ObjAddFanin(d_aigOutputNode, query); 
@@ -345,7 +345,7 @@ bool AigBitblaster::solve(TNode node) {
   TimerStat::CodeTimer solveTimer(d_statistics.d_solveTime);
   prop::SatValue result = d_satSolver->solve();
 
-  Assert (result != prop::SAT_VALUE_UNKNOWN); 
+  Assert(result != prop::SAT_VALUE_UNKNOWN);
   return result == prop::SAT_VALUE_TRUE; 
 }
 
@@ -356,7 +356,7 @@ void AigBitblaster::simplifyAig() {
   TimerStat::CodeTimer simpTimer(d_statistics.d_simplificationTime);
 
   Abc_AigCleanup(currentAigM());
-  Assert (Abc_NtkCheck(currentAigNtk()));
+  Assert(Abc_NtkCheck(currentAigNtk()));
 
   const char* command = options::bitvectorAigSimplifications().c_str(); 
   Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
@@ -376,8 +376,8 @@ void AigBitblaster::convertToCnfAndAssert() {
   
   Aig_Man_t * pMan = NULL;
   Cnf_Dat_t * pCnf = NULL;
-  Assert( Abc_NtkIsStrash(currentAigNtk()) );
-  
+  Assert(Abc_NtkIsStrash(currentAigNtk()));
+
   // convert to the AIG manager
   pMan = Abc_NtkToDar(currentAigNtk(), 0, 0 );
   Abc_Stop(); 
@@ -385,9 +385,9 @@ void AigBitblaster::convertToCnfAndAssert() {
   // // free old network
   // Abc_NtkDelete(currentAigNtk());
   // s_abcAigNetwork = NULL;
-  
-  Assert (pMan != NULL);
-  Assert (Aig_ManCheck(pMan));
+
+  Assert(pMan != NULL);
+  Assert(Aig_ManCheck(pMan));
   pCnf = Cnf_DeriveFast( pMan, 0 );
 
   assertToSatSolver(pCnf); 
@@ -416,9 +416,9 @@ void AigBitblaster::assertToSatSolver(Cnf_Dat_t* pCnf) {
     prop::SatClause clause; 
     for (pLit = pCnf->pClauses[i], pStop = pCnf->pClauses[i+1]; pLit < pStop; pLit++ ) {
       int int_lit = Cnf_Lit2Var(*pLit);
-      Assert (int_lit != 0); 
+      Assert(int_lit != 0);
       unsigned index = int_lit < 0? -int_lit : int_lit;
-      Assert (index - 1 < sat_variables.size()); 
+      Assert(index - 1 < sat_variables.size());
       prop::SatLiteral lit(sat_variables[index-1], int_lit < 0); 
       clause.push_back(lit); 
     }
@@ -464,7 +464,7 @@ void AigBitblaster::storeBBAtom(TNode atom, Abc_Obj_t* atom_bb) {
 }
 
 Abc_Obj_t* AigBitblaster::getBBAtom(TNode atom) const {
-  Assert (hasBBAtom(atom));
+  Assert(hasBBAtom(atom));
   return d_bbAtoms.find(atom)->second;
 }
 
diff --git a/src/theory/bv/bitblast/bitblast_strategies_template.h b/src/theory/bv/bitblast/bitblast_strategies_template.h
index 9e668e258..047396506 100644
--- a/src/theory/bv/bitblast/bitblast_strategies_template.h
+++ b/src/theory/bv/bitblast/bitblast_strategies_template.h
@@ -50,7 +50,7 @@ T UndefinedAtomBBStrategy(TNode node, TBitblaster<T>* bb) {
 template <class T>
 T DefaultEqBB(TNode node, TBitblaster<T>* bb) {
   Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
-  
+
   Assert(node.getKind() == kind::EQUAL);
   std::vector<T> lhs, rhs; 
   bb->bbTerm(node[0], lhs);
@@ -75,7 +75,7 @@ T AdderUltBB(TNode node, TBitblaster<T>* bb) {
   bb->bbTerm(node[0], a);
   bb->bbTerm(node[1], b);
   Assert(a.size() == b.size());
-  
+
   // a < b <=> ~ (add(a, ~b, 1).carry_out)
   std::vector<T> not_b;
   negateBits(b, not_b);
@@ -98,7 +98,7 @@ T DefaultUltBB(TNode node, TBitblaster<T>* bb) {
   bb->bbTerm(node[0], a);
   bb->bbTerm(node[1], b);
   Assert(a.size() == b.size());
-  
+
   // construct bitwise comparison 
   T res = uLessThanBB(a, b, false);
   return res; 
@@ -139,7 +139,7 @@ T DefaultSltBB(TNode node, TBitblaster<T>* bb){
   bb->bbTerm(node[0], a);
   bb->bbTerm(node[1], b);
   Assert(a.size() == b.size());
-  
+
   T res = sLessThanBB(a, b, false); 
   return res;
 }
@@ -152,7 +152,7 @@ T DefaultSleBB(TNode node, TBitblaster<T>* bb){
   bb->bbTerm(node[0], a);
   bb->bbTerm(node[1], b);
   Assert(a.size() == b.size());
-  
+
   T res = sLessThanBB(a, b, true); 
   return res;
 }
@@ -204,13 +204,13 @@ void DefaultConstBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
   Debug("bitvector-bb") << "theory::bv::DefaultConstBB bitblasting " << node << "\n";
   Assert(node.getKind() == kind::CONST_BITVECTOR);
   Assert(bits.size() == 0);
-  
+
   for (unsigned i = 0; i < utils::getSize(node); ++i) {
     Integer bit = node.getConst<BitVector>().extract(i, i).getValue();
     if(bit == Integer(0)){
       bits.push_back(mkFalse<T>());
     } else {
-      Assert (bit == Integer(1));
+      Assert(bit == Integer(1));
       bits.push_back(mkTrue<T>()); 
     }
   }
@@ -234,8 +234,8 @@ template <class T>
 void DefaultConcatBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
   Debug("bitvector-bb") << "theory::bv::DefaultConcatBB bitblasting " << node << "\n";
   Assert(bits.size() == 0);
-  
-  Assert (node.getKind() == kind::BITVECTOR_CONCAT);
+
+  Assert(node.getKind() == kind::BITVECTOR_CONCAT);
   for (int i = node.getNumChildren() -1 ; i >= 0; --i ) {
     TNode current = node[i];
     std::vector<T> current_bits; 
@@ -245,7 +245,7 @@ void DefaultConcatBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
       bits.push_back(current_bits[j]);
     }
   }
-  Assert (bits.size() == utils::getSize(node)); 
+  Assert(bits.size() == utils::getSize(node));
   if(Debug.isOn("bitvector-bb")) {
     Debug("bitvector-bb") << "with  bits: " << toString(bits) << "\n"; 
   }
@@ -254,9 +254,8 @@ void DefaultConcatBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
 template <class T>
 void DefaultAndBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
   Debug("bitvector-bb") << "theory::bv::DefaultAndBB bitblasting " << node << "\n";
-  
-  Assert(node.getKind() == kind::BITVECTOR_AND &&
-         bits.size() == 0);
+
+  Assert(node.getKind() == kind::BITVECTOR_AND && bits.size() == 0);
 
   bb->bbTerm(node[0], bits);
   std::vector<T> current;
@@ -267,15 +266,14 @@ void DefaultAndBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
     }
     current.clear();
   }
-  Assert (bits.size() == utils::getSize(node));
+  Assert(bits.size() == utils::getSize(node));
 }
 
 template <class T>
 void DefaultOrBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
   Debug("bitvector-bb") << "theory::bv::DefaultOrBB bitblasting " << node << "\n";
 
-  Assert(node.getKind() == kind::BITVECTOR_OR &&
-         bits.size() == 0);
+  Assert(node.getKind() == kind::BITVECTOR_OR && bits.size() == 0);
 
   bb->bbTerm(node[0], bits);
   std::vector<T> current;
@@ -286,15 +284,14 @@ void DefaultOrBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
     }
     current.clear();
   }
-  Assert (bits.size() == utils::getSize(node));
+  Assert(bits.size() == utils::getSize(node));
 }
 
 template <class T>
 void DefaultXorBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
   Debug("bitvector-bb") << "theory::bv::DefaultXorBB bitblasting " << node << "\n";
 
-  Assert(node.getKind() == kind::BITVECTOR_XOR &&
-         bits.size() == 0);
+  Assert(node.getKind() == kind::BITVECTOR_XOR && bits.size() == 0);
 
   bb->bbTerm(node[0], bits);
   std::vector<T> current;
@@ -305,21 +302,20 @@ void DefaultXorBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
     }
     current.clear();
   }
-  Assert (bits.size() == utils::getSize(node));
+  Assert(bits.size() == utils::getSize(node));
 }
 
 template <class T>
 void DefaultXnorBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
   Debug("bitvector-bb") << "theory::bv::DefaultXnorBB bitblasting " << node << "\n";
 
-  Assert(node.getNumChildren() == 2 &&
-         node.getKind() == kind::BITVECTOR_XNOR &&
-         bits.size() == 0);
+  Assert(node.getNumChildren() == 2 && node.getKind() == kind::BITVECTOR_XNOR
+         && bits.size() == 0);
   std::vector<T> lhs, rhs;
   bb->bbTerm(node[0], lhs);
   bb->bbTerm(node[1], rhs);
-  Assert(lhs.size() == rhs.size()); 
-  
+  Assert(lhs.size() == rhs.size());
+
   for (unsigned i = 0; i < lhs.size(); ++i) {
     bits.push_back(mkIff(lhs[i], rhs[i])); 
   }
@@ -342,7 +338,8 @@ template <class T>
 void DefaultCompBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
   Debug("bitvector") << "theory::bv:: DefaultCompBB bitblasting "<< node << "\n";
 
-  Assert(utils::getSize(node) == 1 && bits.size() == 0 && node.getKind() == kind::BITVECTOR_COMP);
+  Assert(utils::getSize(node) == 1 && bits.size() == 0
+         && node.getKind() == kind::BITVECTOR_COMP);
   std::vector<T> a, b;
   bb->bbTerm(node[0], a);
   bb->bbTerm(node[1], b);
@@ -359,8 +356,7 @@ void DefaultCompBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
 template <class T>
 void DefaultMultBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
   Debug("bitvector") << "theory::bv:: DefaultMultBB bitblasting "<< node << "\n";
-  Assert(res.size() == 0 &&
-         node.getKind() == kind::BITVECTOR_MULT);
+  Assert(res.size() == 0 && node.getKind() == kind::BITVECTOR_MULT);
 
   // if (node.getNumChildren() == 2) {
   //   std::vector<T> a;
@@ -401,8 +397,7 @@ void DefaultMultBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
 template <class T>
 void DefaultPlusBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
   Debug("bitvector-bb") << "theory::bv::DefaultPlusBB bitblasting " << node << "\n";
-  Assert(node.getKind() == kind::BITVECTOR_PLUS &&
-         res.size() == 0);
+  Assert(node.getKind() == kind::BITVECTOR_PLUS && res.size() == 0);
 
   bb->bbTerm(node[0], res);
 
@@ -415,7 +410,7 @@ void DefaultPlusBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
     rippleCarryAdder(res, current, newres, mkFalse<T>());
     res = newres; 
   }
-  
+
   Assert(res.size() == utils::getSize(node));
 }
 
@@ -423,13 +418,12 @@ void DefaultPlusBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
 template <class T>
 void DefaultSubBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
   Debug("bitvector-bb") << "theory::bv::DefaultSubBB bitblasting " << node << "\n";
-  Assert(node.getKind() == kind::BITVECTOR_SUB &&
-         node.getNumChildren() == 2 &&
-         bits.size() == 0);
-    
+  Assert(node.getKind() == kind::BITVECTOR_SUB && node.getNumChildren() == 2
+         && bits.size() == 0);
+
   std::vector<T> a, b;
   bb->bbTerm(node[0], a);
-  bb->bbTerm(node[1], b); 
+  bb->bbTerm(node[1], b);
   Assert(a.size() == b.size() && utils::getSize(node) == a.size());
 
   // bvsub a b = adder(a, ~b, 1)
@@ -442,7 +436,7 @@ template <class T>
 void DefaultNegBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
   Debug("bitvector-bb") << "theory::bv::DefaultNegBB bitblasting " << node << "\n";
   Assert(node.getKind() == kind::BITVECTOR_NEG);
-  
+
   std::vector<T> a;
   bb->bbTerm(node[0], a);
   Assert(utils::getSize(node) == a.size());
@@ -458,7 +452,7 @@ void DefaultNegBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
 
 template <class T>
 void uDivModRec(const std::vector<T>& a, const std::vector<T>& b, std::vector<T>& q, std::vector<T>& r, unsigned rec_width) {
-  Assert( q.size() == 0 && r.size() == 0);
+  Assert(q.size() == 0 && r.size() == 0);
 
   if(rec_width == 0 || isZero(a)) {
     makeZero(q, a.size());
@@ -788,7 +782,7 @@ void DefaultUltbvBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
   bb->bbTerm(node[0], a);
   bb->bbTerm(node[1], b);
   Assert(a.size() == b.size());
-  
+
   // construct bitwise comparison 
   res.push_back(uLessThanBB(a, b, false));
 }
@@ -801,7 +795,7 @@ void DefaultSltbvBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
   bb->bbTerm(node[0], a);
   bb->bbTerm(node[1], b);
   Assert(a.size() == b.size());
-  
+
   // construct bitwise comparison 
   res.push_back(sLessThanBB(a, b, false));
 }
@@ -814,7 +808,7 @@ void DefaultIteBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
   bb->bbTerm(node[0], cond);
   bb->bbTerm(node[1], thenpart);
   bb->bbTerm(node[2], elsepart);
-  
+
   Assert(cond.size() == 1);
   Assert(thenpart.size() == elsepart.size());
 
@@ -826,9 +820,9 @@ void DefaultIteBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
 
 template <class T>
 void DefaultExtractBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
-  Assert (node.getKind() == kind::BITVECTOR_EXTRACT);
+  Assert(node.getKind() == kind::BITVECTOR_EXTRACT);
   Assert(bits.size() == 0);
-  
+
   std::vector<T> base_bits;
   bb->bbTerm(node[0], base_bits);
   unsigned high = utils::getExtractHigh(node);
@@ -837,7 +831,7 @@ void DefaultExtractBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
   for (unsigned i = low; i <= high; ++i) {
     bits.push_back(base_bits[i]); 
   }
-  Assert (bits.size() == high - low + 1);   
+  Assert(bits.size() == high - low + 1);
 
   if(Debug.isOn("bitvector-bb")) {
     Debug("bitvector-bb") << "theory::bv::DefaultExtractBB bitblasting " << node << "\n";
@@ -868,8 +862,7 @@ template <class T>
 void DefaultSignExtendBB (TNode node, std::vector<T>& res_bits, TBitblaster<T>* bb) {
   Debug("bitvector-bb") << "theory::bv::DefaultSignExtendBB bitblasting " << node  << "\n";
 
-  Assert (node.getKind() == kind::BITVECTOR_SIGN_EXTEND &&
-          res_bits.size() == 0);
+  Assert(node.getKind() == kind::BITVECTOR_SIGN_EXTEND && res_bits.size() == 0);
 
   std::vector<T> bits;
   bb->bbTerm(node[0], bits);
@@ -884,8 +877,8 @@ void DefaultSignExtendBB (TNode node, std::vector<T>& res_bits, TBitblaster<T>*
   for (unsigned i = 0 ; i < amount ; ++i ) {
     res_bits.push_back(sign_bit); 
   }
-         
-  Assert (res_bits.size() == amount + bits.size()); 
+
+  Assert(res_bits.size() == amount + bits.size());
 }
 
 template <class T>
diff --git a/src/theory/bv/bitblast/bitblast_utils.h b/src/theory/bv/bitblast/bitblast_utils.h
index f2bee22e5..03e0aa349 100644
--- a/src/theory/bv/bitblast/bitblast_utils.h
+++ b/src/theory/bv/bitblast/bitblast_utils.h
@@ -81,7 +81,7 @@ Node mkOr<Node>(Node a, Node b) {
 
 template <> inline
 Node mkOr<Node>(const std::vector<Node>& children) {
-  Assert (children.size());
+  Assert(children.size());
   if (children.size() == 1)
     return children[0]; 
   return NodeManager::currentNM()->mkNode(kind::OR, children); 
@@ -95,7 +95,7 @@ Node mkAnd<Node>(Node a, Node b) {
 
 template <> inline
 Node mkAnd<Node>(const std::vector<Node>& children) {
-  Assert (children.size());
+  Assert(children.size());
   if (children.size() == 1)
     return children[0]; 
   return NodeManager::currentNM()->mkNode(kind::AND, children); 
@@ -123,7 +123,7 @@ Node mkIte<Node>(Node cond, Node a, Node b) {
 
 template <class T>
 void inline extractBits(const std::vector<T>& b, std::vector<T>& dest, unsigned lo, unsigned hi) {
-  Assert ( lo < b.size() && hi < b.size() && lo <= hi);
+  Assert(lo < b.size() && hi < b.size() && lo <= hi);
   for (unsigned i = lo; i <= hi; ++i) {
     dest.push_back(b[i]); 
   }
@@ -168,7 +168,7 @@ void inline lshift(std::vector<T>& bits, unsigned amount) {
 
 template <class T>
 void inline makeZero(std::vector<T>& bits, unsigned width) {
-  Assert(bits.size() == 0); 
+  Assert(bits.size() == 0);
   for(unsigned i = 0; i < width; ++i) {
     bits.push_back(mkFalse<T>()); 
   }
@@ -188,7 +188,7 @@ void inline makeZero(std::vector<T>& bits, unsigned width) {
 template <class T>
 T inline rippleCarryAdder(const std::vector<T>&a, const std::vector<T>& b, std::vector<T>& res, T carry) {
   Assert(a.size() == b.size() && res.size() == 0);
-  
+
   for (unsigned i = 0 ; i < a.size(); ++i) {
     T sum = mkXor(mkXor(a[i], b[i]), carry);
     carry = mkOr( mkAnd(a[i], b[i]),
@@ -222,8 +222,8 @@ inline void shiftAddMultiplier(const std::vector<T>&a, const std::vector<T>&b, s
 
 template <class T>
 T inline uLessThanBB(const std::vector<T>&a, const std::vector<T>& b, bool orEqual) {
-  Assert (a.size() && b.size());
-  
+  Assert(a.size() && b.size());
+
   T res = mkAnd(mkNot(a[0]), b[0]);
   
   if(orEqual) {
@@ -240,7 +240,7 @@ T inline uLessThanBB(const std::vector<T>&a, const std::vector<T>& b, bool orEqu
 
 template <class T>
 T inline sLessThanBB(const std::vector<T>&a, const std::vector<T>& b, bool orEqual) {
-  Assert (a.size() && b.size());
+  Assert(a.size() && b.size());
   if (a.size() == 1) {
     if(orEqual) {
       return  mkOr(mkIff(a[0], b[0]),
diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp
index 0d3d3b483..9d43355cc 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.cpp
+++ b/src/theory/bv/bitblast/eager_bitblaster.cpp
@@ -60,7 +60,7 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv, context::Context* c)
       solver = prop::SatSolverFactory::createCryptoMinisat(
           smtStatisticsRegistry(), "EagerBitblaster");
       break;
-    default: Unreachable("Unknown SAT solver type");
+    default: Unreachable() << "Unknown SAT solver type";
   }
   d_satSolver.reset(solver);
   d_cnfStream.reset(
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp
index 845fd399e..2018590f7 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.cpp
+++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp
@@ -232,7 +232,7 @@ void TLazyBitblaster::bbTerm(TNode node, Bits& bits) {
     getBBTerm(node, bits);
     return;
   }
-  Assert( node.getType().isBitVector() );
+  Assert(node.getType().isBitVector());
 
   d_bv->spendResource(options::bitblastStep());
   Debug("bitvector-bitblast") << "Bitblasting term " << node <<"\n";
@@ -240,7 +240,7 @@ void TLazyBitblaster::bbTerm(TNode node, Bits& bits) {
 
   d_termBBStrategies[node.getKind()] (node, bits,this);
 
-  Assert (bits.size() == utils::getSize(node));
+  Assert(bits.size() == utils::getSize(node));
 
   storeBBTerm(node, bits);
 }
@@ -257,7 +257,7 @@ void TLazyBitblaster::explain(TNode atom, std::vector<TNode>& explanation) {
 
   ++(d_statistics.d_numExplainedPropagations);
   if (options::bvEagerExplanations()) {
-    Assert (d_explanations->find(lit) != d_explanations->end());
+    Assert(d_explanations->find(lit) != d_explanations->end());
     const std::vector<prop::SatLiteral>& literal_explanation = (*d_explanations)[lit].get();
     for (unsigned i = 0; i < literal_explanation.size(); ++i) {
       explanation.push_back(d_cnfStream->getNode(literal_explanation[i]));
@@ -292,9 +292,9 @@ bool TLazyBitblaster::assertToSat(TNode lit, bool propagate) {
   } else {
     atom = lit;
   }
-  Assert( utils::isBitblastAtom( atom ) );
+  Assert(utils::isBitblastAtom(atom));
 
-  Assert (hasBBAtom(atom));
+  Assert(hasBBAtom(atom));
 
   prop::SatLiteral markerLit = d_cnfStream->getLiteral(atom);
 
@@ -483,7 +483,7 @@ bool TLazyBitblaster::isSharedTerm(TNode node) {
 }
 
 bool TLazyBitblaster::hasValue(TNode a) {
-  Assert (hasBBTerm(a));
+  Assert(hasBBTerm(a));
   Bits bits;
   getBBTerm(a, bits);
   for (int i = bits.size() -1; i >= 0; --i) {
@@ -522,7 +522,7 @@ Node TLazyBitblaster::getModelFromSatSolver(TNode a, bool fullModel) {
     if (d_cnfStream->hasLiteral(bits[i])) {
       prop::SatLiteral bit = d_cnfStream->getLiteral(bits[i]);
       bit_value = d_satSolver->value(bit);
-      Assert (bit_value != prop::SAT_VALUE_UNKNOWN);
+      Assert(bit_value != prop::SAT_VALUE_UNKNOWN);
     } else {
       if (!fullModel) return Node();
       // unconstrained bits default to false
@@ -545,12 +545,12 @@ bool TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel)
     if (d_variables.find(var) == d_variables.end())
       continue;
 
-    Assert (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var));
+    Assert(Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var));
     // only shared terms could not have been bit-blasted
-    Assert (hasBBTerm(var) || isSharedTerm(var));
+    Assert(hasBBTerm(var) || isSharedTerm(var));
 
     Node const_value = getModelFromSatSolver(var, true);
-    Assert (const_value.isNull() || const_value.isConst());
+    Assert(const_value.isNull() || const_value.isConst());
     if(const_value != Node()) {
       Debug("bitvector-model") << "TLazyBitblaster::collectModelInfo (assert (= "
                                << var << " "
@@ -565,7 +565,7 @@ bool TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel)
 }
 
 void TLazyBitblaster::clearSolver() {
-  Assert (d_ctx->getLevel() == 0);
+  Assert(d_ctx->getLevel() == 0);
   d_assertedAtoms->deleteSelf();
   d_assertedAtoms = new(true) context::CDList<prop::SatLiteral>(d_ctx);
   d_explanations->deleteSelf();
diff --git a/src/theory/bv/bv_inequality_graph.cpp b/src/theory/bv/bv_inequality_graph.cpp
index 89d5e1883..ed8756456 100644
--- a/src/theory/bv/bv_inequality_graph.cpp
+++ b/src/theory/bv/bv_inequality_graph.cpp
@@ -36,7 +36,7 @@ bool InequalityGraph::addInequality(TNode a, TNode b, bool strict, TNode reason)
   TermId id_b = registerTerm(b);
   ReasonId id_reason = registerReason(reason);
 
-  Assert (!(isConst(id_a) && isConst(id_b))); 
+  Assert(!(isConst(id_a) && isConst(id_b)));
   BitVector a_val = getValue(id_a);
   BitVector b_val = getValue(id_b);
     
@@ -73,7 +73,7 @@ bool InequalityGraph::addInequality(TNode a, TNode b, bool strict, TNode reason)
   // add the inequality edge
   addEdge(id_a, id_b, strict, id_reason);
   BFSQueue queue(&d_modelValues);
-  Assert (hasModelValue(id_a)); 
+  Assert(hasModelValue(id_a));
   queue.push(id_a);
   return processQueue(queue, id_a); 
 }
@@ -141,7 +141,7 @@ bool InequalityGraph::processQueue(BFSQueue& queue, TermId start) {
         // it means we have an overflow and hence a conflict
         std::vector<TermId> conflict;
         conflict.push_back(it->reason);
-        Assert (hasModelValue(start));
+        Assert(hasModelValue(start));
         ReasonId start_reason = getModelValue(start).reason;
         if (start_reason != UndefinedReasonId) {
           conflict.push_back(start_reason);
@@ -193,9 +193,9 @@ void InequalityGraph::computeExplanation(TermId from, TermId to, std::vector<Rea
   while(hasReason(to) && from != to && !seen.count(to)) {
     seen.insert(to); 
     const ModelValue& exp = getModelValue(to);
-    Assert (exp.reason != UndefinedReasonId); 
+    Assert(exp.reason != UndefinedReasonId);
     explanation.push_back(exp.reason);
-    Assert (exp.parent != UndefinedTermId); 
+    Assert(exp.parent != UndefinedTermId);
     to = exp.parent; 
     Debug("bv-inequality-internal") << "  parent: " << getTermNode(to) << "\n"
                                     << "  reason: " << getReasonNode(exp.reason) << "\n"; 
@@ -213,8 +213,8 @@ void InequalityGraph::addEdge(TermId a, TermId b, bool strict, TermId reason) {
 }
 
 void InequalityGraph::initializeModelValue(TNode node) {
-  TermId id = getTermId(node); 
-  Assert (!hasModelValue(id));
+  TermId id = getTermId(node);
+  Assert(!hasModelValue(id));
   bool isConst = node.getKind() == kind::CONST_BITVECTOR;
   unsigned size = utils::getSize(node); 
   BitVector value = isConst? node.getConst<BitVector>() : BitVector(size, 0u); 
@@ -248,10 +248,10 @@ TermId InequalityGraph::registerTerm(TNode term) {
   bool isConst = term.getKind() == kind::CONST_BITVECTOR;
   InequalityNode ineq = InequalityNode(id, size, isConst);
 
-  Assert (d_ineqNodes.size() == id); 
+  Assert(d_ineqNodes.size() == id);
   d_ineqNodes.push_back(ineq);
-  
-  Assert (d_ineqEdges.size() == id); 
+
+  Assert(d_ineqEdges.size() == id);
   d_ineqEdges.push_back(Edges());
 
   initializeModelValue(term); 
@@ -272,22 +272,22 @@ ReasonId InequalityGraph::registerReason(TNode reason) {
 }
 
 TNode InequalityGraph::getReasonNode(ReasonId id) const {
-  Assert (d_reasonNodes.size() > id);
+  Assert(d_reasonNodes.size() > id);
   return d_reasonNodes[id]; 
 }
 
 TNode InequalityGraph::getTermNode(TermId id) const {
-  Assert (d_termNodes.size() > id);
+  Assert(d_termNodes.size() > id);
   return d_termNodes[id]; 
 }
 
 TermId InequalityGraph::getTermId(TNode node) const {
-  Assert (d_termNodeToIdMap.find(node) != d_termNodeToIdMap.end());
+  Assert(d_termNodeToIdMap.find(node) != d_termNodeToIdMap.end());
   return d_termNodeToIdMap.find(node)->second; 
 }
 
 void InequalityGraph::setConflict(const std::vector<ReasonId>& conflict) {
-  Assert (!d_inConflict); 
+  Assert(!d_inConflict);
   d_inConflict = true;
   d_conflict.clear(); 
   for (unsigned i = 0; i < conflict.size(); ++i) {
@@ -314,7 +314,7 @@ void InequalityGraph::setModelValue(TermId term, const ModelValue& mv) {
 }
 
 InequalityGraph::ModelValue InequalityGraph::getModelValue(TermId term) const {
-  Assert (d_modelValues.find(term) != d_modelValues.end());
+  Assert(d_modelValues.find(term) != d_modelValues.end());
   return (*(d_modelValues.find(term))).second; 
 }
 
@@ -323,7 +323,7 @@ bool InequalityGraph::hasModelValue(TermId id) const {
 }
 
 BitVector InequalityGraph::getValue(TermId id) const {
-  Assert (hasModelValue(id)); 
+  Assert(hasModelValue(id));
   return (*(d_modelValues.find(id))).second.value;
 }
 
@@ -387,10 +387,12 @@ bool InequalityGraph::addDisequality(TNode a, TNode b, TNode reason) {
 }
 
 // void InequalityGraph::splitDisequality(TNode diseq) {
-//   Debug("bv-inequality-internal")<<"InequalityGraph::splitDisequality " << diseq <<"\n"; 
-//   Assert (diseq.getKind() == kind::NOT && diseq[0].getKind() == kind::EQUAL);
-//   if (d_disequalitiesAlreadySplit.find(diseq) == d_disequalitiesAlreadySplit.end()) {
-//     d_disequalitiesToSplit.push_back(diseq); 
+//   Debug("bv-inequality-internal")<<"InequalityGraph::splitDisequality " <<
+//   diseq <<"\n"; Assert (diseq.getKind() == kind::NOT &&
+//   diseq[0].getKind() == kind::EQUAL); if
+//   (d_disequalitiesAlreadySplit.find(diseq) ==
+//   d_disequalitiesAlreadySplit.end()) {
+//     d_disequalitiesToSplit.push_back(diseq);
 //   }
 // }
 
@@ -398,7 +400,7 @@ void InequalityGraph::backtrack() {
   Debug("bv-inequality-internal") << "InequalityGraph::backtrack()\n"; 
   int size = d_undoStack.size(); 
   for (int i = size - 1; i >= (int)d_undoStackIndex.get(); --i) {
-    Assert (!d_undoStack.empty());
+    Assert(!d_undoStack.empty());
     TermId id = d_undoStack.back().first; 
     InequalityEdge edge = d_undoStack.back().second;
     d_undoStack.pop_back();
@@ -409,8 +411,8 @@ void InequalityGraph::backtrack() {
     for (Edges::const_iterator it = edges.begin(); it!= edges.end(); ++it) {
       Debug("bv-inequality-internal") << getTermNode(it->next) <<" " << it->strict << "\n"; 
     }
-    Assert (!edges.empty());
-    Assert (edges.back() == edge);
+    Assert(!edges.empty());
+    Assert(edges.back() == edge);
     edges.pop_back(); 
   }
 }
@@ -444,7 +446,7 @@ void InequalityGraph::checkDisequalities(std::vector<Node>& lemmas) {
 }
 
 bool InequalityGraph::isLessThan(TNode a, TNode b) {
-  Assert (isRegistered(a) && isRegistered(b));
+  Assert(isRegistered(a) && isRegistered(b));
   Unimplemented(); 
 }
 
@@ -457,8 +459,8 @@ bool InequalityGraph::hasValueInModel(TNode node) const {
 }
 
 BitVector InequalityGraph::getValueInModel(TNode node) const {
-  TermId id = getTermId(node); 
-  Assert (hasModelValue(id));
+  TermId id = getTermId(node);
+  Assert(hasModelValue(id));
   return getValue(id); 
 }
 
diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h
index 07facf4af..9e8078a72 100644
--- a/src/theory/bv/bv_inequality_graph.h
+++ b/src/theory/bv/bv_inequality_graph.h
@@ -95,9 +95,9 @@ class InequalityGraph : public context::ContextNotifyObj{
       : d_model(model)
     {}
     bool operator() (TermId left, TermId right) const {
-      Assert (d_model->find(left) != d_model->end() &&
-              d_model->find(right) != d_model->end());
-      
+      Assert(d_model->find(left) != d_model->end()
+             && d_model->find(right) != d_model->end());
+
       return (*(d_model->find(left))).second.value < (*(d_model->find(right))).second.value; 
     }
   }; 
@@ -148,11 +148,22 @@ class InequalityGraph : public context::ContextNotifyObj{
   
   ReasonId registerReason(TNode reason);
   TNode getReasonNode(ReasonId id) const;
-  
-  
-  Edges& getEdges(TermId id) { Assert (id < d_ineqEdges.size()); return d_ineqEdges[id]; }
-  InequalityNode& getInequalityNode(TermId id) { Assert (id < d_ineqNodes.size()); return d_ineqNodes[id]; }
-  const InequalityNode& getInequalityNode(TermId id) const { Assert (id < d_ineqNodes.size()); return d_ineqNodes[id]; }
+
+  Edges& getEdges(TermId id)
+  {
+    Assert(id < d_ineqEdges.size());
+    return d_ineqEdges[id];
+  }
+  InequalityNode& getInequalityNode(TermId id)
+  {
+    Assert(id < d_ineqNodes.size());
+    return d_ineqNodes[id];
+  }
+  const InequalityNode& getInequalityNode(TermId id) const
+  {
+    Assert(id < d_ineqNodes.size());
+    return d_ineqNodes[id];
+  }
   unsigned getBitwidth(TermId id) const { return getInequalityNode(id).getBitwidth(); }
   bool isConst(TermId id) const { return getInequalityNode(id).isConstant(); }
   
diff --git a/src/theory/bv/bv_quick_check.cpp b/src/theory/bv/bv_quick_check.cpp
index 0183dd6e7..dbdeccfe5 100644
--- a/src/theory/bv/bv_quick_check.cpp
+++ b/src/theory/bv/bv_quick_check.cpp
@@ -55,7 +55,7 @@ prop::SatValue BVQuickCheck::checkSat(std::vector<Node>& assumptions, unsigned l
 
   for (unsigned i = 0; i < assumptions.size(); ++i) {
     TNode a = assumptions[i];
-    Assert (a.getType().isBoolean());
+    Assert(a.getType().isBoolean());
     d_bitblaster->bbAtom(a);
     bool ok = d_bitblaster->assertToSat(a, false);
     if (!ok) {
@@ -91,7 +91,7 @@ prop::SatValue BVQuickCheck::checkSat(unsigned long budget) {
 }
 
 bool BVQuickCheck::addAssertion(TNode assertion) {
-  Assert (assertion.getType().isBoolean());
+  Assert(assertion.getType().isBoolean());
   d_bitblaster->bbAtom(assertion);
   // assert to sat solver and run bcp to detect easy conflicts
   bool ok = d_bitblaster->assertToSat(assertion, true);
@@ -162,9 +162,7 @@ QuickXPlain::~QuickXPlain() {}
 
 unsigned QuickXPlain::selectUnsatCore(unsigned low, unsigned high,
                                       std::vector<TNode>& conflict) {
-
-  Assert(!d_solver->getConflict().isNull() &&
-         d_solver->inConflict());
+  Assert(!d_solver->getConflict().isNull() && d_solver->inConflict());
   Node query_confl = d_solver->getConflict();
 
   // conflict wasn't actually minimized
@@ -190,24 +188,23 @@ unsigned QuickXPlain::selectUnsatCore(unsigned low, unsigned high,
   if (write == low) {
     return low;
   }
-  Assert (write != 0);
+  Assert(write != 0);
   unsigned new_high = write - 1;
 
   for (TNodeSet::const_iterator it = nodes.begin(); it != nodes.end(); ++it) {
     conflict[write++] = *it;
   }
-  Assert (write -1 == high);
-  Assert (new_high <= high);
-  
+  Assert(write - 1 == high);
+  Assert(new_high <= high);
+
   return new_high;
 }
 
 void QuickXPlain::minimizeConflictInternal(unsigned low, unsigned high,
                                            std::vector<TNode>& conflict,
                                            std::vector<TNode>& new_conflict) {
+  Assert(low <= high && high < conflict.size());
 
-  Assert (low <= high && high < conflict.size());
-  
   if (low == high) {
     new_conflict.push_back(conflict[low]);
     return;
@@ -323,7 +320,7 @@ Node QuickXPlain::minimizeConflict(TNode confl) {
   ++d_numCalled;
   ++(d_statistics.d_numConflictsMinimized);
   TimerStat::CodeTimer xplainTimer(d_statistics.d_xplainTime);
-  Assert (confl.getNumChildren() > 2);
+  Assert(confl.getNumChildren() > 2);
   std::vector<TNode> conflict;
   for (unsigned i = 0; i < confl.getNumChildren(); ++i) {
     conflict.push_back(confl[i]);
diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index 1f4aef42d..6f8804042 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -83,7 +83,7 @@ SubstitutionEx::SubstitutionEx(theory::SubstitutionMap* modelMap)
 bool SubstitutionEx::addSubstitution(TNode from, TNode to, TNode reason) {
   Debug("bv-substitution") << "SubstitutionEx::addSubstitution: "<< from
                            <<" => "<< to << "\n" << " reason "<<reason << "\n";
-  Assert (from != to);
+  Assert(from != to);
   if (d_substitutions.find(from) != d_substitutions.end()) {
     return false;
   }
@@ -160,12 +160,12 @@ Node SubstitutionEx::internalApply(TNode node) {
 
       if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
         TNode op = current.getOperator();
-        Assert (hasCache(op));
+        Assert(hasCache(op));
         nb << getCache(op);
         reasons.push_back(getReason(op));
       }
       for (unsigned i = 0; i < current.getNumChildren(); ++i) {
-        Assert (hasCache(current[i]));
+        Assert(hasCache(current[i]));
         nb << getCache(current[i]);
         reasons.push_back(getReason(current[i]));
       }
@@ -217,13 +217,13 @@ bool SubstitutionEx::hasCache(TNode node) const {
 }
 
 Node SubstitutionEx::getCache(TNode node) const {
-  Assert (hasCache(node));
+  Assert(hasCache(node));
   return d_cache.find(node)->second.to;
 }
 
 void SubstitutionEx::storeCache(TNode from, TNode to, Node reason) {
   //  Debug("bv-substitution") << "SubstitutionEx::storeCache(" << from <<", " << to <<", "<< reason<<")\n";
-  Assert (!hasCache(from));
+  Assert(!hasCache(from));
   d_cache[from] = SubstitutionElement(to, reason);
 }
 
@@ -284,7 +284,7 @@ bool AlgebraicSolver::check(Theory::Effort e)
     storeExplanation(assertion);
 
     uint64_t assertion_size = d_quickSolver->computeAtomWeight(assertion, seen_assertions);
-    Assert (original_bb_cost <= original_bb_cost + assertion_size);
+    Assert(original_bb_cost <= original_bb_cost + assertion_size);
     original_bb_cost+= assertion_size;
   }
 
@@ -294,7 +294,7 @@ bool AlgebraicSolver::check(Theory::Effort e)
 
   Debug("bv-subtheory-algebraic") << "Assertions " << worklist.size() <<" : \n";
 
-  Assert (d_explanations.size() == worklist.size());
+  Assert(d_explanations.size() == worklist.size());
 
   d_modelMap.reset(new SubstitutionMap(d_context));
   SubstitutionEx subst(d_modelMap.get());
@@ -424,8 +424,8 @@ bool AlgebraicSolver::quickCheck(std::vector<Node>& facts) {
     return true;
   }
 
-  Assert (res == SAT_VALUE_FALSE);
-  Assert (d_quickSolver->inConflict());
+  Assert(res == SAT_VALUE_FALSE);
+  Assert(d_quickSolver->inConflict());
   d_isComplete.set(true);
   Debug("bv-subtheory-algebraic") << " Unsat.\n";
   ++(d_numSolved);
@@ -437,15 +437,15 @@ bool AlgebraicSolver::quickCheck(std::vector<Node>& facts) {
 
   // singleton conflict
   if (conflict.getKind() != kind::AND) {
-    Assert (d_ids.find(conflict) != d_ids.end());
+    Assert(d_ids.find(conflict) != d_ids.end());
     unsigned id = d_ids[conflict];
-    Assert (id < d_explanations.size());
+    Assert(id < d_explanations.size());
     Node theory_confl = d_explanations[id];
     d_bv->setConflict(theory_confl);
     return false;
   }
 
-  Assert (conflict.getKind() == kind::AND);
+  Assert(conflict.getKind() == kind::AND);
   if (options::bitvectorQuickXplain()) {
     d_quickSolver->popToZero();
     Debug("bv-quick-xplain") << "AlgebraicSolver::quickCheck original conflict size " << conflict.getNumChildren() << "\n";
@@ -457,9 +457,9 @@ bool AlgebraicSolver::quickCheck(std::vector<Node>& facts) {
   for (unsigned i = 0; i < conflict.getNumChildren(); ++i) {
     TNode c = conflict[i];
 
-    Assert (d_ids.find(c) != d_ids.end());
+    Assert(d_ids.find(c) != d_ids.end());
     unsigned c_id = d_ids[c];
-    Assert (c_id < d_explanations.size());
+    Assert(c_id < d_explanations.size());
     TNode c_expl = d_explanations[c_id];
     theory_confl.push_back(c_expl);
   }
@@ -514,7 +514,7 @@ bool AlgebraicSolver::solve(TNode fact, TNode reason, SubstitutionEx& subst) {
         if (right[i] != var)
           right_children.push_back(right[i]);
       }
-      Assert (right_children.size());
+      Assert(right_children.size());
       Node new_right = utils::mkNaryNode(kind::BITVECTOR_XOR, right_children);
       std::vector<Node> left_children;
       for (unsigned i = 1; i < left.getNumChildren(); ++i) {
@@ -656,17 +656,17 @@ void AlgebraicSolver::processAssertions(std::vector<WorklistElement>& worklist,
       worklist[i] = WorklistElement(utils::mkTrue(), worklist[i].id);
       changed = true;
     }
-    Assert (d_explanations.size() == worklist.size());
+    Assert(d_explanations.size() == worklist.size());
   }
 }
 
 void AlgebraicSolver::storeExplanation(unsigned id, TNode explanation) {
-  Assert (checkExplanation(explanation));
+  Assert(checkExplanation(explanation));
   d_explanations[id] = explanation;
 }
 
 void AlgebraicSolver::storeExplanation(TNode explanation) {
-  Assert (checkExplanation(explanation));
+  Assert(checkExplanation(explanation));
   d_explanations.push_back(explanation);
 }
 
@@ -713,7 +713,7 @@ EqualityStatus AlgebraicSolver::getEqualityStatus(TNode a, TNode b) {
 bool AlgebraicSolver::collectModelInfo(TheoryModel* model, bool fullModel)
 {
   Debug("bitvector-model") << "AlgebraicSolver::collectModelInfo\n";
-  AlwaysAssert (!d_quickSolver->inConflict());
+  AlwaysAssert(!d_quickSolver->inConflict());
   set<Node> termSet;
   d_bv->computeRelevantTerms(termSet);
 
@@ -746,13 +746,13 @@ bool AlgebraicSolver::collectModelInfo(TheoryModel* model, bool fullModel)
   for (NodeSet::const_iterator it = leaf_vars.begin(); it != leaf_vars.end(); ++it) {
     TNode var = *it;
     Node value = d_quickSolver->getVarValue(var, true);
-    Assert (!value.isNull() || !fullModel);
+    Assert(!value.isNull() || !fullModel);
 
     // may be a shared term that did not appear in the current assertions
     // AJR: need to check whether already in map for cases where collectModelInfo is called multiple times in the same context
     if (!value.isNull() && !d_modelMap->hasSubstitution(var)) {
       Debug("bitvector-model") << "   " << var << " => " << value << "\n";
-      Assert (value.getKind() == kind::CONST_BITVECTOR);
+      Assert(value.getKind() == kind::CONST_BITVECTOR);
       d_modelMap->addSubstitution(var, value);
     }
   }
@@ -763,7 +763,7 @@ bool AlgebraicSolver::collectModelInfo(TheoryModel* model, bool fullModel)
     TNode subst = Rewriter::rewrite(d_modelMap->apply(current));
     Debug("bitvector-model") << "AlgebraicSolver:   " << variables[i] << " => " << subst << "\n";
     // Doesn't have to be constant as it may be irrelevant
-    Assert (subst.getKind() == kind::CONST_BITVECTOR);
+    Assert(subst.getKind() == kind::CONST_BITVECTOR);
     if (!model->assertEquality(variables[i], subst, true))
     {
       return false;
@@ -860,16 +860,16 @@ void ExtractSkolemizer::skolemize(std::vector<WorklistElement>& facts) {
     std::vector<Node> skolems;
     for (unsigned i = 0; i < cuts.size(); ++i) {
       current = cuts[i];
-      Assert (current > 0);
+      Assert(current > 0);
       int size = current - previous;
-      Assert (size > 0);
+      Assert(size > 0);
       Node sk = utils::mkVar(size);
       skolems.push_back(sk);
       previous = current;
     }
     if (current < bw -1) {
       int size = bw - current;
-      Assert (size > 0);
+      Assert(size > 0);
       Node sk = utils::mkVar(size);
       skolems.push_back(sk);
     }
@@ -880,7 +880,7 @@ void ExtractSkolemizer::skolemize(std::vector<WorklistElement>& facts) {
     }
 
     Node skolem_concat = skolems.size() == 1 ? (Node)skolems[0] : (Node) skolem_nb;
-    Assert (utils::getSize(skolem_concat) == utils::getSize(var));
+    Assert(utils::getSize(skolem_concat) == utils::getSize(var));
     storeSkolem(var, skolem_concat);
 
     for (unsigned i = 0; i < el.extracts.size(); ++i) {
@@ -888,8 +888,8 @@ void ExtractSkolemizer::skolemize(std::vector<WorklistElement>& facts) {
       unsigned l = el.extracts[i].low;
       Node extract = utils::mkExtract(var, h, l);
       Node skolem_extract = Rewriter::rewrite(utils::mkExtract(skolem_concat, h, l));
-      Assert (skolem_extract.getMetaKind() == kind::metakind::VARIABLE ||
-              skolem_extract.getKind() == kind::BITVECTOR_CONCAT);
+      Assert(skolem_extract.getMetaKind() == kind::metakind::VARIABLE
+             || skolem_extract.getKind() == kind::BITVECTOR_CONCAT);
       storeSkolem(extract, skolem_extract);
     }
   }
@@ -900,9 +900,9 @@ void ExtractSkolemizer::skolemize(std::vector<WorklistElement>& facts) {
 }
 
 Node ExtractSkolemizer::mkSkolem(Node node) {
-  Assert (node.getKind() == kind::BITVECTOR_EXTRACT &&
-          node[0].getMetaKind() == kind::metakind::VARIABLE);
-  Assert (!d_skolemSubst.hasSubstitution(node));
+  Assert(node.getKind() == kind::BITVECTOR_EXTRACT
+         && node[0].getMetaKind() == kind::metakind::VARIABLE);
+  Assert(!d_skolemSubst.hasSubstitution(node));
   return utils::mkVar(utils::getSize(node));
 }
 
@@ -933,7 +933,7 @@ void ExtractSkolemizer::ExtractList::addExtract(Extract& e) {
 }
 
 void ExtractSkolemizer::storeExtract(TNode var, unsigned high, unsigned low) {
-  Assert (var.getMetaKind() == kind::metakind::VARIABLE);
+  Assert(var.getMetaKind() == kind::metakind::VARIABLE);
   if (d_varToExtract.find(var) == d_varToExtract.end()) {
     d_varToExtract[var] = ExtractList(utils::getSize(var));
   }
@@ -982,7 +982,7 @@ Node mergeExplanations(const std::vector<Node>& expls) {
   TNodeSet literals;
   for (unsigned i = 0; i < expls.size(); ++i) {
     TNode expl = expls[i];
-    Assert (expl.getType().isBoolean());
+    Assert(expl.getType().isBoolean());
     if (expl.getKind() == kind::AND) {
       for (unsigned i = 0; i < expl.getNumChildren(); ++i) {
         TNode child = expl[i];
diff --git a/src/theory/bv/bv_subtheory_algebraic.h b/src/theory/bv/bv_subtheory_algebraic.h
index 7f38b1563..de75ad859 100644
--- a/src/theory/bv/bv_subtheory_algebraic.h
+++ b/src/theory/bv/bv_subtheory_algebraic.h
@@ -228,7 +228,7 @@ public:
   bool check(Theory::Effort e) override;
   void explain(TNode literal, std::vector<TNode>& assumptions) override
   {
-    Unreachable("AlgebraicSolver does not propagate.\n");
+    Unreachable() << "AlgebraicSolver does not propagate.\n";
   }
   EqualityStatus getEqualityStatus(TNode a, TNode b) override;
   bool collectModelInfo(TheoryModel* m, bool fullModel) override;
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index f809c38c0..bf9bfa480 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -86,7 +86,7 @@ void CoreSolver::setMasterEqualityEngine(eq::EqualityEngine* eq) {
 }
 
 void CoreSolver::enableSlicer() {
-  AlwaysAssert (!d_preregisterCalled);
+  AlwaysAssert(!d_preregisterCalled);
   d_useSlicer = true;
   d_statistics.d_slicerEnabled.setData(true);
 }
@@ -97,7 +97,7 @@ void CoreSolver::preRegister(TNode node) {
       d_equalityEngine.addTriggerEquality(node);
       if (d_useSlicer) {
         d_slicer->processEquality(node);
-        AlwaysAssert(!d_checkCalled); 
+        AlwaysAssert(!d_checkCalled);
       }
   } else {
     d_equalityEngine.addTerm(node);
@@ -137,8 +137,8 @@ bool CoreSolver::decomposeFact(TNode fact) {
   Node new_a = getBaseDecomposition(a);
   Node new_b = getBaseDecomposition(b);
 
-  Assert (utils::getSize(new_a) == utils::getSize(new_b) &&
-          utils::getSize(new_a) == utils::getSize(a));
+  Assert(utils::getSize(new_a) == utils::getSize(new_b)
+         && utils::getSize(new_a) == utils::getSize(a));
 
   NodeManager* nm = NodeManager::currentNM();
   Node a_eq_new_a = nm->mkNode(kind::EQUAL, a, new_a);
@@ -157,8 +157,7 @@ bool CoreSolver::decomposeFact(TNode fact) {
     //    a_i == b_i
     if (new_a.getKind() == kind::BITVECTOR_CONCAT &&
         new_b.getKind() == kind::BITVECTOR_CONCAT) {
-
-      Assert (new_a.getNumChildren() == new_b.getNumChildren());
+      Assert(new_a.getNumChildren() == new_b.getNumChildren());
       for (unsigned i = 0; i < new_a.getNumChildren(); ++i) {
         Node eq_i = nm->mkNode(kind::EQUAL, new_a[i], new_b[i]);
         ok = assertFactToEqualityEngine(eq_i, fact);
@@ -174,8 +173,8 @@ bool CoreSolver::check(Theory::Effort e) {
 
   d_bv->spendResource(options::theoryCheckStep());
 
-  d_checkCalled = true; 
-  Assert (!d_bv->inConflict());
+  d_checkCalled = true;
+  Assert(!d_bv->inConflict());
   ++(d_statistics.d_numCallstoCheck);
   bool ok = true;
   std::vector<Node> core_eqs;
@@ -413,7 +412,7 @@ void CoreSolver::conflict(TNode a, TNode b) {
 }
 
 void CoreSolver::eqNotifyNewClass(TNode t) {
-  Assert( d_bv->getExtTheory()!=NULL );
+  Assert(d_bv->getExtTheory() != NULL);
   d_bv->getExtTheory()->registerTerm( t );
 }
 
@@ -460,7 +459,7 @@ bool CoreSolver::collectModelInfo(TheoryModel* m, bool fullModel)
 
 Node CoreSolver::getModelValue(TNode var) {
   Debug("bitvector-model") << "CoreSolver::getModelValue (" << var <<")";
-  Assert (isComplete());
+  Assert(isComplete());
   TNode repr = d_equalityEngine.getRepresentative(var);
   Node result = Node();
   if (repr.getKind() == kind::CONST_BITVECTOR) {
diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index b527eada4..332f96aa2 100644
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -182,22 +182,20 @@ bool InequalitySolver::isInequalityOnly(TNode node) {
 }
 
 void InequalitySolver::explain(TNode literal, std::vector<TNode>& assumptions) {
-  Assert (d_explanations.find(literal) != d_explanations.end());
+  Assert(d_explanations.find(literal) != d_explanations.end());
   TNode explanation = d_explanations[literal];
   assumptions.push_back(explanation);
   Debug("bv-inequality-explain") << "InequalitySolver::explain " << literal << " with " << explanation <<"\n";
 }
 
-void InequalitySolver::propagate(Theory::Effort e) {
-  Assert (false);
-}
+void InequalitySolver::propagate(Theory::Effort e) { Assert(false); }
 bool InequalitySolver::collectModelInfo(TheoryModel* m, bool fullModel)
 {
   Debug("bitvector-model") << "InequalitySolver::collectModelInfo \n";
   std::vector<Node> model;
   d_inequalityGraph.getAllValuesInModel(model);
   for (unsigned i = 0; i < model.size(); ++i) {
-    Assert (model[i].getKind() == kind::EQUAL);
+    Assert(model[i].getKind() == kind::EQUAL);
     if (!m->assertEquality(model[i][0], model[i][1], true))
     {
       return false;
@@ -207,12 +205,12 @@ bool InequalitySolver::collectModelInfo(TheoryModel* m, bool fullModel)
 }
 
 Node InequalitySolver::getModelValue(TNode var) {
-  Assert (isInequalityOnly(var));
+  Assert(isInequalityOnly(var));
   Debug("bitvector-model") << "InequalitySolver::getModelValue (" << var <<")";
-  Assert (isComplete());
+  Assert(isComplete());
   Node result = Node();
   if (!d_inequalityGraph.hasValueInModel(var)) {
-    Assert (d_bv->isSharedTerm(var));
+    Assert(d_bv->isSharedTerm(var));
   } else {
     BitVector val = d_inequalityGraph.getValueInModel(var);
     result = utils::mkConst(val);
diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp
index e633792d8..0ffd58d5a 100644
--- a/src/theory/bv/slicer.cpp
+++ b/src/theory/bv/slicer.cpp
@@ -58,7 +58,7 @@ Base::Base(uint32_t size)
   : d_size(size),
     d_repr(size/32 + (size % 32 == 0? 0 : 1), 0)
 {
-  Assert (d_size > 0); 
+  Assert(d_size > 0);
 }
 
 void Base::sliceAt(Index index)
@@ -73,7 +73,7 @@ void Base::sliceAt(Index index)
 }
 
 void Base::sliceWith(const Base& other) {
-  Assert (d_size == other.d_size);
+  Assert(d_size == other.d_size);
   for (unsigned i = 0; i < d_repr.size(); ++i) {
     d_repr[i] = d_repr[i] | other.d_repr[i]; 
   }
@@ -86,7 +86,7 @@ bool Base::isCutPoint (Index index) const
     return true;
 
   Index vector_index = index / 32;
-  Assert (vector_index < d_size);
+  Assert(vector_index < d_size);
   Index int_index = index % 32;
   uint32_t bit_mask = 1u << int_index;
 
@@ -94,9 +94,9 @@ bool Base::isCutPoint (Index index) const
 }
 
 void Base::diffCutPoints(const Base& other, Base& res) const {
-  Assert (d_size == other.d_size && res.d_size == d_size);
+  Assert(d_size == other.d_size && res.d_size == d_size);
   for (unsigned i = 0; i < d_repr.size(); ++i) {
-    Assert (res.d_repr[i] == 0); 
+    Assert(res.d_repr[i] == 0);
     res.d_repr[i] = d_repr[i] ^ other.d_repr[i]; 
   }
 }
@@ -144,7 +144,7 @@ std::string ExtractTerm::debugPrint() const {
  */
 
 std::pair<TermId, Index> NormalForm::getTerm(Index index, const UnionFind& uf) const {
-  Assert (index < base.getBitwidth()); 
+  Assert(index < base.getBitwidth());
   Index count = 0;
   for (unsigned i = 0; i < decomp.size(); ++i) {
     Index size = uf.getBitwidth(decomp[i]); 
@@ -207,17 +207,17 @@ TermId UnionFind::addTerm(Index bitwidth) {
 void UnionFind::unionTerms(const ExtractTerm& t1, const ExtractTerm& t2) {
   Debug("bv-slicer") << "UnionFind::unionTerms " << t1.debugPrint() << " and \n"
                      << "                      " << t2.debugPrint() << endl;
-  Assert (t1.getBitwidth() == t2.getBitwidth());
-  
+  Assert(t1.getBitwidth() == t2.getBitwidth());
+
   NormalForm nf1(t1.getBitwidth());
   NormalForm nf2(t2.getBitwidth());
   
   getNormalForm(t1, nf1);
   getNormalForm(t2, nf2);
 
-  Assert (nf1.decomp.size() == nf2.decomp.size());
-  Assert (nf1.base == nf2.base);
-  
+  Assert(nf1.decomp.size() == nf2.decomp.size());
+  Assert(nf1.base == nf2.base);
+
   for (unsigned i = 0; i < nf1.decomp.size(); ++i) {
     merge (nf1.decomp[i], nf2.decomp[i]); 
   } 
@@ -239,7 +239,7 @@ void UnionFind::merge(TermId t1, TermId t2) {
   if (t1 == t2)
     return;
 
-  Assert (! hasChildren(t1) && ! hasChildren(t2));
+  Assert(!hasChildren(t1) && !hasChildren(t2));
   setRepr(t1, t2); 
   d_representatives.erase(t1);
   d_statistics.d_numRepresentatives += -1; 
@@ -271,7 +271,7 @@ void UnionFind::split(TermId id, Index i) {
     // nothing to do 
     return;
   }
-  Assert (i < getBitwidth(id));
+  Assert(i < getBitwidth(id));
   if (!hasChildren(id)) {
     // first time we split this term 
     TermId bottom_id = addTerm(i);
@@ -303,13 +303,12 @@ void UnionFind::getNormalForm(const ExtractTerm& term, NormalForm& nf) {
 
 void UnionFind::getDecomposition(const ExtractTerm& term, Decomposition& decomp) {
   // making sure the term is aligned
-  TermId id = find(term.id); 
+  TermId id = find(term.id);
 
-  Assert (term.high < getBitwidth(id));
+  Assert(term.high < getBitwidth(id));
   // because we split the node, this must be the whole extract
   if (!hasChildren(id)) {
-    Assert (term.high == getBitwidth(id) - 1 &&
-            term.low == 0);
+    Assert(term.high == getBitwidth(id) - 1 && term.low == 0);
     decomp.push_back(id);
     return; 
   }
@@ -380,9 +379,9 @@ void UnionFind::handleCommonSlice(const Decomposition& decomp1, const Decomposit
 
   if (start2 - start1 < common_size) {
     Index overlap = start1 + common_size - start2;
-    Assert (overlap > 0);
+    Assert(overlap > 0);
     Index diff = common_size - overlap;
-    Assert (diff >= 0);
+    Assert(diff >= 0);
     Index granularity = gcd(diff, overlap);
     // split the common part 
     for (unsigned i = 0; i < common_size; i+= granularity) {
@@ -401,7 +400,7 @@ void UnionFind::alignSlicings(const ExtractTerm& term1, const ExtractTerm& term2
   getNormalForm(term1, nf1);
   getNormalForm(term2, nf2);
 
-  Assert (nf1.base.getBitwidth() == nf2.base.getBitwidth());
+  Assert(nf1.base.getBitwidth() == nf2.base.getBitwidth());
 
   // first check if the two have any common slices
   std::vector<TermId> intersection;
@@ -480,8 +479,8 @@ ExtractTerm Slicer::registerTerm(TNode node) {
 
 void Slicer::processEquality(TNode eq) {
   Debug("bv-slicer") << "Slicer::processEquality: " << eq << endl;
-  
-  Assert (eq.getKind() == kind::EQUAL);
+
+  Assert(eq.getKind() == kind::EQUAL);
   TNode a = eq[0];
   TNode b = eq[1];
   ExtractTerm a_ex= registerTerm(a);
@@ -508,7 +507,7 @@ void Slicer::getBaseDecomposition(TNode node, std::vector<Node>& decomp) {
     low = utils::getExtractLow(node);
     top = node[0]; 
   }
-  AlwaysAssert (d_nodeToId.find(top) != d_nodeToId.end()); 
+  AlwaysAssert(d_nodeToId.find(top) != d_nodeToId.end());
   TermId id = d_nodeToId[top];
   NormalForm nf(high-low+1); 
   d_unionFind.getNormalForm(ExtractTerm(id, high, low), nf);
diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h
index 3ddbcaf36..88ac0debb 100644
--- a/src/theory/bv/slicer.h
+++ b/src/theory/bv/slicer.h
@@ -91,7 +91,7 @@ struct ExtractTerm {
       high(h),
       low(l)
   {
-    Assert (h >= l && id != UndefinedId); 
+    Assert(h >= l && id != UndefinedId);
   }
   Index getBitwidth() const { return high - low + 1; }
   std::string debugPrint() const; 
@@ -138,15 +138,15 @@ class UnionFind {
     bool hasChildren() const { return d_ch1 != UndefinedId && d_ch0 != UndefinedId; }
 
     TermId getChild(Index i) const {
-      Assert (i < 2);
+      Assert(i < 2);
       return i == 0? d_ch0 : d_ch1;
     }
     void setRepr(TermId id) {
-      Assert (! hasChildren());
+      Assert(!hasChildren());
       d_repr = id;
     }
     void setChildren(TermId ch1, TermId ch0) {
-      Assert (d_repr == UndefinedId && !hasChildren());
+      Assert(d_repr == UndefinedId && !hasChildren());
       d_ch1 = ch1;
       d_ch0 = ch0; 
     }
@@ -162,27 +162,28 @@ class UnionFind {
   void handleCommonSlice(const Decomposition& d1, const Decomposition& d2, TermId common);
   /// getter methods for the internal nodes
   TermId getRepr(TermId id)  const {
-    Assert (id < d_nodes.size());
+    Assert(id < d_nodes.size());
     return d_nodes[id].getRepr(); 
   }
   TermId getChild(TermId id, Index i) const {
-    Assert (id < d_nodes.size());
+    Assert(id < d_nodes.size());
     return d_nodes[id].getChild(i); 
   }
   Index getCutPoint(TermId id) const {
     return getBitwidth(getChild(id, 0)); 
   }
   bool hasChildren(TermId id) const {
-    Assert (id < d_nodes.size());
+    Assert(id < d_nodes.size());
     return d_nodes[id].hasChildren(); 
   }
   /// setter methods for the internal nodes
   void setRepr(TermId id, TermId new_repr) {
-    Assert (id < d_nodes.size());
+    Assert(id < d_nodes.size());
     d_nodes[id].setRepr(new_repr); 
   }
   void setChildren(TermId id, TermId ch1, TermId ch0) {
-    Assert (id < d_nodes.size() && getBitwidth(id) == getBitwidth(ch1) + getBitwidth(ch0));
+    Assert(id < d_nodes.size()
+           && getBitwidth(id) == getBitwidth(ch1) + getBitwidth(ch0));
     d_nodes[id].setChildren(ch1, ch0); 
   }
 
@@ -218,7 +219,7 @@ public:
   void alignSlicings(const ExtractTerm& term1, const ExtractTerm& term2);
   void ensureSlicing(const ExtractTerm& term);
   Index getBitwidth(TermId id) const {
-    Assert (id < d_nodes.size());
+    Assert(id < d_nodes.size());
     return d_nodes[id].getBitwidth(); 
   }
   std::string debugPrint(TermId id);
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index b7e52205f..23ffabcd1 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -336,7 +336,7 @@ void TheoryBV::check(Effort e)
     std::vector<TNode> assertions;
     while (!done()) {
       TNode fact = get().assertion;
-      Assert (fact.getKind() == kind::BITVECTOR_EAGER_ATOM);
+      Assert(fact.getKind() == kind::BITVECTOR_EAGER_ATOM);
       assertions.push_back(fact);
       d_eagerSolver->assertFormula(fact[0]);
     }
@@ -379,13 +379,13 @@ void TheoryBV::check(Effort e)
   bool ok = true;
   bool complete = false;
   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
-    Assert (!inConflict());
+    Assert(!inConflict());
     ok = d_subtheories[i]->check(e);
     complete = d_subtheories[i]->isComplete();
 
     if (!ok) {
       // if we are in a conflict no need to check with other theories
-      Assert (inConflict());
+      Assert(inConflict());
       sendConflict();
       return;
     }
@@ -511,7 +511,7 @@ bool TheoryBV::doExtfReductions( std::vector< Node >& terms ) {
   if( getExtTheory()->doReductions( 0, terms, nredr ) ){
     return true;
   }
-  Assert( nredr.empty() );
+  Assert(nredr.empty());
   return false;
 }
 
@@ -873,7 +873,7 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
 
 
 void TheoryBV::explain(TNode literal, std::vector<TNode>& assumptions) {
-  Assert (wasPropagatedBySubtheory(literal));
+  Assert(wasPropagatedBySubtheory(literal));
   SubTheory sub = getPropagatingSubtheory(literal);
   d_subtheoryMap[sub]->explain(literal, assumptions);
 }
@@ -912,7 +912,7 @@ EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
 {
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER)
     return EQUALITY_UNKNOWN;
-  Assert (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY);
+  Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY);
   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
     EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b);
     if (status != EQUALITY_UNKNOWN) {
@@ -924,7 +924,7 @@ EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
 
 
 void TheoryBV::enableCoreTheorySlicer() {
-  Assert (!d_calledPreregister);
+  Assert(!d_calledPreregister);
   d_isCoreTheory = true;
   if (d_subtheoryMap.find(SUB_CORE) != d_subtheoryMap.end()) {
     CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
@@ -979,7 +979,7 @@ bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions, std::vector
       options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER &&
       options::bitvectorAig()) {
     // disable AIG mode
-    AlwaysAssert (!d_eagerSolver->isInitialized());
+    AlwaysAssert(!d_eagerSolver->isInitialized());
     d_eagerSolver->turnOffAig();
     d_eagerSolver->initialize();
   }
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index eefda524e..44ac14464 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -389,6 +389,7 @@ class RewriteRule {
   /** Actually apply the rewrite rule */
   static inline Node apply(TNode node) {
     Unreachable();
+    SuppressWrongNoReturnWarning;
   }
 
 public:
@@ -408,8 +409,10 @@ public:
     
   }
 
-  static inline bool applies(TNode node) {
+  static inline bool applies(TNode node)
+  {
     Unreachable();
+    SuppressWrongNoReturnWarning;
   }
 
   template<bool checkApplies>
diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index cada3d30c..153f785ca 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -312,7 +312,7 @@ static inline void updateCoefMap(TNode current, unsigned size,
       break;
     }
     case kind::BITVECTOR_SUB:
-      // turn into a + (-1)*b 
+      // turn into a + (-1)*b
       Assert(current.getNumChildren() == 2);
       addToCoefMap(factorToCoefficient, current[0], BitVector(size, (unsigned)1)); 
       addToCoefMap(factorToCoefficient, current[1], -BitVector(size, (unsigned)1)); 
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index 0e42886b5..c3e1b316c 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -308,7 +308,7 @@ Node RewriteRule<ShlByConst>::apply(TNode node) {
   
   // make sure we do not lose information casting
   Assert(amount < Integer(1).multiplyByPow2(32));
-  
+
   uint32_t uint32_amount = amount.toUnsignedInt();
 
   Node left = utils::mkExtract(a, size - 1 - uint32_amount, 0);
@@ -350,7 +350,7 @@ Node RewriteRule<LshrByConst>::apply(TNode node) {
   
   // make sure we do not lose information casting
   Assert(amount < Integer(1).multiplyByPow2(32));
-  
+
   uint32_t uint32_amount = amount.toUnsignedInt();
   Node right = utils::mkExtract(a, size - 1, uint32_amount);
   Node left = utils::mkZero(uint32_amount);
@@ -481,7 +481,7 @@ Node RewriteRule<AndOne>::apply(TNode node) {
   if (node[0] == utils::mkOnes(size)) {
     return node[1]; 
   } else {
-    Assert (node[1] == utils::mkOnes(size)); 
+    Assert(node[1] == utils::mkOnes(size));
     return node[0]; 
   }
 }
@@ -1640,7 +1640,7 @@ Node RewriteRule<MergeSignExtend>::apply(TNode node) {
     Node res = nb;
     return res;
   }
-  Assert (node[0].getKind() == kind::BITVECTOR_SIGN_EXTEND);
+  Assert(node[0].getKind() == kind::BITVECTOR_SIGN_EXTEND);
   unsigned amount2 =
       node[0].getOperator().getConst<BitVectorSignExtend>().signExtendAmount;
   return utils::mkSignExtend(node[0][0], amount1 + amount2);
diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h
index e56f752af..9d5c6f396 100644
--- a/src/theory/bv/theory_bv_type_rules.h
+++ b/src/theory/bv/theory_bv_type_rules.h
@@ -342,7 +342,8 @@ class IntToBitVectorOpTypeRule
                                          nodeManager->mkBitVectorType(bvSize));
     }
 
-    InternalError("bv-conversion typerule invoked for non-bv-conversion kind");
+    InternalError()
+        << "bv-conversion typerule invoked for non-bv-conversion kind";
   }
 }; /* class IntToBitVectorOpTypeRule */
 
@@ -372,7 +373,8 @@ class BitVectorConversionTypeRule
       return nodeManager->mkBitVectorType(bvSize);
     }
 
-    InternalError("bv-conversion typerule invoked for non-bv-conversion kind");
+    InternalError()
+        << "bv-conversion typerule invoked for non-bv-conversion kind";
   }
 }; /* class BitVectorConversionTypeRule */
 
diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp
index f1cb197ab..c0df9f35c 100644
--- a/src/theory/bv/theory_bv_utils.cpp
+++ b/src/theory/bv/theory_bv_utils.cpp
@@ -287,9 +287,8 @@ Node mkVar(unsigned size)
 
 Node mkSortedNode(Kind kind, TNode child1, TNode child2)
 {
-  Assert(kind == kind::BITVECTOR_AND
-      || kind == kind::BITVECTOR_OR
-      || kind == kind::BITVECTOR_XOR);
+  Assert(kind == kind::BITVECTOR_AND || kind == kind::BITVECTOR_OR
+         || kind == kind::BITVECTOR_XOR);
 
   if (child1 < child2)
   {
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 975796719..23eaab3f8 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -118,15 +118,10 @@ Node mkSortedNode(Kind kind, std::vector<Node>& children);
 template<bool ref_count>
 Node mkNaryNode(Kind k, const std::vector<NodeTemplate<ref_count>>& nodes)
 {
-  Assert (k == kind::AND
-          || k == kind::OR
-          || k == kind::XOR
-          || k == kind::BITVECTOR_AND
-          || k == kind::BITVECTOR_OR
-          || k == kind::BITVECTOR_XOR
-          || k == kind::BITVECTOR_PLUS
-          || k == kind::BITVECTOR_SUB
-          || k == kind::BITVECTOR_MULT);
+  Assert(k == kind::AND || k == kind::OR || k == kind::XOR
+         || k == kind::BITVECTOR_AND || k == kind::BITVECTOR_OR
+         || k == kind::BITVECTOR_XOR || k == kind::BITVECTOR_PLUS
+         || k == kind::BITVECTOR_SUB || k == kind::BITVECTOR_MULT);
 
   if (nodes.size() == 1) { return nodes[0]; }
   return NodeManager::currentNM()->mkNode(k, nodes);