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

38 files changed, 374 insertions, 365 deletions

diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp
index 9d516de61..9e6e4842f 100644
--- a/src/theory/quantifiers/alpha_equivalence.cpp
+++ b/src/theory/quantifiers/alpha_equivalence.cpp
@@ -85,7 +85,7 @@ Node AlphaEquivalenceTypeNode::registerNode(Node q,
   while (index < typs.size())
   {
     TypeNode curr = typs[index];
-    Assert( typ_count.find( curr )!=typ_count.end() );
+    Assert(typ_count.find(curr) != typ_count.end());
     Trace("aeq-debug") << "[" << curr << " " << typ_count[curr] << "] ";
     aetn = &(aetn->d_children[curr][typ_count[curr]]);
     index = index + 1;
@@ -96,7 +96,7 @@ Node AlphaEquivalenceTypeNode::registerNode(Node q,
 
 Node AlphaEquivalenceDb::addTerm(Node q)
 {
-  Assert( q.getKind()==FORALL );
+  Assert(q.getKind() == FORALL);
   Trace("aeq") << "Alpha equivalence : register " << q << std::endl;
   //construct canonical quantified formula
   Node t = d_tc->getCanonicalTerm(q[1], true);
diff --git a/src/theory/quantifiers/anti_skolem.cpp b/src/theory/quantifiers/anti_skolem.cpp
index d972f2a1c..cdb15b349 100644
--- a/src/theory/quantifiers/anti_skolem.cpp
+++ b/src/theory/quantifiers/anti_skolem.cpp
@@ -37,7 +37,7 @@ struct sortTypeOrder {
 
 void QuantAntiSkolem::SkQuantTypeCache::add( std::vector< TypeNode >& typs, Node q, unsigned index ) {
   if( index==typs.size() ){
-    Assert( std::find( d_quants.begin(), d_quants.end(), q )==d_quants.end() );
+    Assert(std::find(d_quants.begin(), d_quants.end(), q) == d_quants.end());
     d_quants.push_back( q );
   }else{
     d_children[typs[index]].add( typs, q, index+1 );
@@ -134,12 +134,12 @@ void QuantAntiSkolem::check(Theory::Effort e, QEffort quant_e)
           for( unsigned j=0; j<d_ask_types[q].size();  ){
             TypeNode curr = d_ask_types[q][j];
             for( unsigned k=0; k<indices[curr].size(); k++ ){
-              Assert( d_ask_types[q][j]==curr );
+              Assert(d_ask_types[q][j] == curr);
               d_ask_types_index[q].push_back( indices[curr][k] );
               j++;
             }
           }
-          Assert( d_ask_types_index[q].size()==d_ask_types[q].size() );
+          Assert(d_ask_types_index[q].size() == d_ask_types[q].size());
         }else{
           d_quant_sip.erase( q );
         }
@@ -158,7 +158,7 @@ void QuantAntiSkolem::check(Theory::Effort e, QEffort quant_e)
 }
 
 bool QuantAntiSkolem::sendAntiSkolemizeLemma( std::vector< Node >& quants, bool pconnected ) {
-  Assert( !quants.empty() );
+  Assert(!quants.empty());
   std::sort( quants.begin(), quants.end() );
   if( d_sqc->add( d_quantEngine->getUserContext(), quants ) ){
     //partition into connected components
@@ -190,7 +190,7 @@ bool QuantAntiSkolem::sendAntiSkolemizeLemma( std::vector< Node >& quants, bool
             eqcs.push_back( func_to_eqc[f] );
           }
         }
-        Assert( !eqcs.empty() );
+        Assert(!eqcs.empty());
         //merge equivalence classes
         int id = eqcs[0];
         eqc_to_quant[id].push_back( q );
@@ -214,7 +214,7 @@ bool QuantAntiSkolem::sendAntiSkolemizeLemma( std::vector< Node >& quants, bool
       if( eqc_to_quant.size()>1 ){
         bool addedLemma = false;
         for( std::map< int, std::vector< Node > >::iterator it = eqc_to_quant.begin(); it != eqc_to_quant.end(); ++it ){
-          Assert( it->second.size()<quants.size() );
+          Assert(it->second.size() < quants.size());
           bool ret = sendAntiSkolemizeLemma( it->second, false );
           addedLemma = addedLemma || ret;
         }
@@ -245,7 +245,7 @@ bool QuantAntiSkolem::sendAntiSkolemizeLemma( std::vector< Node >& quants, bool
       std::vector< Node > subs_lhs;
       std::vector< Node > subs_rhs;
       //get outer variable substitution
-      Assert( d_ask_types_index[q].size()==d_ask_types[q].size() );
+      Assert(d_ask_types_index[q].size() == d_ask_types[q].size());
       std::vector<Node> sivars;
       d_quant_sip[q].getSingleInvocationVariables(sivars);
       for (unsigned j = 0, size = d_ask_types_index[q].size(); j < size; j++)
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index c52666dad..bed382e28 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -479,7 +479,7 @@ void CegInstantiator::activateInstantiationVariable(Node v, unsigned index)
     if( tn.isReal() ){
       vinst = new ArithInstantiator(tn, d_parent->getVtsTermCache());
     }else if( tn.isSort() ){
-      Assert( options::quantEpr() );
+      Assert(options::quantEpr());
       vinst = new EprInstantiator(tn);
     }else if( tn.isDatatype() ){
       vinst = new DtInstantiator(tn);
@@ -622,7 +622,7 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i)
     //get the instantiator object
     Assert(d_instantiator.find(pv) != d_instantiator.end());
     Instantiator* vinst = d_instantiator[pv];
-    Assert( vinst!=NULL );
+    Assert(vinst != NULL);
     d_active_instantiators[pv] = vinst;
     vinst->reset(this, sf, pv, d_effort);
     // if d_effort is full, we must choose at least one model value
@@ -656,7 +656,7 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i)
           && d_qe->getLogicInfo().isLinear())
       {
         Trace("cbqi-warn") << "Had to resort to model value." << std::endl;
-        Assert( false );
+        Assert(false);
       }
 #endif
       Node mv = getModelValue( pv );
@@ -940,7 +940,7 @@ void CegInstantiator::pushStackVariable( Node v ) {
 }
 
 void CegInstantiator::popStackVariable() {
-  Assert( !d_stack_vars.empty() );
+  Assert(!d_stack_vars.empty());
   d_stack_vars.pop_back();
 }
 
@@ -961,11 +961,11 @@ bool CegInstantiator::constructInstantiationInc(Node pv,
                          << ") ";
       Node mod_pv = pv_prop.getModifiedTerm( pv );
       Trace("cbqi-inst-debug") << mod_pv << " -> " << n << std::endl;
-      Assert( n.getType().isSubtypeOf( pv.getType() ) );
+      Assert(n.getType().isSubtypeOf(pv.getType()));
     }
     //must ensure variables have been computed for n
     computeProgVars( n );
-    Assert( d_inelig.find( n )==d_inelig.end() );
+    Assert(d_inelig.find(n) == d_inelig.end());
 
     //substitute into previous substitutions, when applicable
     std::vector< Node > a_var;
@@ -986,7 +986,7 @@ bool CegInstantiator::constructInstantiationInc(Node pv,
     Trace("cbqi-inst-debug2") << "Applying substitutions to previous substitution terms..." << std::endl;
     for( unsigned j=0; j<sf.d_subs.size(); j++ ){
       Trace("cbqi-inst-debug2") << "  Apply for " << sf.d_subs[j]  << std::endl;
-      Assert( d_prog_var.find( sf.d_subs[j] )!=d_prog_var.end() );
+      Assert(d_prog_var.find(sf.d_subs[j]) != d_prog_var.end());
       if( d_prog_var[sf.d_subs[j]].find( pv )!=d_prog_var[sf.d_subs[j]].end() ){
         prev_subs[j] = sf.d_subs[j];
         TNode tv = pv;
@@ -1016,14 +1016,17 @@ bool CegInstantiator::constructInstantiationInc(Node pv,
             
             // if previously was basic, becomes non-basic
             if( prev_basic && !sf.d_props[j].isBasic() ){
-              Assert( std::find( sf.d_non_basic.begin(), sf.d_non_basic.end(), sf.d_vars[j] )==sf.d_non_basic.end() );
+              Assert(std::find(sf.d_non_basic.begin(),
+                               sf.d_non_basic.end(),
+                               sf.d_vars[j])
+                     == sf.d_non_basic.end());
               new_non_basic.push_back( sf.d_vars[j] );
               sf.d_non_basic.push_back( sf.d_vars[j] );
             }
           }
           if( sf.d_subs[j]!=prev_subs[j] ){
             computeProgVars( sf.d_subs[j] );
-            Assert( d_inelig.find( sf.d_subs[j] )==d_inelig.end() );
+            Assert(d_inelig.find(sf.d_subs[j]) == d_inelig.end());
           }
           Trace("cbqi-inst-debug2") << "Subs " << j << " " << sf.d_subs[j] << std::endl;
         }else{
@@ -1088,7 +1091,7 @@ bool CegInstantiator::doAddInstantiation( std::vector< Node >& vars, std::vector
     for (unsigned i = 0, size = d_input_vars.size(); i < size; ++i)
     {
       std::map<Node, Node>::iterator it = subs_map.find(d_input_vars[i]);
-      Assert( it!=subs_map.end() );
+      Assert(it != subs_map.end());
       Node n = it->second;
       Trace("cbqi-inst-debug") << "  " << d_input_vars[i] << " -> " << n
                                << std::endl;
@@ -1144,7 +1147,7 @@ bool CegInstantiator::isEligibleForInstantiation(Node n) const
 }
 
 bool CegInstantiator::canApplyBasicSubstitution( Node n, std::vector< Node >& non_basic ){
-  Assert( d_prog_var.find( n )!=d_prog_var.end() );
+  Assert(d_prog_var.find(n) != d_prog_var.end());
   if( !non_basic.empty() ){
     for (std::unordered_set<Node, NodeHashFunction>::iterator it =
              d_prog_var[n].begin();
@@ -1163,13 +1166,13 @@ bool CegInstantiator::canApplyBasicSubstitution( Node n, std::vector< Node >& no
 Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< TermProperties >& prop, 
                                          std::vector< Node >& non_basic, TermProperties& pv_prop, bool try_coeff ) {
   computeProgVars( n );
-  Assert( n==Rewriter::rewrite( n ) );
+  Assert(n == Rewriter::rewrite(n));
   bool is_basic = canApplyBasicSubstitution( n, non_basic );
   if( Trace.isOn("cegqi-si-apply-subs-debug") ){
     Trace("cegqi-si-apply-subs-debug") << "is_basic = " << is_basic << "  " << tn << std::endl;
     for( unsigned i=0; i<subs.size(); i++ ){
       Trace("cegqi-si-apply-subs-debug") << "  " << vars[i] << " -> " << subs[i] << "   types : " << vars[i].getType() << " -> " << subs[i].getType() << std::endl;
-      Assert( subs[i].getType().isSubtypeOf( vars[i].getType() ) );
+      Assert(subs[i].getType().isSubtypeOf(vars[i].getType()));
     }
   }
   Node nret;
@@ -1182,8 +1185,8 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node
       std::vector< Node > nsubs;
       for( unsigned i=0; i<vars.size(); i++ ){
         if( !prop[i].d_coeff.isNull() ){
-          Assert( vars[i].getType().isInteger() );
-          Assert( prop[i].d_coeff.isConst() );
+          Assert(vars[i].getType().isInteger());
+          Assert(prop[i].d_coeff.isConst());
           Node nn = NodeManager::currentNM()->mkNode( MULT, subs[i], NodeManager::currentNM()->mkConst( Rational(1)/prop[i].d_coeff.getConst<Rational>() ) );
           nn = NodeManager::currentNM()->mkNode( kind::TO_INTEGER, nn );
           nn =  Rewriter::rewrite( nn );
@@ -1238,7 +1241,7 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node
             if( !it->second.isNull() ){
               c_coeff = NodeManager::currentNM()->mkNode( MULT, c_coeff, it->second );
             }
-            Assert( !c_coeff.isNull() );
+            Assert(!c_coeff.isNull());
             Node c;
             if( msum_term[it->first].isNull() ){
               c = c_coeff;
@@ -1285,7 +1288,7 @@ Node CegInstantiator::applySubstitutionToLiteral( Node lit, std::vector< Node >&
     bool pol = lit.getKind()!=NOT;
     //arithmetic inequalities and disequalities
     if( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol && atom[0].getType().isReal() ) ){
-      Assert( atom.getKind()!=GEQ || atom[1].isConst() );
+      Assert(atom.getKind() != GEQ || atom[1].isConst());
       Node atom_lhs;
       Node atom_rhs;
       if( atom.getKind()==GEQ ){
@@ -1512,7 +1515,7 @@ void CegInstantiator::processAssertions() {
       addToAuxVarSubstitution( subs_lhs, subs_rhs, r, it->second );
     }else{
       Trace("cbqi-proc") << "....no substitution found for auxiliary variable " << r << "!!! type is " << r.getType() << std::endl;
-      Assert( false );
+      Assert(false);
     }
   }
 
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 7f9c21a65..0ec87f239 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -121,7 +121,7 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q)
               //add totality lemma
               std::map< TypeNode, std::vector< Node > >::iterator itc = qepr->d_consts.find( tn );
               if( itc!=qepr->d_consts.end() ){
-                Assert( !itc->second.empty() );
+                Assert(!itc->second.empty());
                 Node ic = d_quantEngine->getTermUtil()->getInstantiationConstant( q, i );
                 std::vector< Node > disj;
                 for( unsigned j=0; j<itc->second.size(); j++ ){
@@ -131,10 +131,10 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q)
                 Trace("cbqi-lemma") << "EPR totality lemma : " << tlem << std::endl;
                 d_quantEngine->getOutputChannel().lemma( tlem );
               }else{
-                Assert( false );
+                Assert(false);
               }                  
             }else{
-              Assert( !options::cbqiAll() );
+              Assert(!options::cbqiAll());
             }
           }
         }
@@ -152,7 +152,7 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q)
           if( std::find( d_parent_quant[q].begin(), d_parent_quant[q].end(), qi )==d_parent_quant[q].end() ){
             d_parent_quant[q].push_back( qi );
             d_children_quant[qi].push_back( q );
-            Assert( hasAddedCbqiLemma( qi ) );
+            Assert(hasAddedCbqiLemma(qi));
             Node qicel = getCounterexampleLiteral(qi);
             dep.push_back( qi );
             dep.push_back( qicel );
@@ -221,7 +221,7 @@ void InstStrategyCegqi::reset_round(Theory::Effort effort)
     Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
     //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine
     if( doCbqi( q ) ){
-      Assert( hasAddedCbqiLemma( q ) );
+      Assert(hasAddedCbqiLemma(q));
       if( d_quantEngine->getModel()->isQuantifierActive( q ) ){
         d_active_quant[q] = true;
         Debug("cbqi-debug") << "Check quantified formula " << q << "..." << std::endl;
@@ -242,8 +242,8 @@ void InstStrategyCegqi::reset_round(Theory::Effort effort)
               //process from waitlist
               while( d_nested_qe_waitlist_proc[q]<d_nested_qe_waitlist_size[q] ){
                 int index = d_nested_qe_waitlist_proc[q];
-                Assert( index>=0 );
-                Assert( index<(int)d_nested_qe_waitlist[q].size() );
+                Assert(index >= 0);
+                Assert(index < (int)d_nested_qe_waitlist[q].size());
                 Node nq = d_nested_qe_waitlist[q][index];
                 Node nqeqn = doNestedQENode( d_nested_qe_info[nq].d_q, q, nq, d_nested_qe_info[nq].d_inst_terms, d_nested_qe_info[nq].d_doVts );
                 Node dqelem = nq.eqNode( nqeqn ); 
@@ -279,10 +279,10 @@ void InstStrategyCegqi::reset_round(Theory::Effort effort)
       } 
       Trace("cbqi-debug") << "Found " << ninner.size() << " non-innermost." << std::endl;
       for( unsigned i=0; i<ninner.size(); i++ ){
-        Assert( d_active_quant.find( ninner[i] )!=d_active_quant.end() );
+        Assert(d_active_quant.find(ninner[i]) != d_active_quant.end());
         d_active_quant.erase( ninner[i] );
       }
-      Assert( !d_active_quant.empty() );
+      Assert(!d_active_quant.empty());
       Trace("cbqi-debug") << "...done removing." << std::endl;
     }
   }
@@ -293,7 +293,7 @@ void InstStrategyCegqi::check(Theory::Effort e, QEffort quant_e)
 {
   if (quant_e == QEFFORT_STANDARD)
   {
-    Assert( !d_quantEngine->inConflict() );
+    Assert(!d_quantEngine->inConflict());
     double clSet = 0;
     if( Trace.isOn("cbqi-engine") ){
       clSet = double(clock())/double(CLOCKS_PER_SEC);
@@ -314,7 +314,7 @@ void InstStrategyCegqi::check(Theory::Effort e, QEffort quant_e)
           }
         }else{
           Trace("cbqi-warn") << "CBQI : Cannot process already eliminated quantified formula " << q << std::endl;
-          Assert( false );
+          Assert(false);
         }
       }
       if( d_quantEngine->inConflict() || d_quantEngine->getNumLemmasWaiting()>lastWaiting ){
@@ -490,9 +490,10 @@ Node InstStrategyCegqi::doNestedQENode(
     Trace("cbqi-nqe") << "  " << ceq << std::endl; 
     Trace("cbqi-nqe") << "  " << d_nested_qe[ceq] << std::endl;
     //should not contain quantifiers
-    Assert( !QuantifiersRewriter::containsQuantifiers( d_nested_qe[ceq] ) );
+    Assert(!QuantifiersRewriter::containsQuantifiers(d_nested_qe[ceq]));
   }
-  Assert( d_quantEngine->getTermUtil()->d_inst_constants[q].size()==inst_terms.size() );
+  Assert(d_quantEngine->getTermUtil()->d_inst_constants[q].size()
+         == inst_terms.size());
   //replace inst constants with instantiation
   Node ret = d_nested_qe[ceq].substitute( d_quantEngine->getTermUtil()->d_inst_constants[q].begin(),
                                           d_quantEngine->getTermUtil()->d_inst_constants[q].end(),
@@ -544,7 +545,7 @@ Node InstStrategyCegqi::doNestedQERec(Node q,
             d_nested_qe_info[nr].d_inst_terms.insert( d_nested_qe_info[nr].d_inst_terms.end(), inst_terms.begin(), inst_terms.end() );
             d_nested_qe_info[nr].d_doVts = doVts;
             //TODO: ensure this holds by restricting prenex when cbqiNestedQe is true.
-            Assert( !options::cbqiInnermost() );
+            Assert(!options::cbqiInnermost());
           }
         } 
       } 
@@ -665,7 +666,7 @@ Node InstStrategyCegqi::getCounterexampleLiteral(Node q)
 }
 
 bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) {
-  Assert( !d_curr_quant.isNull() );
+  Assert(!d_curr_quant.isNull());
   //if doing partial quantifier elimination, record the instantiation and set the incomplete flag instead of sending instantiation lemma
   if( d_quantEngine->getQuantAttributes()->isQuantElimPartial( d_curr_quant ) ){
     d_cbqi_set_quant_inactive = true;
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 400db4a8e..bdab6810c 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -42,7 +42,7 @@ struct sortConjectureScore {
 
 void OpArgIndex::addTerm( std::vector< TNode >& terms, TNode n, unsigned index ){
   if( index==n.getNumChildren() ){
-    Assert( n.hasOperator() );
+    Assert(n.hasOperator());
     if( std::find( d_ops.begin(), d_ops.end(), n.getOperator() )==d_ops.end() ){
       d_ops.push_back( n.getOperator() );
       d_op_terms.push_back( n );
@@ -188,12 +188,12 @@ void ConjectureGenerator::setUniversalRelevant( TNode n ) {
 
 bool ConjectureGenerator::isUniversalLessThan( TNode rt1, TNode rt2 ) {
   //prefer the one that is (normal, smaller) lexographically
-  Assert( d_pattern_is_relevant.find( rt1 )!=d_pattern_is_relevant.end() );
-  Assert( d_pattern_is_relevant.find( rt2 )!=d_pattern_is_relevant.end() );
-  Assert( d_pattern_is_normal.find( rt1 )!=d_pattern_is_normal.end() );
-  Assert( d_pattern_is_normal.find( rt2 )!=d_pattern_is_normal.end() );
-  Assert( d_pattern_fun_sum.find( rt1 )!=d_pattern_fun_sum.end() );
-  Assert( d_pattern_fun_sum.find( rt2 )!=d_pattern_fun_sum.end() );
+  Assert(d_pattern_is_relevant.find(rt1) != d_pattern_is_relevant.end());
+  Assert(d_pattern_is_relevant.find(rt2) != d_pattern_is_relevant.end());
+  Assert(d_pattern_is_normal.find(rt1) != d_pattern_is_normal.end());
+  Assert(d_pattern_is_normal.find(rt2) != d_pattern_is_normal.end());
+  Assert(d_pattern_fun_sum.find(rt1) != d_pattern_fun_sum.end());
+  Assert(d_pattern_fun_sum.find(rt2) != d_pattern_fun_sum.end());
 
   if( d_pattern_is_relevant[rt1] && !d_pattern_is_relevant[rt2] ){
     Trace("thm-ee-debug") << "UEE : LT due to relevant." << std::endl;
@@ -271,7 +271,7 @@ TNode ConjectureGenerator::getUniversalRepresentative( TNode n, bool add ) {
               if( d_urelevant_terms.find( eq_terms[i] )!=d_urelevant_terms.end() ){
                 assertEq = true;
               }else{
-                Assert( eq_terms[i].getType()==tn );
+                Assert(eq_terms[i].getType() == tn);
                 registerPattern( eq_terms[i], tn );
                 if( isUniversalLessThan( eq_terms[i], t ) || ( options::conjectureUeeIntro() && d_pattern_fun_sum[t]>=d_pattern_fun_sum[eq_terms[i]] ) ){
                   setUniversalRelevant( eq_terms[i] );
@@ -409,8 +409,8 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e)
         }
         ++eqcs_i;
       }
-      Assert( !d_bool_eqc[0].isNull() );
-      Assert( !d_bool_eqc[1].isNull() );
+      Assert(!d_bool_eqc[0].isNull());
+      Assert(!d_bool_eqc[1].isNull());
       d_urelevant_terms.clear();
       Trace("sg-proc") << "...done get eq classes" << std::endl;
 
@@ -675,7 +675,10 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e)
 
             //add information about pattern
             Trace("sg-gen-tg-debug") << "Collect pattern information..." << std::endl;
-            Assert( std::find( d_rel_patterns[tnn].begin(), d_rel_patterns[tnn].end(), nn )==d_rel_patterns[tnn].end() );
+            Assert(std::find(d_rel_patterns[tnn].begin(),
+                             d_rel_patterns[tnn].end(),
+                             nn)
+                   == d_rel_patterns[tnn].end());
             d_rel_patterns[tnn].push_back( nn );
             //build information concerning the variables in this pattern
             unsigned sum = 0;
@@ -695,7 +698,7 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e)
             d_rel_pattern_var_sum[nn] = sum;
             //register the pattern
             registerPattern( nn, tnn );
-            Assert( d_pattern_is_normal[nn] );
+            Assert(d_pattern_is_normal[nn]);
             Trace("sg-gen-tg-debug") << "...done collect pattern information" << std::endl;
 
             //record information about types
@@ -739,7 +742,7 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e)
                       Trace("sg-rel-term-debug") << "    ";
                     }
                     Trace("sg-rel-term-debug") << it->first << ":x" << it2->first << " -> " << it2->second;
-                    Assert( tindex+it2->first<gsubs_terms.size() );
+                    Assert(tindex + it2->first < gsubs_terms.size());
                     gsubs_terms[tindex+it2->first] = it2->second;
                   }
                 }
@@ -787,7 +790,7 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e)
               if( considerTermCanon( rhs, false ) ){
                 Trace("sg-rel-prop") << "Relevant RHS : " << rhs << std::endl;
                 //register pattern
-                Assert( rhs.getType()==rt_types[i] );
+                Assert(rhs.getType() == rt_types[i]);
                 registerPattern( rhs, rt_types[i] );
                 if( rdepth<depth ){
                   //consider against all LHS at depth
@@ -969,7 +972,7 @@ unsigned ConjectureGenerator::collectFunctions( TNode opat, TNode pat, std::map<
     }
     return sum;
   }else{
-    Assert( pat.getNumChildren()==0 );
+    Assert(pat.getNumChildren() == 0);
     funcs[pat]++;
     //for variables
     if( pat.getKind()==BOUND_VARIABLE ){
@@ -1009,8 +1012,8 @@ void ConjectureGenerator::registerPattern( Node pat, TypeNode tpat ) {
     d_patterns[TypeNode::null()].push_back( pat );
     d_patterns[tpat].push_back( pat );
 
-    Assert( d_pattern_fun_id.find( pat )==d_pattern_fun_id.end() );
-    Assert( d_pattern_var_id.find( pat )==d_pattern_var_id.end() );
+    Assert(d_pattern_fun_id.find(pat) == d_pattern_fun_id.end());
+    Assert(d_pattern_var_id.find(pat) == d_pattern_var_id.end());
 
     //collect functions
     std::map< TypeNode, unsigned > mnvn;
@@ -1034,11 +1037,11 @@ bool ConjectureGenerator::isGeneralization( TNode patg, TNode pat, std::map< TNo
       return true;
     }
   }else{
-    Assert( patg.hasOperator() );
+    Assert(patg.hasOperator());
     if( !pat.hasOperator() || patg.getOperator()!=pat.getOperator() ){
       return false;
     }else{
-      Assert( patg.getNumChildren()==pat.getNumChildren() );
+      Assert(patg.getNumChildren() == pat.getNumChildren());
       for( unsigned i=0; i<patg.getNumChildren(); i++ ){
         if( !isGeneralization( patg[i], pat[i], subs ) ){
           return false;
@@ -1151,8 +1154,8 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector<
             children.push_back( n.getOperator() );
             for( unsigned i=0; i<(vec.size()-1); i++ ){
               Node nn = te->getEnumerateTerm(types[i], vec[i]);
-              Assert( !nn.isNull() );
-              Assert( nn.getType()==n[i].getType() );
+              Assert(!nn.isNull());
+              Assert(nn.getType() == n[i].getType());
               children.push_back( nn );
             }
             children.push_back( lc );
@@ -1233,7 +1236,7 @@ void ConjectureGenerator::processCandidateConjecture( TNode lhs, TNode rhs, unsi
 }
 
 int ConjectureGenerator::considerCandidateConjecture( TNode lhs, TNode rhs ) {
-  Assert( lhs.getType()==rhs.getType() );
+  Assert(lhs.getType() == rhs.getType());
 
   Trace("sg-cconj-debug") << "Consider candidate conjecture : " << lhs << " == " << rhs << "?" << std::endl;
   if( lhs==rhs ){
@@ -1288,7 +1291,7 @@ int ConjectureGenerator::considerCandidateConjecture( TNode lhs, TNode rhs ) {
     Trace("sg-cconj") << "Consider possible candidate conjecture : " << lhs << " == " << rhs << "?" << std::endl;
     //find witness for counterexample, if possible
     if( options::conjectureFilterModel() ){
-      Assert( d_rel_pattern_var_sum.find( lhs )!=d_rel_pattern_var_sum.end() );
+      Assert(d_rel_pattern_var_sum.find(lhs) != d_rel_pattern_var_sum.end());
       Trace("sg-cconj-debug") << "Notify substitutions over " << d_rel_pattern_var_sum[lhs] << " variables." << std::endl;
       std::map< TNode, TNode > subs;
       d_subs_confirmCount = 0;
@@ -1329,7 +1332,7 @@ bool ConjectureGenerator::notifySubstitution( TNode glhs, std::map< TNode, TNode
   if( Trace.isOn("sg-cconj-debug") ){
     Trace("sg-cconj-debug") << "Ground eqc for LHS : " << glhs << ", based on substituion: " << std::endl;
     for( std::map< TNode, TNode >::iterator it = subs.begin(); it != subs.end(); ++it ){
-      Assert( getRepresentative( it->second )==it->second );
+      Assert(getRepresentative(it->second) == it->second);
       Trace("sg-cconj-debug") << "  " << it->first << " -> " << it->second << std::endl;
     }
   }
@@ -1398,7 +1401,7 @@ bool ConjectureGenerator::notifySubstitution( TNode glhs, std::map< TNode, TNode
 
 
 void TermGenerator::reset( TermGenEnv * s, TypeNode tn ) {
-  Assert( d_children.empty() );
+  Assert(d_children.empty());
   d_typ = tn;
   d_status = 0;
   d_status_num = 0;
@@ -1496,14 +1499,14 @@ bool TermGenerator::getNextTerm( TermGenEnv * s, unsigned depth ) {
       return s->considerCurrentTermCanon( d_id ) ? true : getNextTerm( s, depth );
       //return true;
     }else{
-      Assert( d_status_child_num<(int)s->d_func_args[f].size() );
+      Assert(d_status_child_num < (int)s->d_func_args[f].size());
       if( d_status_child_num==(int)d_children.size() ){
         d_children.push_back( s->d_tg_id );
-        Assert( s->d_tg_alloc.find( s->d_tg_id )==s->d_tg_alloc.end() );
+        Assert(s->d_tg_alloc.find(s->d_tg_id) == s->d_tg_alloc.end());
         s->d_tg_alloc[d_children[d_status_child_num]].reset( s, s->d_func_args[f][d_status_child_num] );
         return getNextTerm( s, depth );
       }else{
-        Assert( d_status_child_num+1==(int)d_children.size() );
+        Assert(d_status_child_num + 1 == (int)d_children.size());
         if( s->d_tg_alloc[d_children[d_status_child_num]].getNextTerm( s, depth-1 ) ){
           d_status_child_num++;
           return getNextTerm( s, depth );
@@ -1520,7 +1523,7 @@ bool TermGenerator::getNextTerm( TermGenEnv * s, unsigned depth ) {
   }else if( d_status==1 || d_status==3 ){
     if( d_status==1 ){
       s->removeVar( d_typ );
-      Assert( d_status_num==(int)s->d_var_id[d_typ] );
+      Assert(d_status_num == (int)s->d_var_id[d_typ]);
       //check if there is only one feasible equivalence class.  if so, don't make pattern any more specific.
       //unsigned i = s->d_ccand_eqc[0].size()-1;
       //if( s->d_ccand_eqc[0][i].size()==1 && s->d_ccand_eqc[1][i].empty() ){
@@ -1533,7 +1536,7 @@ bool TermGenerator::getNextTerm( TermGenEnv * s, unsigned depth ) {
     d_status_num = -1;
     return getNextTerm( s, depth );
   }else{
-    Assert( d_children.empty() );
+    Assert(d_children.empty());
     return false;
   }
 }
@@ -1598,7 +1601,7 @@ bool TermGenerator::getNextMatch( TermGenEnv * s, TNode eqc, std::map< TypeNode,
           return false;
         }
       }
-      Assert( subs[d_typ].find( d_status_num )==subs[d_typ].end() );
+      Assert(subs[d_typ].find(d_status_num) == subs[d_typ].end());
       subs[d_typ][d_status_num] = eqc;
       return true;
     }else{
@@ -1612,9 +1615,9 @@ bool TermGenerator::getNextMatch( TermGenEnv * s, TNode eqc, std::map< TypeNode,
   }else if( d_status==2 ){
     if( d_match_status==0 ){
       d_match_status++;
-      Assert( d_status_num<(int)s->getNumTgVars( d_typ ) );
+      Assert(d_status_num < (int)s->getNumTgVars(d_typ));
       std::map< unsigned, TNode >::iterator it = subs[d_typ].find( d_status_num );
-      Assert( it!=subs[d_typ].end() );
+      Assert(it != subs[d_typ].end());
       return it->second==eqc;
     }else{
       return false;
@@ -1630,7 +1633,7 @@ bool TermGenerator::getNextMatch( TermGenEnv * s, TNode eqc, std::map< TypeNode,
         if( d_match_status_child_num==0 ){
           //initial binding
           TNode f = s->getTgFunc( d_typ, d_status_num );
-          Assert( !eqc.isNull() );
+          Assert(!eqc.isNull());
           TNodeTrie* tat = s->getTermDatabase()->getTermArgTrie(eqc, f);
           if( tat ){
             d_match_children.push_back( tat->d_data.begin() );
@@ -1646,7 +1649,7 @@ bool TermGenerator::getNextMatch( TermGenEnv * s, TNode eqc, std::map< TypeNode,
         }
       }
       d_match_status++;
-      Assert( d_match_status_child_num+1==(int)d_match_children.size() );
+      Assert(d_match_status_child_num + 1 == (int)d_match_children.size());
       if( d_match_children[d_match_status_child_num]==d_match_children_end[d_match_status_child_num] ){
         //no more arguments to bind
         d_match_children.pop_back();
@@ -1667,9 +1670,10 @@ bool TermGenerator::getNextMatch( TermGenEnv * s, TNode eqc, std::map< TypeNode,
         }
       }
     }else{
-      Assert( d_match_status==1 );
-      Assert( d_match_status_child_num+1==(int)d_match_children.size() );
-      Assert( d_match_children[d_match_status_child_num]!=d_match_children_end[d_match_status_child_num] );
+      Assert(d_match_status == 1);
+      Assert(d_match_status_child_num + 1 == (int)d_match_children.size());
+      Assert(d_match_children[d_match_status_child_num]
+             != d_match_children_end[d_match_status_child_num]);
       d_match_status--;
       if( s->d_tg_alloc[d_children[d_match_status_child_num]].getNextMatch( s, d_match_children[d_match_status_child_num]->first, subs, rev_subs ) ){
         d_match_status_child_num++;
@@ -1681,7 +1685,7 @@ bool TermGenerator::getNextMatch( TermGenEnv * s, TNode eqc, std::map< TypeNode,
       }
     }
   }
-  Assert( false );
+  Assert(false);
   return false;
 }
 
@@ -1708,7 +1712,7 @@ unsigned TermGenerator::calculateGeneralizationDepth( TermGenEnv * s, std::map<
     }
     return sum;
   }else{
-    Assert( d_status==2 || d_status==1 );
+    Assert(d_status == 2 || d_status == 1);
     std::map< TypeNode, std::vector< int > >::iterator it = fvs.find( d_typ );
     if( it!=fvs.end() ){
       if( std::find( it->second.begin(), it->second.end(), d_status_num )!=it->second.end() ){
@@ -1731,7 +1735,7 @@ unsigned TermGenerator::getGeneralizationDepth( TermGenEnv * s ) {
 
 Node TermGenerator::getTerm( TermGenEnv * s ) {
   if( d_status==1 || d_status==2 ){
-    Assert( !d_typ.isNull() );
+    Assert(!d_typ.isNull());
     return s->getFreeVar( d_typ, d_status_num );
   }else if( d_status==5 ){
     Node f = s->getTgFunc( d_typ, d_status_num );
@@ -1752,7 +1756,7 @@ Node TermGenerator::getTerm( TermGenEnv * s ) {
       return NodeManager::currentNM()->mkNode( s->d_func_kind[f], children );
     }
   }else{
-    Assert( false );
+    Assert(false);
   }
   return Node::null();
 }
@@ -1833,7 +1837,7 @@ void TermGenEnv::collectSignatureInformation() {
 }
 
 void TermGenEnv::reset( unsigned depth, bool genRelevant, TypeNode tn ) {
-  Assert( d_tg_alloc.empty() );
+  Assert(d_tg_alloc.empty());
   d_tg_alloc.clear();
 
   if( genRelevant ){
@@ -1852,7 +1856,8 @@ void TermGenEnv::reset( unsigned depth, bool genRelevant, TypeNode tn ) {
 
 bool TermGenEnv::getNextTerm() {
   if( d_tg_alloc[0].getNextTerm( this, d_tg_gdepth_limit ) ){
-    Assert( (int)d_tg_alloc[0].getGeneralizationDepth( this )<=d_tg_gdepth_limit );
+    Assert((int)d_tg_alloc[0].getGeneralizationDepth(this)
+           <= d_tg_gdepth_limit);
     if( (int)d_tg_alloc[0].getGeneralizationDepth( this )!=d_tg_gdepth_limit ){
       return getNextTerm();
     }else{
@@ -1919,7 +1924,7 @@ Node TermGenEnv::getFreeVar( TypeNode tn, unsigned i ) {
 }
 
 bool TermGenEnv::considerCurrentTerm() {
-  Assert( !d_tg_alloc.empty() );
+  Assert(!d_tg_alloc.empty());
 
   //if generalization depth is too large, don't consider it
   unsigned i = d_tg_alloc.size();
@@ -1954,10 +1959,10 @@ bool TermGenEnv::considerCurrentTerm() {
     Trace("sg-gen-tg-debug") << "Filter based on relevant ground EQC";
     Trace("sg-gen-tg-debug") << ", #eqc to try = " << d_ccand_eqc[0][i-1].size() << "/" << d_ccand_eqc[1][i-1].size() << std::endl;
 
-    Assert( d_ccand_eqc[0].size()>=2 );
-    Assert( d_ccand_eqc[0].size()==d_ccand_eqc[1].size() );
-    Assert( d_ccand_eqc[0].size()==d_tg_id+1 );
-    Assert( d_tg_id==d_tg_alloc.size() );
+    Assert(d_ccand_eqc[0].size() >= 2);
+    Assert(d_ccand_eqc[0].size() == d_ccand_eqc[1].size());
+    Assert(d_ccand_eqc[0].size() == d_tg_id + 1);
+    Assert(d_tg_id == d_tg_alloc.size());
     for( unsigned r=0; r<2; r++ ){
       d_ccand_eqc[r][i].clear();
     }
@@ -2018,13 +2023,13 @@ void TermGenEnv::changeContext( bool add ) {
       d_ccand_eqc[r].pop_back();
     }
     d_tg_id--;
-    Assert( d_tg_alloc.find( d_tg_id )!=d_tg_alloc.end() );
+    Assert(d_tg_alloc.find(d_tg_id) != d_tg_alloc.end());
     d_tg_alloc.erase( d_tg_id );
   }
 }
 
 bool TermGenEnv::considerCurrentTermCanon( unsigned tg_id ){
-  Assert( tg_id<d_tg_alloc.size() );
+  Assert(tg_id < d_tg_alloc.size());
   if( options::conjectureFilterCanonical() ){
     //check based on a canonicity of the term (if there is one)
     Trace("sg-gen-tg-debug") << "Consider term canon ";
@@ -2081,7 +2086,7 @@ void SubstitutionIndex::addSubstitution( TNode eqc, std::vector< TNode >& vars,
   if( i==vars.size() ){
     d_var = eqc;
   }else{
-    Assert( d_var.isNull() || d_var==vars[i] );
+    Assert(d_var.isNull() || d_var == vars[i]);
     d_var = vars[i];
     d_children[terms[i]].addSubstitution( eqc, vars, terms, i+1 );
   }
@@ -2089,10 +2094,10 @@ void SubstitutionIndex::addSubstitution( TNode eqc, std::vector< TNode >& vars,
 
 bool SubstitutionIndex::notifySubstitutions( ConjectureGenerator * s, std::map< TNode, TNode >& subs, TNode rhs, unsigned numVars, unsigned i ) {
   if( i==numVars ){
-    Assert( d_children.empty() );
+    Assert(d_children.empty());
     return s->notifySubstitution( d_var, subs, rhs );
   }else{
-    Assert( i==0 || !d_children.empty() );
+    Assert(i == 0 || !d_children.empty());
     for( std::map< TNode, SubstitutionIndex >::iterator it = d_children.begin(); it != d_children.end(); ++it ){
       Trace("sg-cconj-debug2") << "Try " << d_var << " -> " << it->first << " (" << i << "/" << numVars << ")" << std::endl;
       subs[d_var] = it->first;
@@ -2130,9 +2135,9 @@ void TheoremIndex::addTheoremNode( TNode curr, std::vector< TNode >& lhs_v, std:
     lhs_arg.push_back( 0 );
     d_children[curr.getOperator()].addTheorem( lhs_v, lhs_arg, rhs );
   }else{
-    Assert( curr.getKind()==kind::BOUND_VARIABLE );
+    Assert(curr.getKind() == kind::BOUND_VARIABLE);
     TypeNode tn = curr.getType();
-    Assert( d_var[tn].isNull() || d_var[tn]==curr );
+    Assert(d_var[tn].isNull() || d_var[tn] == curr);
     d_var[tn] = curr;
     d_children[curr].addTheorem( lhs_v, lhs_arg, rhs );
   }
@@ -2180,7 +2185,7 @@ void TheoremIndex::getEquivalentTermsNode( Node curr, std::vector< TNode >& n_v,
   std::map< TypeNode, TNode >::iterator itt = d_var.find( tn );
   if( itt!=d_var.end() ){
     Trace("thm-db-debug") << "Check for substitution with " << itt->second << "..." << std::endl;
-    Assert( curr.getType()==itt->second.getType() );
+    Assert(curr.getType() == itt->second.getType());
     //add to substitution if possible
     bool success = false;
     std::map< TNode, TNode >::iterator it = smap.find( itt->second );
diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp
index 3be1d4a4b..3a075ec8a 100644
--- a/src/theory/quantifiers/ematching/candidate_generator.cpp
+++ b/src/theory/quantifiers/ematching/candidate_generator.cpp
@@ -40,7 +40,7 @@ CandidateGeneratorQE::CandidateGeneratorQE(QuantifiersEngine* qe, Node pat)
       d_mode(cand_term_none)
 {
   d_op = qe->getTermDatabase()->getMatchOperator( pat );
-  Assert( !d_op.isNull() );
+  Assert(!d_op.isNull());
 }
 
 void CandidateGeneratorQE::resetInstantiationRound(){
@@ -130,8 +130,7 @@ Node CandidateGeneratorQE::getNextCandidate(){
 
 CandidateGeneratorQELitDeq::CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat ) :
 CandidateGenerator( qe ), d_match_pattern( mpat ){
-
-  Assert( d_match_pattern.getKind()==EQUAL );
+  Assert(d_match_pattern.getKind() == EQUAL);
   d_match_pattern_type = d_match_pattern[0].getType();
 }
 
@@ -161,7 +160,7 @@ Node CandidateGeneratorQELitDeq::getNextCandidate(){
 CandidateGeneratorQEAll::CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mpat ) :
   CandidateGenerator( qe ), d_match_pattern( mpat ){
   d_match_pattern_type = mpat.getType();
-  Assert( mpat.getKind()==INST_CONSTANT );
+  Assert(mpat.getKind() == INST_CONSTANT);
   d_f = quantifiers::TermUtil::getInstConstAttr( mpat );
   d_index = mpat.getAttribute(InstVarNumAttribute());
   d_firstTime = false;
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp
index 9e76a6a31..e639dc446 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp
@@ -43,7 +43,7 @@ InstMatchGenerator::InstMatchGenerator( Node pat ){
   d_cg = NULL;
   d_needsReset = true;
   d_active_add = true;
-  Assert( quantifiers::TermUtil::hasInstConstAttr(pat) );
+  Assert(quantifiers::TermUtil::hasInstConstAttr(pat));
   d_pattern = pat;
   d_match_pattern = pat;
   d_match_pattern_type = pat.getType();
@@ -258,7 +258,7 @@ int InstMatchGenerator::getMatch(
 {
   Trace("matching") << "Matching " << t << " against pattern " << d_match_pattern << " ("
                     << m << ")" << ", " << d_children.size() << ", pattern is " << d_pattern << std::endl;
-  Assert( !d_match_pattern.isNull() );
+  Assert(!d_match_pattern.isNull());
   if (d_cg == nullptr)
   {
     Trace("matching-fail") << "Internal error for match generator." << std::endl;
@@ -270,10 +270,12 @@ int InstMatchGenerator::getMatch(
     //InstMatch prev( &m );
     std::vector< int > prev;
     //if t is null
-    Assert( !t.isNull() );
-    Assert( !quantifiers::TermUtil::hasInstConstAttr(t) );
-    Assert( d_match_pattern.getKind()==INST_CONSTANT || t.getKind()==d_match_pattern.getKind() );
-    Assert( !Trigger::isAtomicTrigger( d_match_pattern ) || t.getOperator()==d_match_pattern.getOperator() );
+    Assert(!t.isNull());
+    Assert(!quantifiers::TermUtil::hasInstConstAttr(t));
+    Assert(d_match_pattern.getKind() == INST_CONSTANT
+           || t.getKind() == d_match_pattern.getKind());
+    Assert(!Trigger::isAtomicTrigger(d_match_pattern)
+           || t.getOperator() == d_match_pattern.getOperator());
     //first, check if ground arguments are not equal, or a match is in conflict
     Trace("matching-debug2") << "Setting immediate matches..." << std::endl;
     for (unsigned i = 0, size = d_match_pattern.getNumChildren(); i < size; i++)
@@ -338,7 +340,7 @@ int InstMatchGenerator::getMatch(
           if( t.getType().isBoolean() ){
             t_match = NodeManager::currentNM()->mkConst( !q->areEqual( qe->getTermUtil()->d_true, t ) );
           }else{
-            Assert( t.getType().isReal() );
+            Assert(t.getType().isReal());
             t_match = NodeManager::currentNM()->mkNode(PLUS, t, qe->getTermUtil()->d_one);
           }
         }else if( pat.getKind()==GEQ ){
@@ -467,7 +469,7 @@ int InstMatchGenerator::getNextMatch(Node f,
     //if t not null, try to fit it into match m
     if( !t.isNull() ){
       if( d_curr_exclude_match.find( t )==d_curr_exclude_match.end() ){
-        Assert( t.getType().isComparableTo( d_match_pattern_type ) );
+        Assert(t.getType().isComparableTo(d_match_pattern_type));
         Trace("matching-summary") << "Try " << d_match_pattern << " : " << t << std::endl;
         success = getMatch(f, t, m, qe, tparent);
         if( d_independent_gen && success<0 ){
@@ -533,11 +535,11 @@ InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( Node q, Node pat,
 }
 
 InstMatchGenerator* InstMatchGenerator::mkInstMatchGeneratorMulti( Node q, std::vector< Node >& pats, QuantifiersEngine* qe ) {
-  Assert( pats.size()>1 );
+  Assert(pats.size() > 1);
   InstMatchGeneratorMultiLinear * imgm = new InstMatchGeneratorMultiLinear( q, pats, qe );
   std::vector< InstMatchGenerator* > gens;
   imgm->initialize(q, qe, gens);
-  Assert( gens.size()==pats.size() );
+  Assert(gens.size() == pats.size());
   std::vector< Node > patsn;
   std::map< Node, InstMatchGenerator * > pat_map_init;
   for( unsigned i=0; i<gens.size(); i++ ){
@@ -704,7 +706,7 @@ InstMatchGeneratorMultiLinear::InstMatchGeneratorMultiLinear( Node q, std::vecto
   for( unsigned i=0; i<pats_ordered.size(); i++ ){
     Trace("multi-trigger-linear") << "...make for " << pats_ordered[i] << std::endl;
     InstMatchGenerator* cimg = getInstMatchGenerator(q, pats_ordered[i]);
-    Assert( cimg!=NULL );
+    Assert(cimg != NULL);
     d_children.push_back( cimg );
     if( i==0 ){  //TODO : improve
       cimg->setIndependent();
@@ -722,7 +724,7 @@ int InstMatchGeneratorMultiLinear::resetChildren( QuantifiersEngine* qe ){
 }
 
 bool InstMatchGeneratorMultiLinear::reset( Node eqc, QuantifiersEngine* qe ) {
-  Assert( eqc.isNull() );
+  Assert(eqc.isNull());
   if( options::multiTriggerLinear() ){
     return true;
   }else{
@@ -744,7 +746,7 @@ int InstMatchGeneratorMultiLinear::getNextMatch(Node q,
     }
   }
   Trace("multi-trigger-linear-debug") << "InstMatchGeneratorMultiLinear::getNextMatch : continue match " << std::endl;
-  Assert( d_next!=NULL );
+  Assert(d_next != NULL);
   int ret_val = continueNextMatch(q, m, qe, tparent);
   if( ret_val>0 ){
     Trace("multi-trigger-linear") << "Successful multi-trigger instantiation." << std::endl;
@@ -924,7 +926,7 @@ void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe,
                                                        int endChildIndex,
                                                        bool modEq)
 {
-  Assert( !qe->inConflict() );
+  Assert(!qe->inConflict());
   if( childIndex==endChildIndex ){
     // m is an instantiation
     if (sendInstantiation(tparent, m))
@@ -1036,9 +1038,9 @@ InstMatchGeneratorSimple::InstMatchGeneratorSimple(Node q,
   if( d_match_pattern.getKind()==EQUAL ){
     d_eqc = d_match_pattern[1];
     d_match_pattern = d_match_pattern[0];
-    Assert( !quantifiers::TermUtil::hasInstConstAttr( d_eqc ) );
+    Assert(!quantifiers::TermUtil::hasInstConstAttr(d_eqc));
   }
-  Assert( Trigger::isSimpleTrigger( d_match_pattern ) );
+  Assert(Trigger::isSimpleTrigger(d_match_pattern));
   for( unsigned i=0; i<d_match_pattern.getNumChildren(); i++ ){
     if( d_match_pattern[i].getKind()==INST_CONSTANT ){
       if( !options::cbqi() || quantifiers::TermUtil::getInstConstAttr(d_match_pattern[i])==q ){
@@ -1105,7 +1107,7 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m,
   Debug("simple-trigger-debug") << "Add inst " << argIndex << " " << d_match_pattern << std::endl;
   if (argIndex == d_match_pattern.getNumChildren())
   {
-    Assert( !tat->d_data.empty() );
+    Assert(!tat->d_data.empty());
     TNode t = tat->getData();
     Debug("simple-trigger") << "Actual term is " << t << std::endl;
     //convert to actual used terms
@@ -1135,7 +1137,8 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m,
           Node t = tt.first;
           Node prev = m.get( v );
           //using representatives, just check if equal
-          Assert( t.getType().isComparableTo( d_match_pattern_arg_types[argIndex] ) );
+          Assert(
+              t.getType().isComparableTo(d_match_pattern_arg_types[argIndex]));
           if( prev.isNull() || prev==t ){
             m.setValue( v, t);
             addInstantiations(m, qe, addedLemmas, argIndex + 1, &(tt.second));
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
index 876e4e369..3420f282d 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
@@ -125,7 +125,7 @@ int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){
 }
 
 void InstStrategyUserPatterns::addUserPattern( Node q, Node pat ){
-  Assert( pat.getKind()==INST_PATTERN );
+  Assert(pat.getKind() == INST_PATTERN);
   //add to generators
   bool usable = true;
   std::vector< Node > nodes;
@@ -308,7 +308,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
       if( Trace.isOn("auto-gen-trigger-debug") ){
         Trace("auto-gen-trigger-debug") << "Collected pat terms for " << bd << ", no-patterns : " << d_user_no_gen[f].size() << std::endl;
         for( unsigned i=0; i<patTermsF.size(); i++ ){
-          Assert( tinfo.find( patTermsF[i] )!=tinfo.end() );
+          Assert(tinfo.find(patTermsF[i]) != tinfo.end());
           Trace("auto-gen-trigger-debug") << "   " << patTermsF[i] << std::endl;
           Trace("auto-gen-trigger-debug2") << "     info = [" << tinfo[patTermsF[i]].d_reqPol << ", " << tinfo[patTermsF[i]].d_reqPolEq << ", " << tinfo[patTermsF[i]].d_fv.size() << "]" << std::endl;
         }
@@ -320,7 +320,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
     std::map< Node, bool > rmPatTermsF;
     int last_weight = -1;
     for( unsigned i=0; i<patTermsF.size(); i++ ){
-      Assert( patTermsF[i].getKind()!=NOT );
+      Assert(patTermsF[i].getKind() != NOT);
       bool newVar = false;
       for( unsigned j=0; j<tinfo[ patTermsF[i] ].d_fv.size(); j++ ){
         if( vcMap.find( tinfo[ patTermsF[i] ].d_fv[j] )==vcMap.end() ){
@@ -362,17 +362,17 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
         Trace("auto-gen-trigger-debug") << "...processing pattern " << pat << std::endl;
         Node mpat = pat;
         //process the pattern: if it has a required polarity, consider it
-        Assert( tinfo.find( pat )!=tinfo.end() );
+        Assert(tinfo.find(pat) != tinfo.end());
         int rpol = tinfo[pat].d_reqPol;
         Node rpoleq = tinfo[pat].d_reqPolEq;
         unsigned num_fv = tinfo[pat].d_fv.size();
         Trace("auto-gen-trigger-debug") << "...required polarity for " << pat << " is " << rpol << ", eq=" << rpoleq << std::endl;
         if( rpol!=0 ){
-          Assert( rpol==1 || rpol==-1 );
+          Assert(rpol == 1 || rpol == -1);
           if( Trigger::isRelationalTrigger( pat ) ){
             pat = rpol==-1 ? pat.negate() : pat;
           }else{
-            Assert( Trigger::isAtomicTrigger( pat ) );
+            Assert(Trigger::isAtomicTrigger(pat));
             if( pat.getType().isBoolean() && rpoleq.isNull() ){
               if( options::literalMatchMode()==LITERAL_MATCH_USE ){
                 pat = NodeManager::currentNM()->mkNode( EQUAL, pat, NodeManager::currentNM()->mkConst( rpol==-1 ) ).negate();
@@ -380,7 +380,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
                 pat = NodeManager::currentNM()->mkNode( EQUAL, pat, NodeManager::currentNM()->mkConst( rpol==1 ) );
               }
             }else{
-              Assert( !rpoleq.isNull() );
+              Assert(!rpoleq.isNull());
               if( rpol==-1 ){
                 if( options::literalMatchMode()!=LITERAL_MATCH_NONE ){
                   //all equivalence classes except rpoleq
@@ -436,8 +436,8 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
         sortQuantifiersForSymbol sqfs;
         sqfs.d_quant_rel = d_quant_rel;
         for( unsigned i=0; i<patTerms.size(); i++ ){
-          Assert( d_pat_to_mpat.find( patTerms[i] )!=d_pat_to_mpat.end() );
-          Assert( d_pat_to_mpat[patTerms[i]].hasOperator() );
+          Assert(d_pat_to_mpat.find(patTerms[i]) != d_pat_to_mpat.end());
+          Assert(d_pat_to_mpat[patTerms[i]].hasOperator());
           sqfs.d_op_map[ patTerms[i] ] = d_pat_to_mpat[patTerms[i]].getOperator();
         }        
         //sort based on # occurrences (this will cause Trigger to select rarer symbols)
@@ -591,7 +591,7 @@ bool InstStrategyAutoGenTriggers::hasUserPatterns( Node q ) {
 }
 
 void InstStrategyAutoGenTriggers::addUserNoPattern( Node q, Node pat ) {
-  Assert( pat.getKind()==INST_NO_PATTERN && pat.getNumChildren()==1 );
+  Assert(pat.getKind() == INST_NO_PATTERN && pat.getNumChildren() == 1);
   if( std::find( d_user_no_gen[q].begin(), d_user_no_gen[q].end(), pat[0] )==d_user_no_gen[q].end() ){
     Trace("user-pat") << "Add user no-pattern: " << pat[0] << " for " << q << std::endl;
     d_user_no_gen[q].push_back( pat[0] );
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp
index 2fe28fc61..23b1ff6c9 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.cpp
+++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp
@@ -145,7 +145,7 @@ void InstantiationEngine::check(Theory::Effort e, QEffort quant_e)
       unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting();
       doInstantiationRound( e );
       if( d_quantEngine->inConflict() ){
-        Assert( d_quantEngine->getNumLemmasWaiting()>lastWaiting );
+        Assert(d_quantEngine->getNumLemmasWaiting() > lastWaiting);
         Trace("inst-engine") << "Conflict, added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl;
       }else if( d_quantEngine->hasAddedLemma() ){
         Trace("inst-engine") << "Added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting)  << std::endl;
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index 201aad3a0..f539bccf5 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -144,7 +144,7 @@ bool Trigger::mkTriggerTerms( Node q, std::vector< Node >& nodes, unsigned n_var
     bool foundVar = false;
     for( unsigned j=0; j<varContains[ temp[i] ].size(); j++ ){
       Node v = varContains[ temp[i] ][j];
-      Assert( quantifiers::TermUtil::getInstConstAttr(v)==q );
+      Assert(quantifiers::TermUtil::getInstConstAttr(v) == q);
       if( vars.find( v )==vars.end() ){
         varCount++;
         vars[ v ] = true;
@@ -282,7 +282,7 @@ bool Trigger::isUsable( Node n, Node q ){
 }
 
 Node Trigger::getIsUsableEq( Node q, Node n ) {
-  Assert( isRelationalTrigger( n ) );
+  Assert(isRelationalTrigger(n));
   for( unsigned i=0; i<2; i++) {
     if( isUsableEqTerms( q, n[i], n[1-i] ) ){
       if( i==1 && n.getKind()==EQUAL && !quantifiers::TermUtil::hasInstConstAttr(n[0]) ){
@@ -451,8 +451,8 @@ void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Nod
         }
       }
       if( !nu.isNull() ){
-        Assert( nu==n );
-        Assert( nu.getKind()!=NOT );
+        Assert(nu == n);
+        Assert(nu.getKind() != NOT);
         Trace("auto-gen-trigger-debug2") << "...found usable trigger : " << nu << std::endl;
         Node reqEq;
         if( nu.getKind()==EQUAL ){
@@ -463,8 +463,9 @@ void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Nod
             nu = nu[0];
           }
         }
-        Assert( reqEq.isNull() || !quantifiers::TermUtil::hasInstConstAttr( reqEq ) );
-        Assert( isUsableTrigger( nu, q ) );
+        Assert(reqEq.isNull()
+               || !quantifiers::TermUtil::hasInstConstAttr(reqEq));
+        Assert(isUsableTrigger(nu, q));
         //tinfo.find( nu )==tinfo.end()
         Trace("auto-gen-trigger-debug2") << "...add usable trigger : " << nu << std::endl;
         tinfo[ nu ].init( q, nu, hasEPol ? ( epol ? 1 : -1 ) : 0, reqEq );
@@ -484,7 +485,7 @@ void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Nod
         bool rm_nu = false;
         for( unsigned i=0; i<added2.size(); i++ ){
           Trace("auto-gen-trigger-debug2") << "..." << nu << " added child " << i << " : " << added2[i] << std::endl;
-          Assert( added2[i]!=nu );
+          Assert(added2[i] != nu);
           // if child was not already removed
           if( tinfo.find( added2[i] )!=tinfo.end() ){
             if( tstrt==quantifiers::TRIGGER_SEL_MAX || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_MAX && !nu_single ) ){
@@ -839,7 +840,7 @@ Node Trigger::getInversion( Node n, Node x ) {
         if( n.getKind()==PLUS ){
           x = NodeManager::currentNM()->mkNode( MINUS, x, n[i] );
         }else if( n.getKind()==MULT ){
-          Assert( n[i].isConst() );
+          Assert(n[i].isConst());
           if( x.getType().isInteger() ){
             Node coeff = NodeManager::currentNM()->mkConst( n[i].getConst<Rational>().abs() );
             if( !n[i].getConst<Rational>().abs().isOne() ){
diff --git a/src/theory/quantifiers/equality_infer.cpp b/src/theory/quantifiers/equality_infer.cpp
index ef80af5f5..66745c94a 100644
--- a/src/theory/quantifiers/equality_infer.cpp
+++ b/src/theory/quantifiers/equality_infer.cpp
@@ -97,7 +97,7 @@ Node EqualityInference::getMaster( Node t, EqcInfo * eqc, bool& updated, Node ne
         return t;
       }
     }else{
-      Assert( d_eqci.find( eqc->d_master.get() )!=d_eqci.end() );
+      Assert(d_eqci.find(eqc->d_master.get()) != d_eqci.end());
       EqcInfo * eqc_m = d_eqci[eqc->d_master.get()];
       Node m = getMaster( eqc->d_master.get(), eqc_m, updated, new_m );
       eqc->d_master = m;
@@ -141,7 +141,7 @@ void EqualityInference::eqNotifyNewClass(TNode t) {
     }else{
       eqci = itec->second;
     }
-    Assert( !eqci->d_valid.get() );
+    Assert(!eqci->d_valid.get());
     if( !eqci->d_solved.get() ){
       //somewhat strange: t may not be in rewritten form    
       Node r = Rewriter::rewrite( t );
@@ -160,16 +160,16 @@ void EqualityInference::eqNotifyNewClass(TNode t) {
             BoolMap::const_iterator itv = d_elim_vars.find( n );
             if( itv!=d_elim_vars.end() ){
               changed = true;
-              Assert( d_eqci.find( n )!=d_eqci.end() );
-              Assert( n!=t );
-              Assert( d_eqci[n]->d_solved.get() );
+              Assert(d_eqci.find(n) != d_eqci.end());
+              Assert(n != t);
+              Assert(d_eqci[n]->d_solved.get());
               Trace("eq-infer-debug2") << "......its solved form is " << d_eqci[n]->d_rep.get() << std::endl;
               if( d_trackExplain ){
                 //track the explanation: justified by explanation for each substitution
                 addToExplanationEqc( exp, n );
               }
               n = d_eqci[n]->d_rep;
-              Assert( !n.isNull() );
+              Assert(!n.isNull());
             }
             if( it->second.isNull() ){
               children.push_back( n );
@@ -177,7 +177,7 @@ void EqualityInference::eqNotifyNewClass(TNode t) {
               children.push_back( NodeManager::currentNM()->mkNode( MULT, it->second, n ) );
             }
           }else{
-            Assert( !it->second.isNull() );
+            Assert(!it->second.isNull());
             children.push_back( it->second );
           }
         }
@@ -275,8 +275,8 @@ void EqualityInference::setEqcRep( Node t, Node r, std::vector< Node >& exp_to_a
 }
 
 void EqualityInference::eqNotifyMerge(TNode t1, TNode t2) {
-  Assert( !t1.isNull() );
-  Assert( !t2.isNull() );
+  Assert(!t1.isNull());
+  Assert(!t2.isNull());
   std::map< Node, EqcInfo * >::iterator itv1 = d_eqci.find( t1 );
   if( itv1!=d_eqci.end() ){
     std::map< Node, EqcInfo * >::iterator itv2 = d_eqci.find( t2 );
@@ -324,7 +324,7 @@ void EqualityInference::eqNotifyMerge(TNode t1, TNode t2) {
             {
               Node v_value = veq[1];
               Trace("eq-infer") << "...solved " << v_solve << " == " << v_value << std::endl;
-              Assert( d_elim_vars.find( v_solve )==d_elim_vars.end() );
+              Assert(d_elim_vars.find(v_solve) == d_elim_vars.end());
               d_elim_vars[v_solve] = true;
               //store value in eqc info
               EqcInfo * eqci_solved;
diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp
index bb0306c06..f7fd13d4d 100644
--- a/src/theory/quantifiers/equality_query.cpp
+++ b/src/theory/quantifiers/equality_query.cpp
@@ -105,7 +105,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a,
           if( r.getType().isSort() ){
             Trace("internal-rep-warn") << "No representative for UF constant." << std::endl;
             //should never happen : UF constants should never escape model
-            Assert( false );
+            Assert(false);
           }
         }
       }
@@ -165,7 +165,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a,
         d_rep_score[ r_best ] = d_reset_count;
       }
       Trace("internal-rep-select") << "...Choose " << r_best << " with score " << r_best_score << std::endl;
-      Assert( r_best.getType().isSubtypeOf( v_tn ) );
+      Assert(r_best.getType().isSubtypeOf(v_tn));
       v_int_rep[r] = r_best;
       if( r_best!=a ){
         Trace("internal-rep-debug") << "rep( " << a << " ) = " << r << ", " << std::endl;
@@ -193,7 +193,7 @@ void EqualityQueryQuantifiersEngine::getEquivalenceClass( Node a, std::vector< N
     eqc.push_back( a );
   }
   //a should be in its equivalence class
-  Assert( std::find( eqc.begin(), eqc.end(), a )!=eqc.end() );
+  Assert(std::find(eqc.begin(), eqc.end(), a) != eqc.end());
 }
 
 TNode EqualityQueryQuantifiersEngine::getCongruentTerm( Node f, std::vector< TNode >& args ) {
@@ -243,7 +243,7 @@ int EqualityQueryQuantifiersEngine::getRepScore(Node n,
       //score prefers earliest use of this term as a representative
       return d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n];
     }else{
-      Assert( options::quantRepMode()==quantifiers::QUANT_REP_MODE_DEPTH );
+      Assert(options::quantRepMode() == quantifiers::QUANT_REP_MODE_DEPTH);
       return quantifiers::TermUtil::getTermDepth( n );
     }
   }
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 4b8b65697..bfef42b65 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -46,7 +46,7 @@ void FirstOrderModel::assertQuantifier( Node n ){
   if( n.getKind()==FORALL ){
     d_forall_asserts.push_back( n );
   }else if( n.getKind()==NOT ){
-    Assert( n[0].getKind()==FORALL );
+    Assert(n[0].getKind() == FORALL);
   }
 }
 
@@ -58,7 +58,7 @@ Node FirstOrderModel::getAssertedQuantifier( unsigned i, bool ordered ) {
   if( !ordered ){
     return d_forall_asserts[i]; 
   }else{
-    Assert( d_forall_rlv_assert.size()==d_forall_asserts.size() );
+    Assert(d_forall_rlv_assert.size() == d_forall_asserts.size());
     return d_forall_rlv_assert[i];
   }
 }
@@ -186,7 +186,7 @@ void FirstOrderModel::reset_round() {
       }
     }
     Trace("fm-relevant-debug") << "Sizes : " << d_forall_rlv_assert.size() << " " << d_forall_asserts.size() << std::endl;
-    Assert( d_forall_rlv_assert.size()==d_forall_asserts.size() );
+    Assert(d_forall_rlv_assert.size() == d_forall_asserts.size());
   }else{
     for( unsigned i=0; i<d_forall_asserts.size(); i++ ){
       d_forall_rlv_assert.push_back( d_forall_asserts[i] );
@@ -225,7 +225,7 @@ bool FirstOrderModel::isQuantifierActive(TNode q) const
 
 bool FirstOrderModel::isQuantifierAsserted(TNode q) const
 {
-  Assert( d_forall_rlv_assert.size()==d_forall_asserts.size() );
+  Assert(d_forall_rlv_assert.size() == d_forall_asserts.size());
   return std::find( d_forall_rlv_assert.begin(), d_forall_rlv_assert.end(), q )!=d_forall_rlv_assert.end();
 }
 
@@ -395,7 +395,7 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) {
   for( int i=(d_models[op]->d_cond.size()-1); i>=0; i--) {
     Node v = d_models[op]->d_value[i];
     Trace("fmc-model-func") << "Value is : " << v << std::endl;
-    Assert( v.isConst() );
+    Assert(v.isConst());
     /*
     if( !hasTerm( v ) ){
       //can happen when the model basis term does not exist in ground assignment
@@ -431,7 +431,7 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) {
           children.push_back( NodeManager::currentNM()->mkNode( EQUAL, vars[j], c ) );
         }
       }
-      Assert( !children.empty() );
+      Assert(!children.empty());
       Node cc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( AND, children );
 
       Trace("fmc-model-func") << "condition : " << cc << ", value : " << v << std::endl;
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index 87f0b1ffe..c6800b092 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -167,7 +167,7 @@ void BoundedIntegers::process( Node q, Node n, bool pol,
         conj = TermUtil::simpleNegate( conj );
       }
       Trace("bound-int-debug") << "Process possible finite disequality conjunction : " << conj << std::endl;
-      Assert( conj.getKind()==AND );
+      Assert(conj.getKind() == AND);
       Node v;
       std::vector< Node > v_cases;
       bool success = true;
@@ -199,7 +199,7 @@ void BoundedIntegers::process( Node q, Node n, bool pol,
           bound_lit_type_map[v] = BOUND_FIXED_SET;
           bound_lit_map[3][v] = n;
           bound_lit_pol_map[3][v] = pol;
-          Assert( v_cases.size()==1 );
+          Assert(v_cases.size() == 1);
           bound_fixed_set[v].clear();
           bound_fixed_set[v].push_back( v_cases[0] );
         }
@@ -266,7 +266,7 @@ void BoundedIntegers::process( Node q, Node n, bool pol,
       }
     }
   }else{
-    Assert( n.getKind()!=LEQ && n.getKind()!=LT && n.getKind()!=GT );
+    Assert(n.getKind() != LEQ && n.getKind() != LT && n.getKind() != GT);
   }
 }
 
@@ -335,7 +335,8 @@ void BoundedIntegers::checkOwnership(Node f)
             setBoundVar = true;
             for( unsigned b=0; b<2; b++ ){
               //set the bounds
-              Assert( bound_int_range_term[b].find( v )!=bound_int_range_term[b].end() );
+              Assert(bound_int_range_term[b].find(v)
+                     != bound_int_range_term[b].end());
               d_bounds[b][f][v] = bound_int_range_term[b][v];
             }
             Node r = nm->mkNode(MINUS, d_bounds[1][f][v], d_bounds[0][f][v]);
@@ -396,7 +397,7 @@ void BoundedIntegers::checkOwnership(Node f)
             }
             else
             {
-              Assert( it->second!=BOUND_INT_RANGE );
+              Assert(it->second != BOUND_INT_RANGE);
             }
           }
         }
@@ -424,7 +425,7 @@ void BoundedIntegers::checkOwnership(Node f)
     for( unsigned i=0; i<f[0].getNumChildren(); i++) {
       Node v = f[0][i];
       if( std::find( d_set[f].begin(), d_set[f].end(), v )!=d_set[f].end() ){
-        Assert( d_bound_type[f].find( v )!=d_bound_type[f].end() );
+        Assert(d_bound_type[f].find(v) != d_bound_type[f].end());
         if( d_bound_type[f][v]==BOUND_INT_RANGE ){
           Trace("bound-int") << "  " << d_bounds[0][f][v] << " <= " << v << " <= " << d_bounds[1][f][v] << " (range is " << d_range[f][v] << ")" << std::endl;
         }else if( d_bound_type[f][v]==BOUND_SET_MEMBER ){
@@ -446,7 +447,7 @@ void BoundedIntegers::checkOwnership(Node f)
           Trace("bound-int") << "  " << v << " has small finite type." << std::endl;
         }else{
           Trace("bound-int") << "  " << v << " has unknown bound." << std::endl;
-          Assert( false );
+          Assert(false);
         }
       }else{
         Trace("bound-int") << "  " << "*** " << v << " is unbounded." << std::endl;
@@ -470,7 +471,7 @@ void BoundedIntegers::checkOwnership(Node f)
       std::map< Node, Node >::iterator itr = d_range[f].find( v );
       if( itr != d_range[f].end() ){
         Node r = itr->second;
-        Assert( !r.isNull() );
+        Assert(!r.isNull());
         bool isProxy = false;
         if (expr::hasBoundVar(r))
         {
@@ -695,16 +696,16 @@ Node BoundedIntegers::getSetRangeValue( Node q, Node v, RepSetIterator * rsi ) {
 bool BoundedIntegers::getRsiSubsitution( Node q, Node v, std::vector< Node >& vars, std::vector< Node >& subs, RepSetIterator * rsi ) {
 
   Trace("bound-int-rsi") << "Get bound value in model of variable " << v << std::endl;
-  Assert( d_set_nums[q].find( v )!=d_set_nums[q].end() );
+  Assert(d_set_nums[q].find(v) != d_set_nums[q].end());
   int vindex = d_set_nums[q][v];
-  Assert( d_set_nums[q][v]==vindex );
+  Assert(d_set_nums[q][v] == vindex);
   Trace("bound-int-rsi-debug") << "  index order is " << vindex << std::endl;
   //must take substitution for all variables that are iterating at higher level
   for( int i=0; i<vindex; i++) {
-    Assert( d_set_nums[q][d_set[q][i]]==i );
+    Assert(d_set_nums[q][d_set[q][i]] == i);
     Trace("bound-int-rsi") << "Look up the value for " << d_set[q][i] << " " << i << std::endl;
     int v = rsi->getVariableOrder( i );
-    Assert( q[0][v]==d_set[q][i] );
+    Assert(q[0][v] == d_set[q][i]);
     Node t = rsi->getCurrentTerm(v, true);
     Trace("bound-int-rsi") << "term : " << t << std::endl;
     vars.push_back( d_set[q][i] );
@@ -772,7 +773,7 @@ bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node
         Node tl = l;
         Node tu = u;
         getBounds( q, v, rsi, tl, tu );
-        Assert( !tl.isNull() && !tu.isNull() );
+        Assert(!tl.isNull() && !tu.isNull());
         if( ra==d_quantEngine->getTermUtil()->d_true ){
           long rr = range.getConst<Rational>().getNumerator().getLong()+1;
           Trace("bound-int-rsi")  << "Actual bound range is " << rr << std::endl;
@@ -797,11 +798,11 @@ bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node
         if( srv.getKind()!=EMPTYSET ){
           //collect the elements
           while( srv.getKind()==UNION ){
-            Assert( srv[1].getKind()==kind::SINGLETON );
+            Assert(srv[1].getKind() == kind::SINGLETON);
             elements.push_back( srv[1][0] );
             srv = srv[0];
           }
-          Assert( srv.getKind()==kind::SINGLETON );
+          Assert(srv.getKind() == kind::SINGLETON);
           elements.push_back( srv[0] );
           //check if we need to do matching, for literals like ( tuple( v ) in S )
           Node t = d_setm_range_lit[q][v][0];
diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index 2306a0565..f6edd3195 100644
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -443,7 +443,7 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){
         }
         if( !isStar && !ri.isConst() ){
           Trace("fmc-warn") << "Warning : model for " << op << " has non-constant argument in model " << ri << " (from " << c[i] << ")" << std::endl;
-          Assert( false );
+          Assert(false);
         }
         entry_children.push_back(ri);
       }
@@ -453,7 +453,7 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){
           << "Representative of " << v << " is " << nv << std::endl;
       if( !nv.isConst() ){
         Trace("fmc-warn") << "Warning : model for " << op << " has non-constant value in model " << nv << std::endl;
-        Assert( false );
+        Assert(false);
       }
       Node en = (useSimpleModels() && hasNonStar) ? n : NodeManager::currentNM()->mkNode( APPLY_UF, entry_children );
       if( std::find(conds.begin(), conds.end(), n )==conds.end() ){
@@ -501,13 +501,14 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){
         inst.push_back( r );
       }
       Node ev = fm->d_models[op]->evaluate( fm, inst );
-      Trace("fmc-model-debug") << ".....Checking eval( " << fm->d_uf_terms[op][i] << " ) = " << ev << std::endl;
-      AlwaysAssert( fm->areEqual( ev, fm->d_uf_terms[op][i] ) );
+      Trace("fmc-model-debug") << ".....Checking eval( " <<
+    fm->d_uf_terms[op][i] << " ) = " << ev << std::endl; AlwaysAssert(
+    fm->areEqual( ev, fm->d_uf_terms[op][i] ) );
     }
     */
   }
-  Assert( d_addedLemmas==0 );
-  
+  Assert(d_addedLemmas == 0);
+
   //make function values
   for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ){
     Node f_def = getFunctionValue( fm, it->first, "$x" );
@@ -582,7 +583,7 @@ void FullModelChecker::debugPrint(const char * tr, Node n, bool dispStar) {
 
 int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) {
   Trace("fmc") << "Full model check " << f << ", effort = " << effort << "..." << std::endl;
-  Assert( !d_qe->inConflict() );
+  Assert(!d_qe->inConflict());
   if( optUseModel() ){
     FirstOrderModelFmc * fmfmc = fm->asFirstOrderModelFmc();
     if (effort==0) {
@@ -606,7 +607,7 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i
         //model check the quantifier
         doCheck(fmfmc, f, d_quant_models[f], f[1]);
         Trace("fmc") << "Definition for quantifier " << f << " is : " << std::endl;
-        Assert( !d_quant_models[f].d_cond.empty() );
+        Assert(!d_quant_models[f].d_cond.empty());
         d_quant_models[f].debugPrint("fmc", Node::null(), this);
         Trace("fmc") << std::endl;
 
@@ -1159,7 +1160,7 @@ void FullModelChecker::doInterpretedCompose( FirstOrderModelFmc * fm, Node f, De
 
 int FullModelChecker::isCompat( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ) {
   Trace("fmc-debug3") << "isCompat " << c << std::endl;
-  Assert(cond.size()==c.getNumChildren()+1);
+  Assert(cond.size() == c.getNumChildren() + 1);
   for (unsigned i=1; i<cond.size(); i++) {
     if (cond[i] != c[i - 1] && !fm->isStar(cond[i]) && !fm->isStar(c[i - 1]))
     {
@@ -1171,7 +1172,7 @@ int FullModelChecker::isCompat( FirstOrderModelFmc * fm, std::vector< Node > & c
 
 bool FullModelChecker::doMeet( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ) {
   Trace("fmc-debug3") << "doMeet " << c << std::endl;
-  Assert(cond.size()==c.getNumChildren()+1);
+  Assert(cond.size() == c.getNumChildren() + 1);
   for (unsigned i=1; i<cond.size(); i++) {
     if( cond[i]!=c[i-1] ) {
       if (fm->isStar(cond[i]))
@@ -1203,7 +1204,7 @@ void FullModelChecker::mkCondDefaultVec( FirstOrderModelFmc * fm, Node f, std::v
   cond.push_back(d_quant_cond[f]);
   for (unsigned i=0; i<f[0].getNumChildren(); i++) {
     Node ts = fm->getStar(f[0][i].getType());
-    Assert( ts.getType()==f[0][i].getType() );
+    Assert(ts.getType() == f[0][i].getType());
     cond.push_back(ts);
   }
 }
diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index 3ab52a63b..cdaaa239a 100644
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -77,7 +77,7 @@ void ModelEngine::check(Theory::Effort e, QEffort quant_e)
     doCheck = quant_e == QEFFORT_MODEL;
   }
   if( doCheck ){
-    Assert( !d_quantEngine->inConflict() );
+    Assert(!d_quantEngine->inConflict());
     int addedLemmas = 0;
     FirstOrderModel* fm = d_quantEngine->getModel();
 
@@ -240,7 +240,7 @@ int ModelEngine::checkModel(){
     if( d_addedLemmas>0 ){
       break;
     }else{
-      Assert( !d_quantEngine->inConflict() );
+      Assert(!d_quantEngine->inConflict());
     }
   }
 
diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp
index 185a349c0..aa3efca19 100644
--- a/src/theory/quantifiers/fun_def_process.cpp
+++ b/src/theory/quantifiers/fun_def_process.cpp
@@ -36,7 +36,7 @@ void FunDefFmf::simplify( std::vector< Node >& assertions ) {
   for( unsigned i=0; i<assertions.size(); i++ ){
     Node n = QuantAttributes::getFunDefHead( assertions[i] );
     if( !n.isNull() ){
-      Assert( n.getKind()==APPLY_UF );
+      Assert(n.getKind() == APPLY_UF);
       Node f = n.getOperator();
 
       //check if already defined, if so, throw error
@@ -127,7 +127,7 @@ void FunDefFmf::simplify( std::vector< Node >& assertions ) {
 Node FunDefFmf::simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, Node hd, bool is_fun_def,
                                  std::map< int, std::map< Node, Node > >& visited,
                                  std::map< int, std::map< Node, Node > >& visited_cons ) {
-  Assert( constraints.empty() );
+  Assert(constraints.empty());
   int index = ( is_fun_def ? 1 : 0 ) + 2*( hasPol ? ( pol ? 1 : -1 ) : 0 );
   std::map< Node, Node >::iterator itv = visited[index].find( n );
   if( itv!=visited[index].end() ){
@@ -240,7 +240,7 @@ Node FunDefFmf::simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Nod
         cons = constraints[0];
       }
       visited_cons[index][n] = cons;
-      Assert( constraints.size()==1 && constraints[0]==cons );
+      Assert(constraints.size() == 1 && constraints[0] == cons);
     }
     visited[index][n] = ret;
     return ret;
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index 069d5b888..bd947d70b 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -107,7 +107,7 @@ void InstMatch::setValue( int i, TNode n ) {
 }
 bool InstMatch::set(EqualityQuery* q, int i, TNode n)
 {
-  Assert( i>=0 );
+  Assert(i >= 0);
   if( !d_vals[i].isNull() ){
     if (q->areEqual(d_vals[i], n))
     {
diff --git a/src/theory/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp
index a3c114d90..6566319fa 100644
--- a/src/theory/quantifiers/inst_propagator.cpp
+++ b/src/theory/quantifiers/inst_propagator.cpp
@@ -121,8 +121,8 @@ Node EqualityQueryInstProp::getRepresentativeExp( Node a, std::vector< Node >& e
   if( !ar.isNull() ){
     if( engine_has_a || getEngine()->hasTerm( ar ) ){
       Trace("qip-eq") << "getRepresentativeExp " << a << " returns " << ar << std::endl;
-      Assert( getEngine()->hasTerm( ar ) );
-      Assert( getEngine()->getRepresentative( ar )==ar );
+      Assert(getEngine()->hasTerm(ar));
+      Assert(getEngine()->getRepresentative(ar) == ar);
       return ar;
     }
   }else{
@@ -187,15 +187,15 @@ TNode EqualityQueryInstProp::getCongruentTermExp( Node f, std::vector< TNode >&
 }
 
 Node EqualityQueryInstProp::getUfRepresentative( Node a, std::vector< Node >& exp ) {
-  Assert( exp.empty() );
+  Assert(exp.empty());
   std::map< Node, Node >::iterator it = d_uf.find( a );
   if( it!=d_uf.end() ){
     if( it->second==a ){
-      Assert( d_uf_exp[ a ].empty() );
+      Assert(d_uf_exp[a].empty());
       return it->second;
     }else{
       Node m = getUfRepresentative( it->second, exp );
-      Assert( !m.isNull() );
+      Assert(!m.isNull());
       if( m!=it->second ){
         //update union find
         d_uf[ a ] = m;
@@ -224,7 +224,7 @@ int EqualityQueryInstProp::setEqual( Node& a, Node& b, bool pol, std::vector< No
   std::vector< Node > exp_a;
   Node ar = getUfRepresentative( a, exp_a );
   if( ar.isNull() ){
-    Assert( exp_a.empty() );
+    Assert(exp_a.empty());
     ar = a;
   }
   if( ar==b ){
@@ -241,7 +241,7 @@ int EqualityQueryInstProp::setEqual( Node& a, Node& b, bool pol, std::vector< No
   std::vector< Node > exp_b;
   Node br = getUfRepresentative( b, exp_b );
   if( br.isNull() ){
-    Assert( exp_b.empty() );
+    Assert(exp_b.empty());
     br = b;
     if( !getEngine()->hasTerm( br ) ){
       if( ar!=a || getEngine()->hasTerm( ar ) ){
@@ -278,8 +278,8 @@ int EqualityQueryInstProp::setEqual( Node& a, Node& b, bool pol, std::vector< No
     br = temp_r;
   }
 
-  Assert( !getEngine()->hasTerm( ar ) || getEngine()->hasTerm( br ) );
-  Assert( ar!=br );
+  Assert(!getEngine()->hasTerm(ar) || getEngine()->hasTerm(br));
+  Assert(ar != br);
 
   std::vector< Node > exp_d;
   if( areDisequalExp( ar, br, exp_d ) ){
@@ -294,8 +294,8 @@ int EqualityQueryInstProp::setEqual( Node& a, Node& b, bool pol, std::vector< No
   }else{
     if( pol ){
       //update the union find
-      Assert( d_uf_exp[ar].empty() );
-      Assert( d_uf_exp[br].empty() );
+      Assert(d_uf_exp[ar].empty());
+      Assert(d_uf_exp[br].empty());
 
       //registerUfTerm( ar );
       d_uf[ar] = br;
@@ -326,8 +326,8 @@ int EqualityQueryInstProp::setEqual( Node& a, Node& b, bool pol, std::vector< No
       return status;
     }else{
       Trace("qip-eq") << "EqualityQueryInstProp::setEqual : disequal " << ar << " <> " << br << std::endl;
-      Assert( d_diseq_list[ar].find( br )==d_diseq_list[ar].end() );
-      Assert( d_diseq_list[br].find( ar )==d_diseq_list[br].end() );
+      Assert(d_diseq_list[ar].find(br) == d_diseq_list[ar].end());
+      Assert(d_diseq_list[br].find(ar) == d_diseq_list[br].end());
 
       merge_exp( d_diseq_list[ar][br], reason );
       merge_exp( d_diseq_list[br][ar], reason );
@@ -372,7 +372,7 @@ bool EqualityQueryInstProp::isPropagateLiteral( Node n ) {
       Node atom = n.getKind()==NOT ? n[0] : n;
       return !atom[0].getType().isBoolean();
     }else{
-      Assert( ak!=NOT );
+      Assert(ak != NOT);
       return ak!=AND && ak!=OR && ak!=ITE;
     }
   }
@@ -410,7 +410,7 @@ Node EqualityQueryInstProp::evaluateTermExp( Node n, std::vector< Node >& exp, s
     Node ret;
     //check if it should be propagated in this context
     if( hasPol && isPropagateLiteral( n ) ){
-      Assert( n.getType().isBoolean() );
+      Assert(n.getType().isBoolean());
       //must be Boolean
       ret = evaluateTermExp( n, exp, visited, false, pol, watch_list_out, props );
       if( isPropagateLiteral( ret ) ){
@@ -432,7 +432,7 @@ Node EqualityQueryInstProp::evaluateTermExp( Node n, std::vector< Node >& exp, s
           bool childChanged = false;
           int abort_i = -1;
           //get the child entailed polarity
-          Assert( n.getKind()!=IMPLIES );
+          Assert(n.getKind() != IMPLIES);
           bool newHasPol, newPol;
           QuantPhaseReq::getEntailPolarity( n, 0, hasPol, pol, newHasPol, newPol );
           std::vector< Node > watch;
@@ -511,19 +511,19 @@ Node EqualityQueryInstProp::evaluateTermExp( Node n, std::vector< Node >& exp, s
                 Trace("qip-eval") << "arg " << i << " : " << args[i] << std::endl;
                 t_args.push_back( args[i] );
               }
-              Assert( args.size()==n.getNumChildren() );
+              Assert(args.size() == n.getNumChildren());
               //args contains terms known by the equality engine
               TNode nn = getCongruentTerm( f, t_args );
               Trace("qip-eval") << "  got congruent term " << nn << " for " << n << std::endl;
               if( !nn.isNull() ){
                 //successfully constructed representative in EE
-                Assert( exp_n.empty() );
+                Assert(exp_n.empty());
                 ret = getRepresentativeExp( nn, exp_n );
                 Trace("qip-eval") << "return rep, exp size = " << exp_n.size() << std::endl;
                 merge_exp( exp, exp_n );
                 ret_set = true;
-                Assert( !ret.isNull() );
-                Assert( ret!=n );
+                Assert(!ret.isNull());
+                Assert(ret != n);
                 // we have that n == ret, check if the union find should be updated TODO?
               }else{
                 watch.push_back( ret );
@@ -542,7 +542,7 @@ Node EqualityQueryInstProp::evaluateTermExp( Node n, std::vector< Node >& exp, s
                     ret_set = true;
                   }
                 }else{
-                  Assert( args.size()==n.getNumChildren() );
+                  Assert(args.size() == n.getNumChildren());
                 }
                 if( !ret_set ){
                   if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
@@ -576,7 +576,7 @@ Node EqualityQueryInstProp::evaluateTermExp( Node n, std::vector< Node >& exp, s
 void EqualityQueryInstProp::merge_exp( std::vector< Node >& v, std::vector< Node >& v_to_merge, int up_to_size ) {
   //TODO : optimize
   if( v.empty() ){
-    Assert( up_to_size==-1 || up_to_size==(int)v_to_merge.size() );
+    Assert(up_to_size == -1 || up_to_size == (int)v_to_merge.size());
     v.insert( v.end(), v_to_merge.begin(), v_to_merge.end() );
   }else{
     //std::vector< Node >::iterator v_end = v.end();
@@ -595,7 +595,7 @@ void InstPropagator::InstInfo::init( Node q, Node lem, std::vector< Node >& term
   //information about the instance
   d_q = q;
   d_lem = lem;
-  Assert( d_terms.empty() );
+  Assert(d_terms.empty());
   d_terms.insert( d_terms.end(), terms.begin(), terms.end() );
   //the current lemma
   d_curr = body;
@@ -641,7 +641,7 @@ bool InstPropagator::notifyInstantiation(QuantifiersModule::QEffort quant_e,
     unsigned id = allocateInstantiation( q, lem, terms, body );
     //initialize the information
     if( cacheConclusion( id, body ) ){
-      Assert( d_update_list.empty() );
+      Assert(d_update_list.empty());
       d_update_list.push_back( id );
       bool firstTime = true;
       //update infos in the update list until empty
@@ -660,7 +660,7 @@ bool InstPropagator::notifyInstantiation(QuantifiersModule::QEffort quant_e,
     Trace("qip-prop") << "...finished notify instantiation." << std::endl;
     return !d_conflict;
   }else{
-    Assert( false );
+    Assert(false);
     return false;
   }
 }
@@ -676,7 +676,7 @@ void InstPropagator::filterInstantiations() {
                   it->second.d_q, it->second.d_lem, it->second.d_terms))
           {
             Trace("qip-warn") << "WARNING : did not remove instantiation id " << it->first << std::endl;
-            Assert( false );
+            Assert(false);
           }else{
             Trace("qip-prop-debug") << it->first << " ";
           }
@@ -700,8 +700,8 @@ unsigned InstPropagator::allocateInstantiation( Node q, Node lem, std::vector< N
 }
 
 bool InstPropagator::update( unsigned id, InstInfo& ii, bool firstTime ) {
-  Assert( !d_conflict );
-  Assert( ii.d_active );
+  Assert(!d_conflict);
+  Assert(ii.d_active);
   Trace("qip-prop-debug") << "Update info [" << id << "]..." << std::endl;
   //update the evaluation of the current lemma
   std::map< Node, std::vector< Node > > watch_list_out;
@@ -733,14 +733,14 @@ bool InstPropagator::update( unsigned id, InstInfo& ii, bool firstTime ) {
     }
     //determine the status of eval
     if( eval==d_qy.d_false ){
-      Assert( props.empty() );
+      Assert(props.empty());
       //we have inferred a conflict
       conflict( ii.d_curr_exp );
       return false;
     }else{
       for( unsigned i=0; i<props.size(); i++ ){
         Trace("qip-prop-debug2")  << "Process propagation " << props[i] << std::endl;
-        Assert( d_qy.isPropagateLiteral( props[i] ) );
+        Assert(d_qy.isPropagateLiteral(props[i]));
         //if we haven't propagated this literal yet
         if( cacheConclusion( id, props[i], 1 ) ){
           //watch list for propagated literal: may not yet be purely EE representatives
@@ -778,7 +778,7 @@ bool InstPropagator::update( unsigned id, InstInfo& ii, bool firstTime ) {
   }else{
     Trace("qip-prop-debug") << "...did not update." << std::endl;
   }
-  Assert( !d_conflict );
+  Assert(!d_conflict);
   return true;
 }
 
@@ -802,8 +802,8 @@ void InstPropagator::propagate( Node a, Node b, bool pol, std::vector< Node >& e
     if( status==EqualityQueryInstProp::STATUS_MERGED_KNOWN ){
       Trace("qip-rlv-propagate")
           << "Relevant propagation : " << a << " == " << b << std::endl;
-      Assert( d_qy.getEngine()->hasTerm( a ) );
-      Assert( d_qy.getEngine()->hasTerm( b ) );
+      Assert(d_qy.getEngine()->hasTerm(a));
+      Assert(d_qy.getEngine()->hasTerm(b));
       Trace("qip-prop-debug") << "...equality between known terms." << std::endl;
       addRelevantInstances( exp, "qip-propagate" );
       //d_has_relevant_inst = true;
@@ -837,7 +837,7 @@ void InstPropagator::conflict( std::vector< Node >& exp ) {
 }
 
 bool InstPropagator::cacheConclusion( unsigned id, Node body, int prop_index ) {
-  Assert( prop_index==0 || prop_index==1 );
+  Assert(prop_index == 0 || prop_index == 1);
   //check if the conclusion is non-redundant
   if( d_conc_to_id[prop_index].find( body )==d_conc_to_id[prop_index].end() ){
     d_conc_to_id[prop_index][body] = id;
@@ -849,7 +849,7 @@ bool InstPropagator::cacheConclusion( unsigned id, Node body, int prop_index ) {
 
 void InstPropagator::addRelevantInstances( std::vector< Node >& exp, const char * c ) {
   for( unsigned i=0; i<exp.size(); i++ ){
-    Assert( d_conc_to_id[0].find( exp[i] )!=d_conc_to_id[0].end() );
+    Assert(d_conc_to_id[0].find(exp[i]) != d_conc_to_id[0].end());
     Trace(c) << "  relevant instance id : " << d_conc_to_id[0][ exp[i] ] << std::endl;
     d_relevant_inst[ d_conc_to_id[0][ exp[i] ] ] = true;
   }
@@ -857,7 +857,7 @@ void InstPropagator::addRelevantInstances( std::vector< Node >& exp, const char
 
 void InstPropagator::debugPrintExplanation( std::vector< Node >& exp, const char * c ) {
   for( unsigned i=0; i<exp.size(); i++ ){
-    Assert( d_conc_to_id[0].find( exp[i] )!=d_conc_to_id[0].end() );
+    Assert(d_conc_to_id[0].find(exp[i]) != d_conc_to_id[0].end());
     Trace(c) << d_conc_to_id[0][ exp[i] ] << " ";
   }
 }
diff --git a/src/theory/quantifiers/local_theory_ext.cpp b/src/theory/quantifiers/local_theory_ext.cpp
index 520088328..a3de5ced9 100644
--- a/src/theory/quantifiers/local_theory_ext.cpp
+++ b/src/theory/quantifiers/local_theory_ext.cpp
@@ -164,11 +164,11 @@ void LtePartialInst::getInstantiations( std::vector< Node >& lemmas ) {
   reset();
   for( unsigned i=0; i<d_lte_asserts.size(); i++ ){
     Node q = d_lte_asserts[i];
-    Assert( d_do_inst.find( q )!=d_do_inst.end() && d_do_inst[q] );
+    Assert(d_do_inst.find(q) != d_do_inst.end() && d_do_inst[q]);
     if( d_inst.find( q )==d_inst.end() ){
       Trace("lte-partial-inst") << "LTE : Get partial instantiations for " << q << "..." << std::endl;
       d_inst[q] = true;
-      Assert( !d_vars[q].empty() );
+      Assert(!d_vars[q].empty());
       //make bound list
       Node bvl;
       std::vector< Node > bvs;
@@ -189,7 +189,7 @@ void LtePartialInst::getInstantiations( std::vector< Node >& lemmas ) {
       }
 
       getPartialInstantiations( conj, q, bvl, d_vars[q], terms, types, NULL, 0, 0, 0 );
-      Assert( !conj.empty() );
+      Assert(!conj.empty());
       lemmas.push_back( NodeManager::currentNM()->mkNode( OR, q.negate(), conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj ) ) );
       d_wasInvoked = true;
     }
@@ -226,16 +226,16 @@ void LtePartialInst::getPartialInstantiations(std::vector<Node>& conj,
       conj.push_back( nq );
     }
   }else{
-    Assert( pindex<q[2][0].getNumChildren() );
+    Assert(pindex < q[2][0].getNumChildren());
     Node pat = q[2][0][pindex];
-    Assert( pat.getNumChildren()==0 || paindex<=pat.getNumChildren() );
+    Assert(pat.getNumChildren() == 0 || paindex <= pat.getNumChildren());
     if( pat.getKind()==APPLY_UF ){
-      Assert( paindex<=pat.getNumChildren() );
+      Assert(paindex <= pat.getNumChildren());
       if( paindex==pat.getNumChildren() ){
         getPartialInstantiations( conj, q, bvl, vars, terms, types, NULL, pindex+1, 0, iindex );
       }else{
         if( !curr ){
-          Assert( paindex==0 );
+          Assert(paindex == 0);
           //start traversing term index for the operator
           curr = d_quantEngine->getTermDatabase()->getTermArgTrie( pat.getOperator() );
         }
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 4b055f71c..de46eee74 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -148,7 +148,7 @@ void QuantInfo::getPropagateVars( QuantConflictFind * p, std::vector< TNode >& v
     bool rec = true;
     bool newPol = pol;
     if( d_var_num.find( n )!=d_var_num.end() ){
-      Assert( std::find( vars.begin(), vars.end(), n )==vars.end() );
+      Assert(std::find(vars.begin(), vars.end(), n) == vars.end());
       vars.push_back( n );
       TNode f = p->getTermDatabase()->getMatchOperator( n );
       if( !f.isNull() ){
@@ -157,7 +157,7 @@ void QuantInfo::getPropagateVars( QuantConflictFind * p, std::vector< TNode >& v
         }
       } 
     }else if( MatchGen::isHandledBoolConnective( n ) ){
-      Assert( n.getKind()!=IMPLIES );
+      Assert(n.getKind() != IMPLIES);
       QuantPhaseReq::getEntailPolarity( n, 0, true, pol, rec, newPol );
     }
     Trace("qcf-opt-debug") << "getPropagateVars " << n << ", pol = " << pol << ", rec = " << rec << std::endl;
@@ -298,7 +298,7 @@ TNode QuantInfo::getCurrentValue( TNode n ) {
     if( d_match[v].isNull() ){
       return n;
     }else{
-      Assert( getVarNum( d_match[v] )!=v );
+      Assert(getVarNum(d_match[v]) != v);
       return getCurrentValue( d_match[v] );
     }
   }
@@ -312,7 +312,7 @@ TNode QuantInfo::getCurrentExpValue( TNode n ) {
     if( d_match[v].isNull() ){
       return n;
     }else{
-      Assert( getVarNum( d_match[v] )!=v );
+      Assert(getVarNum(d_match[v]) != v);
       if( d_match_term[v].isNull() ){
         return getCurrentValue( d_match[v] );
       }else{
@@ -356,9 +356,9 @@ int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, int vn, boo
   //for handling equalities between variables, and disequalities involving variables
   Debug("qcf-match-debug") << "- " << (doRemove ? "un" : "" ) << "constrain : " << v << " -> " << n << " (cv=" << getCurrentValue( n ) << ")";
   Debug("qcf-match-debug") << ", (vn=" << vn << "), polarity = " << polarity << std::endl;
-  Assert( doRemove || n==getCurrentValue( n ) );
-  Assert( doRemove || v==getCurrentRepVar( v ) );
-  Assert( doRemove || vn==getCurrentRepVar( getVarNum( n ) ) );
+  Assert(doRemove || n == getCurrentValue(n));
+  Assert(doRemove || v == getCurrentRepVar(v));
+  Assert(doRemove || vn == getCurrentRepVar(getVarNum(n)));
   if( polarity ){
     if( vn!=v ){
       if( doRemove ){
@@ -398,7 +398,7 @@ int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, int vn, boo
             bool alreadySet = false;
             if( !d_match[vn].isNull() ){
               alreadySet = true;
-              Assert( !isVar( d_match[vn] ) );
+              Assert(!isVar(d_match[vn]));
             }
 
             //copy or check disequalities
@@ -461,7 +461,7 @@ int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, int vn, boo
       return -1;
     }else{
       if( doRemove ){
-        Assert( d_curr_var_deq[v].find( n )!=d_curr_var_deq[v].end() );
+        Assert(d_curr_var_deq[v].find(n) != d_curr_var_deq[v].end());
         d_curr_var_deq[v].erase( n );
         return 1;
       }else{
@@ -831,7 +831,7 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign
                 Trace("qcf-check-unassign") << "Failed match with mg at " << d_una_index << std::endl;
               }
             }else{
-              Assert( doFail || d_una_index==(int)d_una_eqc_count.size()-1 );
+              Assert(doFail || d_una_index == (int)d_una_eqc_count.size() - 1);
               if( d_una_eqc_count[d_una_index]<(int)p->d_eqcs[d_unassigned_tn[d_una_index]].size() ){
                 int currIndex = d_una_eqc_count[d_una_index];
                 d_una_eqc_count[d_una_index]++;
@@ -975,7 +975,7 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar )
   std::vector< Node > qni_apps;
   d_qni_size = 0;
   if( isVar ){
-    Assert( qi->d_var_num.find( n )!=qi->d_var_num.end() );
+    Assert(qi->d_var_num.find(n) != qi->d_var_num.end());
     if( n.getKind()==ITE ){
       d_type = typ_invalid;
     }else{
@@ -1026,10 +1026,10 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar )
         d_type = typ_invalid;
         //literals
         if( isHandledUfTerm( d_n ) ){
-          Assert( qi->isVar( d_n ) );
+          Assert(qi->isVar(d_n));
           d_type = typ_pred;
         }else if( d_n.getKind()==BOUND_VARIABLE ){
-          Assert( d_n.getType().isBoolean() );
+          Assert(d_n.getType().isBoolean());
           d_type = typ_bool_var;
         }else if( d_n.getKind()==EQUAL || options::qcfTConstraint() ){
           for (unsigned i = 0; i < d_n.getNumChildren(); i++)
@@ -1140,7 +1140,7 @@ void MatchGen::determineVariableOrder( QuantInfo * qi, std::vector< int >& bvars
       Trace("qcf-qregister-vo") << vu_count[min_score_index] << " " << vb_count[min_score_index] << " " << has_nested[min_score_index] << std::endl;
       Trace("qcf-qregister-debug") << "...assign child " << min_score_index << std::endl;
       Trace("qcf-qregister-debug") << "...score : " << min_score << std::endl;
-      Assert( min_score_index!=-1 );
+      Assert(min_score_index != -1);
       //add to children order
       d_children_order.push_back( min_score_index );
       assigned[min_score_index] = true;
@@ -1291,7 +1291,7 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
       d_qn.push_back( NULL );
     }
   }else if( d_type==typ_var ){
-    Assert( isHandledUfTerm( d_n ) );
+    Assert(isHandledUfTerm(d_n));
     TNode f = getMatchOperator( p, d_n );
     Debug("qcf-match-debug") << "       reset: Var will match operators of " << f << std::endl;
     TNodeTrie* qni = p->getTermDatabase()->getTermArgTrie(Node::null(), f);
@@ -1520,7 +1520,7 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
         //clean up the matches you set
         for( std::map< int, int >::iterator it = d_qni_bound.begin(); it != d_qni_bound.end(); ++it ){
           Debug("qcf-match") << "       Clean up bound var " << it->second << std::endl;
-          Assert( it->second<qi->getNumVars() );
+          Assert(it->second < qi->getNumVars());
           qi->unsetMatch( p, it->second );
           qi->d_match_term[ it->second ] = TNode::null();
         }
@@ -1650,8 +1650,8 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) {
       d_qn.clear();
       return true;
     }else{
-      Assert( d_type==typ_var );
-      Assert( d_qni_size>0 );
+      Assert(d_type == typ_var);
+      Assert(d_qni_size > 0);
       bool invalidMatch;
       do {
         invalidMatch = false;
@@ -1694,10 +1694,10 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) {
             }
           }else{
             Debug("qcf-match-debug") << "       Match " << index << " is ground term" << std::endl;
-            Assert( d_qni_gterm.find( index )!=d_qni_gterm.end() );
-            Assert( d_qni_gterm_rep.find( index )!=d_qni_gterm_rep.end() );
+            Assert(d_qni_gterm.find(index) != d_qni_gterm.end());
+            Assert(d_qni_gterm_rep.find(index) != d_qni_gterm_rep.end());
             val = d_qni_gterm_rep[index];
-            Assert( !val.isNull() );
+            Assert(!val.isNull());
           }
           if( !val.isNull() ){
             //constrained by val
@@ -1715,7 +1715,7 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) {
             }
           }
         }else{
-          Assert( d_qn.size()==d_qni.size() );
+          Assert(d_qn.size() == d_qni.size());
           int index = d_qni.size()-1;
           //increment if binding this variable
           bool success = false;
@@ -1751,7 +1751,7 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) {
       if( d_qni.size()==d_qni_size ){
         //Assert( !d_qni[d_qni.size()-1]->second.d_data.empty() );
         //Debug("qcf-match-debug") << "       We matched " << d_qni[d_qni.size()-1]->second.d_children.begin()->first << std::endl;
-        Assert( !d_qni[d_qni.size()-1]->second.d_data.empty() );
+        Assert(!d_qni[d_qni.size() - 1]->second.d_data.empty());
         TNode t = d_qni[d_qni.size()-1]->second.d_data.begin()->first;
         Debug("qcf-match-debug") << "       " << d_n << " matched " << t << std::endl;
         qi->d_match_term[d_qni_var_num[0]] = t;
@@ -1760,8 +1760,8 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) {
           Debug("qcf-match-debug") << "       position " << it->first << " bounded " << it->second << " / " << qi->d_q[0].getNumChildren() << std::endl;
           //if( it->second<(int)qi->d_q[0].getNumChildren() ){   //if it is an actual variable, we are interested in knowing the actual term
           if( it->first>0 ){
-            Assert( !qi->d_match[ it->second ].isNull() );
-            Assert( p->areEqual( t[it->first-1], qi->d_match[ it->second ] ) );
+            Assert(!qi->d_match[it->second].isNull());
+            Assert(p->areEqual(t[it->first - 1], qi->d_match[it->second]));
             qi->d_match_term[it->second] = t[it->first-1];
           }
           //}
diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index f5ebb33b1..0e6eb1581 100644
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -64,24 +64,24 @@ void QuantAttributes::setUserAttribute( const std::string& attr, Node n, std::ve
     QuantNameAttribute qna;
     n.setAttribute(qna, true);
   } else if (attr == "sygus-synth-grammar") {
-    Assert( node_values.size()==1 );
+    Assert(node_values.size() == 1);
     Trace("quant-attr-debug") << "Set sygus synth grammar " << n << " to "
                               << node_values[0] << std::endl;
     SygusSynthGrammarAttribute ssg;
     n.setAttribute(ssg, node_values[0]);
   }else if( attr=="sygus-synth-fun-var-list" ){
-    Assert( node_values.size()==1 );
+    Assert(node_values.size() == 1);
     Trace("quant-attr-debug") << "Set sygus synth fun var list to " << n << " to "  << node_values[0] << std::endl;
     SygusSynthFunVarListAttribute ssfvla;
     n.setAttribute( ssfvla, node_values[0] );
   }else if( attr=="quant-inst-max-level" ){
-    Assert( node_values.size()==1 );
+    Assert(node_values.size() == 1);
     uint64_t lvl = node_values[0].getConst<Rational>().getNumerator().getLong();
     Trace("quant-attr-debug") << "Set instantiation level " << n << " to " << lvl << std::endl;
     QuantInstLevelAttribute qila;
     n.setAttribute( qila, lvl );
   }else if( attr=="rr-priority" ){
-    Assert( node_values.size()==1 );
+    Assert(node_values.size() == 1);
     uint64_t lvl = node_values[0].getConst<Rational>().getNumerator().getLong();
     Trace("quant-attr-debug") << "Set rewrite rule priority " << n << " to " << lvl << std::endl;
     RrPriorityAttribute rrpa;
@@ -296,7 +296,7 @@ void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){
         }
         if( avar.getKind()==REWRITE_RULE ){
           Trace("quant-attr") << "Attribute : rewrite rule : " << q << std::endl;
-          Assert( i==0 );
+          Assert(i == 0);
           qa.d_rr = avar;
         }
       }
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 33da46675..0039ec845 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -92,7 +92,7 @@ void QuantifiersRewriter::computeArgVec(const std::vector<Node>& args,
                                         std::vector<Node>& activeArgs,
                                         Node n)
 {
-  Assert( activeArgs.empty() );
+  Assert(activeArgs.empty());
   std::map< Node, bool > activeMap;
   std::map< Node, bool > visited;
   computeArgs( args, activeMap, n, visited );
@@ -110,7 +110,7 @@ void QuantifiersRewriter::computeArgVec2(const std::vector<Node>& args,
                                          Node n,
                                          Node ipl)
 {
-  Assert( activeArgs.empty() );
+  Assert(activeArgs.empty());
   std::map< Node, bool > activeMap;
   std::map< Node, bool > visited;
   computeArgs( args, activeMap, n, visited );
@@ -286,7 +286,7 @@ Node QuantifiersRewriter::computeElimSymbols( Node body ) {
     }
     if( !success ){
       // tautology
-      Assert( k==OR || k==AND );
+      Assert(k == OR || k == AND);
       return NodeManager::currentNM()->mkConst( k==OR );
     }
     childrenChanged = childrenChanged || c!=body[i];
@@ -405,7 +405,7 @@ int getEntailedCond( Node n, std::map< Node, bool >& currCond ){
       }else if( j==start ){
         res1 = res;
       }else{
-        Assert( res!=0 );
+        Assert(res != 0);
         if( n.getKind()==ITE ){
           return res1==res ? res : 0;
         }else if( n.getKind()==EQUAL ){
@@ -456,7 +456,7 @@ void setEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::v
     if( n.getKind()==APPLY_TESTER ){
       const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr());
       unsigned index = Datatype::indexOf(n.getOperator().toExpr());
-      Assert( dt.getNumConstructors()>1 );
+      Assert(dt.getNumConstructors() > 1);
       if( pol ){
         for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
           if( i!=index ){
@@ -491,7 +491,7 @@ Node QuantifiersRewriter::computeProcessTerms( Node body, std::vector< Node >& n
   std::map< Node, Node > icache;
   if( qa.isFunDef() ){
     Node h = QuantAttributes::getFunDefHead( q );
-    Assert( !h.isNull() );
+    Assert(!h.isNull());
     // if it is a function definition, rewrite the body independently
     Node fbody = QuantAttributes::getFunDefBody( q );
     Trace("quantifiers-rewrite-debug") << "Decompose " << h << " / " << fbody << " as function definition for " << q << "." << std::endl;
@@ -572,8 +572,8 @@ Node QuantifiersRewriter::computeProcessTerms2( Node body, bool hasPol, bool pol
               nCurrCond = nCurrCond + 1;
             }
             setEntailedCond( children[0], i==1, currCond, new_cond, conflict );
-            //should not conflict (entailment check failed) 
-            Assert( !conflict );
+            // should not conflict (entailment check failed)
+            Assert(!conflict);
           }
           if( body.getKind()==OR || body.getKind()==AND ){
             bool use_pol = body.getKind()==AND;
@@ -763,7 +763,7 @@ Node QuantifiersRewriter::computeCondSplit(Node body,
     std::map< Node, std::map< int, Node > > ncons;
     std::vector< Node > conj;
     computeDtTesterIteSplit( body, pcons, ncons, conj );
-    Assert( !conj.empty() );
+    Assert(!conj.empty());
     if( conj.size()>1 ){
       Trace("quantifiers-rewrite-ite") << "*** Split ITE (datatype tester) " << body << " into : " << std::endl;
       for( unsigned i=0; i<conj.size(); i++ ){
@@ -1507,7 +1507,7 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, s
               NodeManager::currentNM()->mkNode( kind::OR, body[0], body[1].notNode() ) );
     return computePrenex( nn, args, nargs, pol, prenexAgg );
   }else if( body.getType().isBoolean() ){
-    Assert( body.getKind()!=EXISTS );
+    Assert(body.getKind() != EXISTS);
     bool childrenChanged = false;
     std::vector< Node > newChildren;
     for( unsigned i=0; i<body.getNumChildren(); i++ ){
@@ -1629,8 +1629,8 @@ Node QuantifiersRewriter::computePrenexAgg( Node n, bool topLevel, std::map< uns
         }
         ret = nnn;
       }else{
-        Assert( args.empty() );
-        Assert( nargs.empty() );
+        Assert(args.empty());
+        Assert(nargs.empty());
       }
     }
     visited[tindex][n] = ret;
@@ -1640,7 +1640,7 @@ Node QuantifiersRewriter::computePrenexAgg( Node n, bool topLevel, std::map< uns
 }
 
 Node QuantifiersRewriter::computeSplit( std::vector< Node >& args, Node body, QAttributes& qa ) {
-  Assert( body.getKind()==OR );
+  Assert(body.getKind() == OR);
   size_t var_found_count = 0;
   size_t eqc_count = 0;
   size_t eqc_active = 0;
@@ -1732,7 +1732,7 @@ Node QuantifiersRewriter::computeSplit( std::vector< Node >& args, Node body, QA
       Node fa = NodeManager::currentNM()->mkNode( FORALL, bvl, body );
       lits.push_back(fa);
     }
-    Assert( !lits.empty() );
+    Assert(!lits.empty());
     Node nf = lits.size()==1 ? lits[0] : NodeManager::currentNM()->mkNode(OR,lits);
     Trace("clause-split-debug") << "Made node : " << nf << std::endl;
     return nf;
@@ -1828,7 +1828,7 @@ Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node bo
       }
     }
   }else if( body.getKind()==NOT ){
-    Assert( isLiteral( body[0] ) );
+    Assert(isLiteral(body[0]));
   }
   //remove variables that don't occur
   std::vector< Node > activeArgs;
@@ -1902,8 +1902,8 @@ Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& arg
           qvl2.push_back( args[i] );
         }
       }
-      Assert( !qvl1.empty() );
-      Assert( !qvl2.empty() || !qvsh.empty() );
+      Assert(!qvl1.empty());
+      Assert(!qvl2.empty() || !qvsh.empty());
       //check for literals that only contain shared variables
       std::vector<Node> qlitsh;
       std::vector<Node> qlit2;
@@ -2023,7 +2023,7 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttribut
     }else{
       std::vector< Node > nargs;
       n = computePrenex( n, args, nargs, true, false );
-      Assert( nargs.empty() );
+      Assert(nargs.empty());
     }
   }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
     n = computeVarElimination( n, args, qa );
@@ -2091,9 +2091,7 @@ Node QuantifiersRewriter::rewriteRewriteRule( Node r ) {
       break;
     }
     break;
-  default:
-    Unreachable("RewriteRules can be of only three kinds");
-    break;
+  default: Unreachable() << "RewriteRules can be of only three kinds"; break;
   }
   // Add the other guards
   TNode g = r[1];
diff --git a/src/theory/quantifiers/query_generator.cpp b/src/theory/quantifiers/query_generator.cpp
index 742b3000b..99e7b5a8c 100644
--- a/src/theory/quantifiers/query_generator.cpp
+++ b/src/theory/quantifiers/query_generator.cpp
@@ -177,7 +177,7 @@ void QueryGenerator::checkQuery(Node qy, unsigned spIndex)
         ss << "  " << d_vars[i] << " -> " << pt[i] << std::endl;
       }
       ss << "but CVC4 answered unsat!" << std::endl;
-      AlwaysAssert(false, ss.str().c_str());
+      AlwaysAssert(false) << ss.str();
     }
     if (options::sygusQueryGenDumpFiles() == SYGUS_QUERY_DUMP_UNSOLVED)
     {
diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index 071bd7933..fbd1f05a6 100644
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -27,8 +27,8 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 
 void RelevantDomain::RDomain::merge( RDomain * r ) {
-  Assert( !d_parent );
-  Assert( !r->d_parent );
+  Assert(!d_parent);
+  Assert(!r->d_parent);
   d_parent = r;
   for( unsigned i=0; i<d_terms.size(); i++ ){
     r->addTerm( d_terms[i] );
@@ -79,7 +79,7 @@ RelevantDomain::~RelevantDomain() {
   for( std::map< Node, std::map< int, RDomain * > >::iterator itr = d_rel_doms.begin(); itr != d_rel_doms.end(); ++itr ){
     for( std::map< int, RDomain * >::iterator itr2 = itr->second.begin(); itr2 != itr->second.end(); ++itr2 ){
       RDomain * current = (*itr2).second;
-      Assert( current != NULL );
+      Assert(current != NULL);
       delete current;
     }
   }
@@ -183,7 +183,8 @@ void RelevantDomain::computeRelevantDomain( Node q, Node n, bool hasPol, bool po
     //compute the information for what this literal does
     computeRelevantDomainLit( q, hasPol, pol, n );
     if( d_rel_dom_lit[hasPol][pol][n].d_merge ){
-      Assert( d_rel_dom_lit[hasPol][pol][n].d_rd[0]!=NULL && d_rel_dom_lit[hasPol][pol][n].d_rd[1]!=NULL );
+      Assert(d_rel_dom_lit[hasPol][pol][n].d_rd[0] != NULL
+             && d_rel_dom_lit[hasPol][pol][n].d_rd[1] != NULL);
       RDomain * rd1 = d_rel_dom_lit[hasPol][pol][n].d_rd[0]->getParent();
       RDomain * rd2 = d_rel_dom_lit[hasPol][pol][n].d_rd[1]->getParent();
       if( rd1!=rd2 ){
diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp
index 07ff9ee46..9903456c9 100644
--- a/src/theory/quantifiers/rewrite_engine.cpp
+++ b/src/theory/quantifiers/rewrite_engine.cpp
@@ -68,7 +68,7 @@ void RewriteEngine::check(Theory::Effort e, QEffort quant_e)
 {
   if (quant_e == QEFFORT_STANDARD)
   {
-    Assert( !d_quantEngine->inConflict() );
+    Assert(!d_quantEngine->inConflict());
     Trace("rewrite-engine") << "---Rewrite Engine Round, effort = " << e << "---" << std::endl;
     //if( e==Theory::EFFORT_LAST_CALL ){
     //  if( !d_quantEngine->getModel()->isModelSet() ){
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index 47a1f6142..c34b7d4e3 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -53,7 +53,7 @@ CegSingleInv::~CegSingleInv()
 void CegSingleInv::initialize(Node q)
 {
   // can only register one quantified formula with this
-  Assert( d_quant.isNull() );
+  Assert(d_quant.isNull());
   d_quant = q;
   d_simp_quant = q;
   Trace("cegqi-si") << "CegSingleInv::initialize : " << q << std::endl;
@@ -466,7 +466,7 @@ Node CegSingleInv::getSolution(unsigned sol_index,
                                int& reconstructed,
                                bool rconsSygus)
 {
-  Assert( d_sol!=NULL );
+  Assert(d_sol != NULL);
   const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype();
   Node varList = Node::fromExpr( dt.getSygusVarList() );
   Node prog = d_quant[0][sol_index];
@@ -486,7 +486,7 @@ Node CegSingleInv::getSolution(unsigned sol_index,
     Trace("csi-sol") << "Get solution for " << prog << ", with skolems : ";
     sol_index = d_prog_to_sol_index[prog];
     d_sol->d_varList.clear();
-    Assert( d_single_inv_arg_sk.size()==varList.getNumChildren() );
+    Assert(d_single_inv_arg_sk.size() == varList.getNumChildren());
     for( unsigned i=0; i<d_single_inv_arg_sk.size(); i++ ){
       Trace("csi-sol") << d_single_inv_arg_sk[i] << " ";
       vars.push_back( d_single_inv_arg_sk[i] );
@@ -501,7 +501,7 @@ Node CegSingleInv::getSolution(unsigned sol_index,
     {
       indices.push_back(i);
     }
-    Assert( !indices.empty() );
+    Assert(!indices.empty());
     //sort indices based on heuristic : currently, do all constant returns first (leads to simpler conditions)
     // TODO : to minimize solution size, put the largest term last
     sortSiInstanceIndices ssii;
@@ -520,7 +520,7 @@ Node CegSingleInv::getSolution(unsigned sol_index,
       cond = TermUtil::simpleNegate(cond);
       s = nm->mkNode(ITE, cond, d_inst[uindex][sol_index], s);
     }
-    Assert( vars.size()==d_sol->d_varList.size() );
+    Assert(vars.size() == d_sol->d_varList.size());
     s = s.substitute( vars.begin(), vars.end(), d_sol->d_varList.begin(), d_sol->d_varList.end() );
   }
   d_orig_solution = s;
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
index d349e8ad4..811210628 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
@@ -119,7 +119,7 @@ Node CegSingleInvSol::reconstructSolution(Node sol,
   if( status==0 ){
     Node ret = getReconstructedSolution( d_root_id );
     Trace("csi-rcons") << "Sygus solution is : " << ret << std::endl;
-    Assert( !ret.isNull() );
+    Assert(!ret.isNull());
     reconstructed = 1;
     return ret;
   }
@@ -224,11 +224,11 @@ int CegSingleInvSol::collectReconstructNodes(Node t, TypeNode stn, int& status)
     int id = allocate( t, stn );
     d_rcons_to_status[stn][t] = -1;
     TypeNode tn = t.getType();
-    Assert( stn.isDatatype() );
+    Assert(stn.isDatatype());
     const Datatype& dt = stn.getDatatype();
     TermDbSygus* tds = d_qe->getTermDatabaseSygus();
     SygusTypeInfo& sti = tds->getTypeInfo(stn);
-    Assert( dt.isSygus() );
+    Assert(dt.isSygus());
     Trace("csi-rcons-debug") << "Check reconstruct " << t << ", sygus type " << dt.getName() << ", kind " << t.getKind() << ", id : " << id << std::endl;
     int carg = -1;
     int karg = -1;
@@ -291,7 +291,7 @@ int CegSingleInvSol::collectReconstructNodes(Node t, TypeNode stn, int& status)
           //try identity functions
           for (unsigned ii : d_id_funcs[stn])
           {
-            Assert( dt[ii].getNumArgs()==1 );
+            Assert(dt[ii].getNumArgs() == 1);
             //try to directly reconstruct from single argument
             std::vector< Node > tchildren;
             tchildren.push_back( min_t );
@@ -402,7 +402,7 @@ int CegSingleInvSol::collectReconstructNodes(Node t, TypeNode stn, int& status)
                     //if one succeeds
                     if( status==0 ){
                       Node rsol = getReconstructedSolution( equiv_ids[i] );
-                      Assert( !rsol.isNull() );
+                      Assert(!rsol.isNull());
                       //set all members of the equivalence class that this is the reconstructed solution
                       setReconstructed( id, rsol );
                       break;
@@ -433,7 +433,7 @@ bool CegSingleInvSol::collectReconstructNodes(int pid,
                                               std::vector<int>& ids,
                                               int& status)
 {
-  Assert( dtc.getNumArgs()==ts.size() );
+  Assert(dtc.getNumArgs() == ts.size());
   for( unsigned i=0; i<ts.size(); i++ ){
     TypeNode cstn = d_qe->getTermDatabaseSygus()->getArgType( dtc, i );
     int cstatus;
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 0dc49fa96..8f935de27 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -177,7 +177,7 @@ Node CegGrammarConstructor::process(Node q,
       std::map<Node, Node>::const_iterator itta = templates_arg.find(sf);
       Assert(itta != templates_arg.end());
       TNode templ_arg = itta->second;
-      Assert( !templ_arg.isNull() );
+      Assert(!templ_arg.isNull());
       // if there is a template for this argument, make a sygus type on top of it
       if( options::sygusTemplEmbedGrammar() ){
         Trace("cegqi-debug") << "Template for " << sf << " is : " << templ
@@ -737,7 +737,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
       weights[i].push_back(-1);
       // length
       TypeNode intType = nm->integerType();
-      Assert(std::find(types.begin(),types.end(),intType)!=types.end());
+      Assert(std::find(types.begin(), types.end(), intType) != types.end());
       unsigned i_intType = std::distance(
           types.begin(),
           std::find(types.begin(),
@@ -1086,12 +1086,12 @@ TypeNode CegGrammarConstructor::mkSygusDefaultType(
                         datatypes,
                         unres);
   Trace("sygus-grammar-def")  << "...made " << datatypes.size() << " datatypes, now make mutual datatype types..." << std::endl;
-  Assert( !datatypes.empty() );
+  Assert(!datatypes.empty());
   std::vector<DatatypeType> types =
       NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(
           datatypes, unres, ExprManager::DATATYPE_FLAG_PLACEHOLDER);
   Trace("sygus-grammar-def") << "...finished" << std::endl;
-  Assert( types.size()==datatypes.size() );
+  Assert(types.size() == datatypes.size());
   return TypeNode::fromType( types[0] );
 }
 
@@ -1114,7 +1114,7 @@ TypeNode CegGrammarConstructor::mkSygusTemplateTypeRec( Node templ, Node templ_a
       // TODO : can short circuit to this case when !TermUtil::containsTerm( templ, templ_arg )
       op = templ;
     }else{
-      Assert( templ.hasOperator() );
+      Assert(templ.hasOperator());
       op = templ.getOperator();
       // make constructor taking arguments types from children
       for( unsigned i=0; i<templ.getNumChildren(); i++ ){
@@ -1132,7 +1132,7 @@ TypeNode CegGrammarConstructor::mkSygusTemplateTypeRec( Node templ, Node templ_a
     std::vector<DatatypeType> types =
         NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(
             datatypes, unres, ExprManager::DATATYPE_FLAG_PLACEHOLDER);
-    Assert( types.size()==1 );
+    Assert(types.size() == 1);
     return TypeNode::fromType( types[0] );
   }
 }
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index 64bf0972c..474fdb5d8 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -440,7 +440,7 @@ bool SygusPbe::constructCandidates(const std::vector<Node>& enums,
                                    std::vector<Node>& candidate_values,
                                    std::vector<Node>& lems)
 {
-  Assert( enums.size()==enum_values.size() );
+  Assert(enums.size() == enum_values.size());
   if( !enums.empty() ){
     unsigned min_term_size = 0;
     Trace("sygus-pbe-enum") << "Register new enumerated values : " << std::endl;
diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
index ff58dbe38..72091c0cf 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
@@ -1453,12 +1453,11 @@ Node SygusUnifIo::constructSol(
           if (!rec_c.isNull())
           {
             Assert(ecache_child.d_enum_val_to_index.find(rec_c)
-                    != ecache_child.d_enum_val_to_index.end());
+                   != ecache_child.d_enum_val_to_index.end());
             split_cond_res_index = ecache_child.d_enum_val_to_index[rec_c];
             set_split_cond_res_index = true;
             split_cond_enum = ce;
-            Assert(split_cond_res_index
-                    < ecache_child.d_enum_vals_res.size());
+            Assert(split_cond_res_index < ecache_child.d_enum_vals_res.size());
           }
         }
         else
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index ff9fede0b..7fb54f14e 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -14,7 +14,7 @@
 
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 
-#include "base/cvc4_check.h"
+#include "base/check.h"
 #include "options/base_options.h"
 #include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"
@@ -80,7 +80,7 @@ TNode TermDbSygus::getFreeVar( TypeNode tn, int i, bool useSygusType ) {
     }else{
       ss << "fv_" << tn << "_" << i;
     }
-    Assert( !vtn.isNull() );
+    Assert(!vtn.isNull());
     Node v = NodeManager::currentNM()->mkSkolem( ss.str(), vtn, "for sygus normal form testing" );
     d_fv_stype[v] = tn;
     d_fv_num[v] = i;
@@ -155,7 +155,7 @@ Node TermDbSygus::getProxyVariable(TypeNode tn, Node c)
 }
 
 TypeNode TermDbSygus::getSygusTypeForVar( Node v ) {
-  Assert( d_fv_stype.find( v )!=d_fv_stype.end() );
+  Assert(d_fv_stype.find(v) != d_fv_stype.end());
   return d_fv_stype[v];
 }
 
@@ -165,8 +165,8 @@ Node TermDbSygus::mkGeneric(const Datatype& dt,
                             std::map<int, Node>& pre)
 {
   Assert(c < dt.getNumConstructors());
-  Assert( dt.isSygus() );
-  Assert( !dt[c].getSygusOp().isNull() );
+  Assert(dt.isSygus());
+  Assert(!dt[c].getSygusOp().isNull());
   std::vector< Node > children;
   Trace("sygus-db-debug") << "mkGeneric " << dt.getName() << " " << c << "..."
                           << std::endl;
@@ -182,7 +182,7 @@ Node TermDbSygus::mkGeneric(const Datatype& dt,
     }
     Trace("sygus-db-debug")
         << "  child " << i << " : " << a << " : " << a.getType() << std::endl;
-    Assert( !a.isNull() );
+    Assert(!a.isNull());
     children.push_back( a );
   }
   return datatypes::utils::mkSygusTerm(dt, c, children);
@@ -495,7 +495,7 @@ void TermDbSygus::registerEnumerator(Node e,
     }
     else
     {
-      Unreachable("Unknown enumerator mode in registerEnumerator");
+      Unreachable() << "Unknown enumerator mode in registerEnumerator";
     }
   }
   Trace("sygus-db") << "isActiveGen for " << e << ", role = " << erole
@@ -1039,7 +1039,7 @@ Node TermDbSygus::getEagerUnfold( Node n, std::map< Node, Node >& visited ) {
           std::vector< Node > vars;
           std::vector< Node > subs;
           Node var_list = Node::fromExpr( dt.getSygusVarList() );
-          Assert( var_list.getNumChildren()+1==n.getNumChildren() );
+          Assert(var_list.getNumChildren() + 1 == n.getNumChildren());
           for( unsigned j=0; j<var_list.getNumChildren(); j++ ){
             vars.push_back( var_list[j] );
           }
@@ -1049,7 +1049,7 @@ Node TermDbSygus::getEagerUnfold( Node n, std::map< Node, Node >& visited ) {
             Assert(subs[j - 1].getType().isComparableTo(
                 var_list[j - 1].getType()));
           }
-          Assert( vars.size()==subs.size() );
+          Assert(vars.size() == subs.size());
           bTerm = bTerm.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
           Trace("cegqi-eager") << "Built-in term after subs : " << bTerm << std::endl;
           Trace("cegqi-eager-debug") << "Types : " << bTerm.getType() << " " << n.getType() << std::endl;
diff --git a/src/theory/quantifiers/sygus/type_info.cpp b/src/theory/quantifiers/sygus/type_info.cpp
index 818a53711..8f280c587 100644
--- a/src/theory/quantifiers/sygus/type_info.cpp
+++ b/src/theory/quantifiers/sygus/type_info.cpp
@@ -14,7 +14,7 @@
 
 #include "theory/quantifiers/sygus/type_info.h"
 
-#include "base/cvc4_check.h"
+#include "base/check.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 
@@ -123,7 +123,7 @@ void SygusTypeInfo::initialize(TermDbSygus* tds, TypeNode tn)
         TypeNode ct = TypeNode::fromType(dt[i].getArgType(j));
         TypeNode cbt = tds->sygusToBuiltinType(ct);
         TypeNode lat = TypeNode::fromType(sop[0][j].getType());
-        CVC4_CHECK(cbt.isSubtypeOf(lat))
+        AlwaysAssert(cbt.isSubtypeOf(lat))
             << "In sygus datatype " << dt.getName()
             << ", argument to a lambda constructor is not " << lat << std::endl;
       }
@@ -152,7 +152,7 @@ void SygusTypeInfo::initialize(TermDbSygus* tds, TypeNode tn)
     // e.g. bitvector-and is a constructor of an integer grammar.
     Node g = tds->mkGeneric(dt, i);
     TypeNode gtn = g.getType();
-    CVC4_CHECK(gtn.isSubtypeOf(btn))
+    AlwaysAssert(gtn.isSubtypeOf(btn))
         << "Sygus datatype " << dt.getName()
         << " encodes terms that are not of type " << btn << std::endl;
     Trace("sygus-db") << "...done register Operator #" << i << std::endl;
diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index 10d7ef6ab..834ca1975 100644
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -813,8 +813,8 @@ void SygusSampler::checkEquivalent(Node bv, Node bvr)
 
     if (options::sygusRewVerifyAbort())
     {
-      AlwaysAssert(false,
-                   "--sygus-rr-verify detected unsoundness in the rewriter!");
+      AlwaysAssert(false)
+          << "--sygus-rr-verify detected unsoundness in the rewriter!";
     }
   }
 }
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 9da9c95b6..79279eb41 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -46,7 +46,8 @@ TermDb::~TermDb(){
 }
 
 void TermDb::registerQuantifier( Node q ) {
-  Assert( q[0].getNumChildren()==d_quantEngine->getTermUtil()->getNumInstantiationConstants( q ) );
+  Assert(q[0].getNumChildren()
+         == d_quantEngine->getTermUtil()->getNumInstantiationConstants(q));
   for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
     Node ic = d_quantEngine->getTermUtil()->getInstantiationConstant( q, i );
     setTermInactive( ic );
@@ -257,7 +258,7 @@ void TermDb::computeArgReps( TNode n ) {
 }
 
 void TermDb::computeUfEqcTerms( TNode f ) {
-  Assert( f==getOperatorRepresentative( f ) );
+  Assert(f == getOperatorRepresentative(f));
   if (d_func_map_eqc_trie.find(f) != d_func_map_eqc_trie.end())
   {
     return;
@@ -291,7 +292,7 @@ void TermDb::computeUfTerms( TNode f ) {
     // already computed
     return;
   }
-  Assert( f==getOperatorRepresentative( f ) );
+  Assert(f == getOperatorRepresentative(f));
   d_op_nonred_count[f] = 0;
   // get the matchable operators in the equivalence class of f
   std::vector<TNode> ops;
@@ -501,8 +502,9 @@ bool TermDb::inRelevantDomain( TNode f, unsigned i, TNode r ) {
     f = getOperatorRepresentative( f );
   }
   computeUfTerms( f );
-  Assert( !d_quantEngine->getActiveEqualityEngine()->hasTerm( r ) || 
-          d_quantEngine->getActiveEqualityEngine()->getRepresentative( r )==r );
+  Assert(!d_quantEngine->getActiveEqualityEngine()->hasTerm(r)
+         || d_quantEngine->getActiveEqualityEngine()->getRepresentative(r)
+                == r);
   std::map< Node, std::map< unsigned, std::vector< Node > > >::iterator it = d_func_map_rel_dom.find( f );
   if( it != d_func_map_rel_dom.end() ){
     std::map< unsigned, std::vector< Node > >::iterator it2 = it->second.find( i );
@@ -712,7 +714,7 @@ Node TermDb::evaluateTerm2(TNode n,
 
 
 TNode TermDb::getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy ) {
-  Assert( !qy->extendsEngine() );
+  Assert(!qy->extendsEngine());
   Trace("term-db-entail") << "get entailed term : " << n << std::endl;
   if( qy->getEngine()->hasTerm( n ) ){
     Trace("term-db-entail") << "...exists in ee, return rep " << std::endl;
@@ -723,8 +725,8 @@ TNode TermDb::getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool su
       if( it!=subs.end() ){
         Trace("term-db-entail") << "...substitution is : " << it->second << std::endl;
         if( subsRep ){
-          Assert( qy->getEngine()->hasTerm( it->second ) );
-          Assert( qy->getEngine()->getRepresentative( it->second )==it->second );
+          Assert(qy->getEngine()->hasTerm(it->second));
+          Assert(qy->getEngine()->getRepresentative(it->second) == it->second);
           return it->second;
         }else{
           return getEntailedTerm2( it->second, subs, subsRep, hasSubs, qy );
@@ -805,9 +807,9 @@ TNode TermDb::getEntailedTerm( TNode n, EqualityQuery * qy ) {
 }
 
 bool TermDb::isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy ) {
-  Assert( !qy->extendsEngine() );
+  Assert(!qy->extendsEngine());
   Trace("term-db-entail") << "Check entailed : " << n << ", pol = " << pol << std::endl;
-  Assert( n.getType().isBoolean() );
+  Assert(n.getType().isBoolean());
   if( n.getKind()==EQUAL && !n[0].getType().isBoolean() ){
     TNode n1 = getEntailedTerm2( n[0], subs, subsRep, hasSubs, qy );
     if( !n1.isNull() ){
@@ -816,8 +818,8 @@ bool TermDb::isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep,
         if( n1==n2 ){
           return pol;
         }else{
-          Assert( qy->getEngine()->hasTerm( n1 ) );
-          Assert( qy->getEngine()->hasTerm( n2 ) );
+          Assert(qy->getEngine()->hasTerm(n1));
+          Assert(qy->getEngine()->hasTerm(n2));
           if( pol ){
             return qy->getEngine()->areEqual( n1, n2 );
           }else{
@@ -854,7 +856,7 @@ bool TermDb::isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep,
   }else if( n.getKind()==APPLY_UF ){
     TNode n1 = getEntailedTerm2( n, subs, subsRep, hasSubs, qy );
     if( !n1.isNull() ){
-      Assert( qy->hasTerm( n1 ) );
+      Assert(qy->hasTerm(n1));
       if( n1==d_true ){
         return pol;
       }else if( n1==d_false ){
@@ -871,7 +873,7 @@ bool TermDb::isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep,
 
 bool TermDb::isEntailed( TNode n, bool pol, EqualityQuery * qy ) {
   if( qy==NULL ){
-    Assert( d_consistent_ee );
+    Assert(d_consistent_ee);
     qy = d_quantEngine->getEqualityQuery();
   }
   std::map< TNode, TNode > subs;
@@ -880,7 +882,7 @@ bool TermDb::isEntailed( TNode n, bool pol, EqualityQuery * qy ) {
 
 bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol, EqualityQuery * qy ) {
   if( qy==NULL ){
-    Assert( d_consistent_ee );
+    Assert(d_consistent_ee);
     qy = d_quantEngine->getEqualityQuery();
   }
   return isEntailed2( n, subs, subsRep, true, pol, qy );
@@ -908,7 +910,7 @@ bool TermDb::hasTermCurrent( Node n, bool useMode ) {
     }else if( options::termDbMode()==TERM_DB_RELEVANT ){
       return d_has_map.find( n )!=d_has_map.end();
     }else{
-      Assert( false );
+      Assert(false);
       return false;
     }
   }
diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index c9c738eb3..7f94130f3 100644
--- a/src/theory/quantifiers/term_util.cpp
+++ b/src/theory/quantifiers/term_util.cpp
@@ -217,7 +217,7 @@ Node TermUtil::substituteBoundVariables(Node n,
                                         std::vector<Node>& terms)
 {
   registerQuantifier(q);
-  Assert( d_vars[q].size()==terms.size() );
+  Assert(d_vars[q].size() == terms.size());
   return n.substitute( d_vars[q].begin(), d_vars[q].end(), terms.begin(), terms.end() );
 }
 
@@ -306,7 +306,7 @@ void TermUtil::computeInstConstContainsForQuant(Node q,
 
 Node TermUtil::ensureType( Node n, TypeNode tn ) {
   TypeNode ntn = n.getType();
-  Assert( ntn.isComparableTo( tn ) );
+  Assert(ntn.isComparableTo(tn));
   if( ntn.isSubtypeOf( tn ) ){
     return n;
   }else{
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index f24a4bb2b..1682b4d0c 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -16,8 +16,7 @@
 
 #include "theory/quantifiers/theory_quantifiers.h"
 
-
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "expr/kind.h"
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/ematching/instantiation_engine.h"
@@ -147,15 +146,11 @@ void TheoryQuantifiers::check(Effort e) {
           //do nothing
           break;
         case kind::INST_CLOSURE:
-        default:
-          Unhandled(assertion[0].getKind());
-          break;
+        default: Unhandled() << assertion[0].getKind(); break;
         }
       }
       break;
-    default:
-      Unhandled(assertion.getKind());
-      break;
+      default: Unhandled() << assertion.getKind(); break;
     }
   }
   // call the quantifiers engine to check
diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h
index ad1c4c69b..62d75cf18 100644
--- a/src/theory/quantifiers/theory_quantifiers_type_rules.h
+++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h
@@ -29,7 +29,7 @@ struct QuantifierForallTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
   {
     Debug("typecheck-q") << "type check for fa " << n << std::endl;
-    Assert(n.getKind() == kind::FORALL && n.getNumChildren()>0 );
+    Assert(n.getKind() == kind::FORALL && n.getNumChildren() > 0);
     if( check ){
       if( n[ 0 ].getType(check)!=nodeManager->boundVarListType() ){
         throw TypeCheckingExceptionPrivate(n, "first argument of universal quantifier is not bound var list");
@@ -49,7 +49,7 @@ struct QuantifierExistsTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
   {
     Debug("typecheck-q") << "type check for ex " << n << std::endl;
-    Assert(n.getKind() == kind::EXISTS && n.getNumChildren()>0 );
+    Assert(n.getKind() == kind::EXISTS && n.getNumChildren() > 0);
     if( check ){
       if( n[ 0 ].getType(check)!=nodeManager->boundVarListType() ){
         throw TypeCheckingExceptionPrivate(n, "first argument of existential quantifier is not bound var list");
@@ -68,7 +68,7 @@ struct QuantifierExistsTypeRule {
 struct QuantifierBoundVarListTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
   {
-    Assert(n.getKind() == kind::BOUND_VAR_LIST );
+    Assert(n.getKind() == kind::BOUND_VAR_LIST);
     if( check ){
       for( int i=0; i<(int)n.getNumChildren(); i++ ){
         if( n[i].getKind()!=kind::BOUND_VARIABLE ){
@@ -83,7 +83,7 @@ struct QuantifierBoundVarListTypeRule {
 struct QuantifierInstPatternTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
   {
-    Assert(n.getKind() == kind::INST_PATTERN );
+    Assert(n.getKind() == kind::INST_PATTERN);
     if( check ){
       TypeNode tn = n[0].getType(check);
       // this check catches the common mistake writing :pattern (f x) instead of :pattern ((f x))
@@ -98,7 +98,7 @@ struct QuantifierInstPatternTypeRule {
 struct QuantifierInstNoPatternTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
   {
-    Assert(n.getKind() == kind::INST_NO_PATTERN );
+    Assert(n.getKind() == kind::INST_NO_PATTERN);
     return nodeManager->instPatternType();
   }
 };/* struct QuantifierInstNoPatternTypeRule */
@@ -106,7 +106,7 @@ struct QuantifierInstNoPatternTypeRule {
 struct QuantifierInstAttributeTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
   {
-    Assert(n.getKind() == kind::INST_ATTRIBUTE );
+    Assert(n.getKind() == kind::INST_ATTRIBUTE);
     return nodeManager->instPatternType();
   }
 };/* struct QuantifierInstAttributeTypeRule */
@@ -114,7 +114,7 @@ struct QuantifierInstAttributeTypeRule {
 struct QuantifierInstPatternListTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
   {
-    Assert(n.getKind() == kind::INST_PATTERN_LIST );
+    Assert(n.getKind() == kind::INST_PATTERN_LIST);
     if( check ){
       for( int i=0; i<(int)n.getNumChildren(); i++ ){
         if( n[i].getKind()!=kind::INST_PATTERN && n[i].getKind()!=kind::INST_NO_PATTERN && n[i].getKind()!=kind::INST_ATTRIBUTE ){
@@ -129,7 +129,7 @@ struct QuantifierInstPatternListTypeRule {
 struct QuantifierInstClosureTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
   {
-    Assert(n.getKind() == kind::INST_CLOSURE );
+    Assert(n.getKind() == kind::INST_CLOSURE);
     if( check ){
       TypeNode tn = n[0].getType(check);
       if( tn.isBoolean() ){
@@ -157,7 +157,7 @@ public:
                                      bool check)
   {
     Debug("typecheck-r") << "type check for rr " << n << std::endl;
-    Assert(n.getKind() == kind::REWRITE_RULE && n.getNumChildren()==3 );
+    Assert(n.getKind() == kind::REWRITE_RULE && n.getNumChildren() == 3);
     if( check ){
       if( n[ 0 ].getType(check)!=nodeManager->boundVarListType() ){
         throw TypeCheckingExceptionPrivate(n[0],
@@ -182,7 +182,7 @@ public:
 
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
   {
-    Assert(n.getKind() == kind::RR_REWRITE );
+    Assert(n.getKind() == kind::RR_REWRITE);
     if( check ){
       if( n[0].getType(check)!=n[1].getType(check) ){
         throw TypeCheckingExceptionPrivate(n,
@@ -204,8 +204,8 @@ public:
 
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
   {
-    Assert(n.getKind() == kind::RR_REDUCTION ||
-           n.getKind() == kind::RR_DEDUCTION );
+    Assert(n.getKind() == kind::RR_REDUCTION
+           || n.getKind() == kind::RR_DEDUCTION);
     if( check ){
       if( n[ 0 ].getType(check)!=nodeManager->booleanType() ){
         throw TypeCheckingExceptionPrivate(n, "head of reduction rule is not boolean");