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

9 files changed, 91 insertions, 71 deletions

diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index 87696ef5f..bb1e434f2 100644
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -65,8 +65,8 @@ void Region::addRep( Node n ) {
 }
 
 void Region::takeNode( Region* r, Node n ){
-  Assert( !hasRep( n ) );
-  Assert( r->hasRep( n ) );
+  Assert(!hasRep(n));
+  Assert(r->hasRep(n));
   //add representative
   setRep( n, true );
   //take disequalities from r
@@ -130,7 +130,7 @@ void Region::combine( Region* r ){
 
 /** setEqual */
 void Region::setEqual( Node a, Node b ){
-  Assert( hasRep( a ) && hasRep( b ) );
+  Assert(hasRep(a) && hasRep(b));
   //move disequalities of b over to a
   for( int t=0; t<2; t++ ){
     DiseqList* del = d_nodes[b]->get(t);
@@ -181,7 +181,7 @@ void Region::setDisequal( Node n1, Node n2, int type, bool valid ){
 }
 
 void Region::setRep( Node n, bool valid ) {
-  Assert( hasRep( n )!=valid );
+  Assert(hasRep(n) != valid);
   if( valid && d_nodes.find( n )==d_nodes.end() ){
     d_nodes[n] = new RegionNodeInfo( d_cf->d_thss->getSatContext() );
   }
@@ -189,7 +189,7 @@ void Region::setRep( Node n, bool valid ) {
   d_reps_size = d_reps_size + ( valid ? 1 : -1 );
   //removing a member of the test clique from this region
   if( d_testClique.find( n ) != d_testClique.end() && d_testClique[n] ){
-    Assert( !valid );
+    Assert(!valid);
     d_testClique[n] = false;
     d_testCliqueSize = d_testCliqueSize - 1;
     //remove all splits involving n
@@ -326,7 +326,7 @@ bool Region::check( Theory::Effort level, int cardinality,
               }
             }
           }
-          Assert( maxNode!=Node::null() );
+          Assert(maxNode != Node::null());
           newClique.push_back( maxNode );
         }
         //check splits internal to new members
@@ -540,7 +540,7 @@ void SortModel::newEqClass( Node n ){
         if( d_regions_index<d_regions.size() ){
           d_regions[ d_regions_index ]->debugPrint("uf-ss-debug",true);
           d_regions[ d_regions_index ]->setValid(true);
-          Assert(d_regions[d_regions_index]->getNumReps()==0);
+          Assert(d_regions[d_regions_index]->getNumReps() == 0);
         }else{
           d_regions.push_back( new Region( this, d_thss->getSatContext() ) );
         }
@@ -564,8 +564,8 @@ void SortModel::merge( Node a, Node b ){
       Debug("uf-ss") << "CardinalityExtension: Merging " << a << " = " << b
                      << "..." << std::endl;
       if( a!=b ){
-        Assert( d_regions_map.find( a )!=d_regions_map.end() );
-        Assert( d_regions_map.find( b )!=d_regions_map.end() );
+        Assert(d_regions_map.find(a) != d_regions_map.end());
+        Assert(d_regions_map.find(b) != d_regions_map.end());
         int ai = d_regions_map[a];
         int bi = d_regions_map[b];
         Debug("uf-ss") << "   regions: " << ai << " " << bi << std::endl;
@@ -636,8 +636,8 @@ void SortModel::assertDisequal( Node a, Node b, Node reason ){
         }
         d_disequalities_index = d_disequalities_index + 1;
         //now, add disequalities to regions
-        Assert( d_regions_map.find( a )!=d_regions_map.end() );
-        Assert( d_regions_map.find( b )!=d_regions_map.end() );
+        Assert(d_regions_map.find(a) != d_regions_map.end());
+        Assert(d_regions_map.find(b) != d_regions_map.end());
         Debug("uf-ss") << "   regions: " << ai << " " << bi << std::endl;
         if( ai==bi ){
           //internal disequality
@@ -671,7 +671,7 @@ bool SortModel::areDisequal( Node a, Node b ) {
 
 /** check */
 void SortModel::check( Theory::Effort level, OutputChannel* out ){
-  Assert( options::ufssMode()==UF_SS_FULL );
+  Assert(options::ufssMode() == UF_SS_FULL);
   if( level>=Theory::EFFORT_STANDARD && d_hasCard && !d_conflict ){
     Debug("uf-ss") << "CardinalityExtension: Check " << level << " " << d_type
                    << std::endl;
@@ -809,7 +809,7 @@ void SortModel::getDisequalitiesToRegions(int ri,
       DiseqList* del = it->second->get(0);
       for( DiseqList::iterator it2 = del->begin(); it2 != del->end(); ++it2 ){
         if( (*it2).second ){
-          Assert( isValid( d_regions_map[ (*it2).first ] ) );
+          Assert(isValid(d_regions_map[(*it2).first]));
           //Notice() << "Found disequality with " << (*it2).first << ", region = " << d_regions_map[ (*it2).first ] << std::endl;
           regions_diseq[ d_regions_map[ (*it2).first ] ]++;
         }
@@ -836,7 +836,7 @@ void SortModel::assertCardinality( OutputChannel* out, int c, bool val ){
         << "Assert cardinality " << d_type << " " << c << " " << val
         << " level = "
         << d_thss->getTheory()->getValuation().getAssertionLevel() << std::endl;
-    Assert( c>0 );
+    Assert(c > 0);
     Node cl = getCardinalityLiteral( c );
     if( val ){
       bool doCheckRegions = !d_hasCard;
@@ -883,7 +883,7 @@ void SortModel::assertCardinality( OutputChannel* out, int c, bool val ){
 
 void SortModel::checkRegion( int ri, bool checkCombine ){
   if( isValid(ri) && d_hasCard ){
-    Assert( d_cardinality>0 );
+    Assert(d_cardinality > 0);
     if( checkCombine && d_regions[ri]->getMustCombine( d_cardinality ) ){
       ////alternatively, check if we can reduce the number of external disequalities by moving single nodes
       //for( std::map< Node, bool >::iterator it = d_regions[i]->d_reps.begin(); it != d_regions[i]->d_reps.end(); ++it ){
@@ -931,9 +931,9 @@ int SortModel::forceCombineRegion( int ri, bool useDensity ){
       Debug("uf-ss-check-region") << it->first << " : " << it->second << std::endl;
     }
     for( std::map< int, int >::iterator it = regions_diseq.begin(); it != regions_diseq.end(); ++it ){
-      Assert( it->first!=ri );
-      Assert( isValid( it->first ) );
-      Assert( d_regions[ it->first ]->getNumReps()>0 );
+      Assert(it->first != ri);
+      Assert(isValid(it->first));
+      Assert(d_regions[it->first]->getNumReps() > 0);
       double tempScore = double(it->second)/double(d_regions[it->first]->getNumReps() );
       if( tempScore>maxScore ){
         maxRegion = it->first;
@@ -959,7 +959,7 @@ int SortModel::combineRegions( int ai, int bi ){
   }
 #endif
   Debug("uf-ss-region") << "uf-ss: Combine Region #" << bi << " with Region #" << ai << std::endl;
-  Assert( isValid( ai ) && isValid( bi ) );
+  Assert(isValid(ai) && isValid(bi));
   Region* region_bi = d_regions[bi];
   for(Region::iterator it = region_bi->begin(); it != region_bi->end(); ++it){
     Region::RegionNodeInfo* rni = it->second;
@@ -975,8 +975,8 @@ int SortModel::combineRegions( int ai, int bi ){
 
 void SortModel::moveNode( Node n, int ri ){
   Debug("uf-ss-region") << "uf-ss: Move node " << n << " to Region #" << ri << std::endl;
-  Assert( isValid( d_regions_map[ n ] ) );
-  Assert( isValid( ri ) );
+  Assert(isValid(d_regions_map[n]));
+  Assert(isValid(ri));
   //move node to region ri
   d_regions[ri]->takeNode( d_regions[ d_regions_map[n] ], n );
   d_regions_map[n] = ri;
@@ -993,11 +993,11 @@ int SortModel::addSplit( Region* r, OutputChannel* out ){
         break;
       }
     }
-    Assert( s!=Node::null() );
+    Assert(s != Node::null());
   }
   if (!s.isNull() ){
     //add lemma to output channel
-    Assert( s.getKind()==EQUAL );
+    Assert(s.getKind() == EQUAL);
     Node ss = Rewriter::rewrite( s );
     if( ss.getKind()!=EQUAL ){
       Node b_t = NodeManager::currentNM()->mkConst( true );
@@ -1042,8 +1042,8 @@ int SortModel::addSplit( Region* r, OutputChannel* out ){
 
 
 void SortModel::addCliqueLemma( std::vector< Node >& clique, OutputChannel* out ){
-  Assert( d_hasCard );
-  Assert( d_cardinality>0 );
+  Assert(d_hasCard);
+  Assert(d_cardinality > 0);
   while( clique.size()>size_t(d_cardinality+1) ){
     clique.pop_back();
   }
@@ -1454,8 +1454,8 @@ void CardinalityExtension::assertNode(Node n, bool isDecision)
   if( options::ufssMode()==UF_SS_FULL ){
     if( lit.getKind()==CARDINALITY_CONSTRAINT ){
       TypeNode tn = lit[0].getType();
-      Assert( tn.isSort() );
-      Assert( d_rep_model[tn] );
+      Assert(tn.isSort());
+      Assert(d_rep_model[tn]);
       int nCard = lit[1].getConst<Rational>().getNumerator().getSignedInt();
       Node ct = d_rep_model[tn]->getCardinalityTerm();
       Trace("uf-ss-debug") << "...check cardinality terms : " << lit[0] << " " << ct << std::endl;
@@ -1627,7 +1627,7 @@ void CardinalityExtension::check(Theory::Effort level)
       }
     }else{
       // unhandled uf ss mode
-      Assert( false );
+      Assert(false);
     }
     Trace("uf-ss-solver") << "Done CardinalityExtension: check " << level
                           << std::endl;
@@ -1776,7 +1776,7 @@ void CardinalityExtension::initializeCombinedCardinality()
 /** check */
 void CardinalityExtension::checkCombinedCardinality()
 {
-  Assert( options::ufssMode()==UF_SS_FULL );
+  Assert(options::ufssMode() == UF_SS_FULL);
   if( options::ufssFairness() ){
     Trace("uf-ss-com-card-debug") << "Check combined cardinality, get maximum negative cardinalities..." << std::endl;
     int totalCombinedCard = 0;
diff --git a/src/theory/uf/cardinality_extension.h b/src/theory/uf/cardinality_extension.h
index 3e3d90be5..37d442968 100644
--- a/src/theory/uf/cardinality_extension.h
+++ b/src/theory/uf/cardinality_extension.h
@@ -76,7 +76,7 @@ class CardinalityExtension
           ~DiseqList(){}
 
           void setDisequal( Node n, bool valid ){
-            Assert( (!isSet(n)) || getDisequalityValue(n) != valid );
+            Assert((!isSet(n)) || getDisequalityValue(n) != valid);
             d_disequalities[ n ] = valid;
             d_size = d_size + ( valid ? 1 : -1 );
           }
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 32d32b479..8e0c96ae3 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -375,7 +375,7 @@ bool EqualityEngine::hasTerm(TNode t) const {
 }
 
 EqualityNodeId EqualityEngine::getNodeId(TNode node) const {
-  Assert(hasTerm(node), node.toString().c_str());
+  Assert(hasTerm(node)) << node;
   return (*d_nodeIds.find(node)).second;
 }
 
@@ -417,7 +417,7 @@ void EqualityEngine::assertEqualityInternal(TNode t1, TNode t2, TNode reason, un
 
 void EqualityEngine::assertPredicate(TNode t, bool polarity, TNode reason, unsigned pid) {
   Debug("equality") << d_name << "::eq::addPredicate(" << t << "," << (polarity ? "true" : "false") << ")" << std::endl;
-  Assert(t.getKind() != kind::EQUAL, "Use assertEquality instead");
+  Assert(t.getKind() != kind::EQUAL) << "Use assertEquality instead";
   assertEqualityInternal(t, polarity ? d_true : d_false, reason, pid);
   propagate();
 }
@@ -556,8 +556,9 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
   // Check for constant merges
   bool class1isConstant = d_isConstant[class1Id];
   bool class2isConstant = d_isConstant[class2Id];
-  Assert(class1isConstant || !class2isConstant, "Should always merge into constants");
-  Assert(!class1isConstant || !class2isConstant, "Don't merge constants");
+  Assert(class1isConstant || !class2isConstant)
+      << "Should always merge into constants";
+  Assert(!class1isConstant || !class2isConstant) << "Don't merge constants";
 
   // Trigger set of class 1
   TriggerTermSetRef class1triggerRef = d_nodeIndividualTrigger[class1Id];
@@ -884,7 +885,8 @@ void EqualityEngine::backtrack() {
   if (d_deducedDisequalities.size() > d_deducedDisequalitiesSize) {
     for(int i = d_deducedDisequalities.size() - 1, i_end = (int)d_deducedDisequalitiesSize; i >= i_end; -- i) {
       EqualityPair pair = d_deducedDisequalities[i];
-      Assert(d_disequalityReasonsMap.find(pair) != d_disequalityReasonsMap.end());
+      Assert(d_disequalityReasonsMap.find(pair)
+             != d_disequalityReasonsMap.end());
       // Remove from the map
       d_disequalityReasonsMap.erase(pair);
       std::swap(pair.first, pair.second);
@@ -934,7 +936,8 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity,
                   << ", proof = " << (eqp ? "ON" : "OFF") << std::endl;
 
   // The terms must be there already
-  Assert(hasTerm(t1) && hasTerm(t2));;
+  Assert(hasTerm(t1) && hasTerm(t2));
+  ;
 
   // Get the ids
   EqualityNodeId t1Id = getNodeId(t1);
@@ -952,7 +955,8 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity,
 
     // Get the reason for this disequality
     EqualityPair pair(t1Id, t2Id);
-    Assert(d_disequalityReasonsMap.find(pair) != d_disequalityReasonsMap.end(), "Don't ask for stuff I didn't notify you about");
+    Assert(d_disequalityReasonsMap.find(pair) != d_disequalityReasonsMap.end())
+        << "Don't ask for stuff I didn't notify you about";
     DisequalityReasonRef reasonRef = d_disequalityReasonsMap.find(pair)->second;
 
     for (unsigned i = reasonRef.mergesStart; i < reasonRef.mergesEnd; ++ i) {
@@ -1219,7 +1223,8 @@ void EqualityEngine::getExplanation(
                       eqpc->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_SELECT_1, d_nodes[f1.b]);
                       // The first child is a PARTIAL_SELECT_0.
                       // Give it a child so that we know what kind of (read) it is, when we dump to LFSC.
-                      Assert(eqpc->d_children[0]->d_node.getKind() == kind::PARTIAL_SELECT_0);
+                      Assert(eqpc->d_children[0]->d_node.getKind()
+                             == kind::PARTIAL_SELECT_0);
                       Assert(eqpc->d_children[0]->d_children.size() == 0);
 
                       eqpc->d_children[0]->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_SELECT_0,
@@ -1241,7 +1246,7 @@ void EqualityEngine::getExplanation(
               Debug("equality") << d_name << "::eq::getExplanation(): due to reflexivity, going deeper" << std::endl;
               EqualityNodeId eqId = currentNode == d_trueId ? edgeNode : currentNode;
               const FunctionApplication& eq = d_applications[eqId].original;
-              Assert(eq.isEquality(), "Must be an equality");
+              Assert(eq.isEquality()) << "Must be an equality";
 
               // Explain why a = b constant
               Debug("equality") << push;
@@ -1416,8 +1421,10 @@ void EqualityEngine::addTriggerEquality(TNode eq) {
 }
 
 void EqualityEngine::addTriggerPredicate(TNode predicate) {
-  Assert(predicate.getKind() != kind::NOT && predicate.getKind() != kind::EQUAL);
-  Assert(d_congruenceKinds.tst(predicate.getKind()), "No point in adding non-congruence predicates");
+  Assert(predicate.getKind() != kind::NOT
+         && predicate.getKind() != kind::EQUAL);
+  Assert(d_congruenceKinds.tst(predicate.getKind()))
+      << "No point in adding non-congruence predicates";
 
   if (d_done) {
     return;
@@ -1811,7 +1818,8 @@ size_t EqualityEngine::getSize(TNode t) {
 
 void EqualityEngine::addPathReconstructionTrigger(unsigned trigger, const PathReconstructionNotify* notify) {
   // Currently we can only inform one callback per trigger
-  Assert(d_pathReconstructionTriggers.find(trigger) == d_pathReconstructionTriggers.end());
+  Assert(d_pathReconstructionTriggers.find(trigger)
+         == d_pathReconstructionTriggers.end());
   d_pathReconstructionTriggers[trigger] = notify;
 }
 
@@ -1993,7 +2001,7 @@ bool EqualityEngine::hasPropagatedDisequality(EqualityNodeId lhsId, EqualityNode
   bool propagated = d_propagatedDisequalities.find(eq) != d_propagatedDisequalities.end();
 #ifdef CVC4_ASSERTIONS
   bool stored = d_disequalityReasonsMap.find(eq) != d_disequalityReasonsMap.end();
-  Assert(propagated == stored, "These two should be in sync");
+  Assert(propagated == stored) << "These two should be in sync";
 #endif
   Debug("equality::disequality") << d_name << "::eq::hasPropagatedDisequality(" << d_nodes[lhsId] << ", " << d_nodes[rhsId] << ") => " << (propagated ? "true" : "false") << std::endl;
   return propagated;
@@ -2005,11 +2013,13 @@ bool EqualityEngine::hasPropagatedDisequality(TheoryId tag, EqualityNodeId lhsId
 
   PropagatedDisequalitiesMap::const_iterator it = d_propagatedDisequalities.find(eq);
   if (it == d_propagatedDisequalities.end()) {
-    Assert(d_disequalityReasonsMap.find(eq) == d_disequalityReasonsMap.end(), "Why do we have a proof if not propagated");
+    Assert(d_disequalityReasonsMap.find(eq) == d_disequalityReasonsMap.end())
+        << "Why do we have a proof if not propagated";
     Debug("equality::disequality") << d_name << "::eq::hasPropagatedDisequality(" << tag << ", " << d_nodes[lhsId] << ", " << d_nodes[rhsId] << ") => false" << std::endl;
     return false;
   }
-  Assert(d_disequalityReasonsMap.find(eq) != d_disequalityReasonsMap.end(), "We propagated but there is no proof");
+  Assert(d_disequalityReasonsMap.find(eq) != d_disequalityReasonsMap.end())
+      << "We propagated but there is no proof";
   bool result = Theory::setContains(tag, (*it).second);
   Debug("equality::disequality") << d_name << "::eq::hasPropagatedDisequality(" << tag << ", " << d_nodes[lhsId] << ", " << d_nodes[rhsId] << ") => " << (result ? "true" : "false") << std::endl;
   return result;
@@ -2017,9 +2027,9 @@ bool EqualityEngine::hasPropagatedDisequality(TheoryId tag, EqualityNodeId lhsId
 
 
 void EqualityEngine::storePropagatedDisequality(TheoryId tag, EqualityNodeId lhsId, EqualityNodeId rhsId) {
-
-  Assert(!hasPropagatedDisequality(tag, lhsId, rhsId), "Check before you store it");
-  Assert(lhsId != rhsId, "Wow, wtf!");
+  Assert(!hasPropagatedDisequality(tag, lhsId, rhsId))
+      << "Check before you store it";
+  Assert(lhsId != rhsId) << "Wow, wtf!";
 
   Debug("equality::disequality") << d_name << "::eq::storePropagatedDisequality(" << tag << ", " << d_nodes[lhsId] << ", " << d_nodes[rhsId] << ")" << std::endl;
 
@@ -2040,12 +2050,15 @@ void EqualityEngine::storePropagatedDisequality(TheoryId tag, EqualityNodeId lhs
   // Store the proof if provided
   if (d_deducedDisequalityReasons.size() > d_deducedDisequalityReasonsSize) {
     Debug("equality::disequality") << d_name << "::eq::storePropagatedDisequality(" << tag << ", " << d_nodes[lhsId] << ", " << d_nodes[rhsId] << "): storing proof" << std::endl;
-    Assert(d_disequalityReasonsMap.find(pair1) == d_disequalityReasonsMap.end(), "There can't be a proof if you're adding a new one");
+    Assert(d_disequalityReasonsMap.find(pair1) == d_disequalityReasonsMap.end())
+        << "There can't be a proof if you're adding a new one";
     DisequalityReasonRef ref(d_deducedDisequalityReasonsSize, d_deducedDisequalityReasons.size());
 #ifdef CVC4_ASSERTIONS
     // Check that the reasons are valid
     for (unsigned i = ref.mergesStart; i < ref.mergesEnd; ++ i) {
-      Assert(getEqualityNode(d_deducedDisequalityReasons[i].first).getFind() == getEqualityNode(d_deducedDisequalityReasons[i].second).getFind());
+      Assert(
+          getEqualityNode(d_deducedDisequalityReasons[i].first).getFind()
+          == getEqualityNode(d_deducedDisequalityReasons[i].second).getFind());
     }
 #endif
     if (Debug.isOn("equality::disequality")) {
@@ -2065,7 +2078,8 @@ void EqualityEngine::storePropagatedDisequality(TheoryId tag, EqualityNodeId lhs
     d_disequalityReasonsMap[pair1] = ref;
     d_disequalityReasonsMap[pair2] = ref;
   } else {
-    Assert(d_disequalityReasonsMap.find(pair1) != d_disequalityReasonsMap.end(), "You must provide a proof initially");
+    Assert(d_disequalityReasonsMap.find(pair1) != d_disequalityReasonsMap.end())
+        << "You must provide a proof initially";
   }
 }
 
@@ -2073,7 +2087,11 @@ void EqualityEngine::getDisequalities(bool allowConstants, EqualityNodeId classI
   // Must be empty on input
   Assert(out.size() == 0);
   // The class we are looking for, shouldn't have any of the tags we are looking for already set
-  Assert(d_nodeIndividualTrigger[classId] == null_set_id || Theory::setIntersection(getTriggerTermSet(d_nodeIndividualTrigger[classId]).tags, inputTags) == 0);
+  Assert(d_nodeIndividualTrigger[classId] == null_set_id
+         || Theory::setIntersection(
+                getTriggerTermSet(d_nodeIndividualTrigger[classId]).tags,
+                inputTags)
+                == 0);
 
   if (inputTags == 0) {
     return;
@@ -2259,7 +2277,7 @@ EqClassIterator::EqClassIterator(Node eqc, const eq::EqualityEngine* ee)
   Assert(d_ee->consistent());
   d_current = d_start = d_ee->getNodeId(eqc);
   Assert(d_start == d_ee->getEqualityNode(d_start).getFind());
-  Assert (!d_ee->d_isInternal[d_start]);
+  Assert(!d_ee->d_isInternal[d_start]);
 }
 
 Node EqClassIterator::operator*() const {
diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h
index 3813bb697..402b21a02 100644
--- a/src/theory/uf/equality_engine_types.h
+++ b/src/theory/uf/equality_engine_types.h
@@ -261,7 +261,7 @@ public:
    */
   template<typename memory_class>
   void removeTopFromUseList(memory_class& memory) {
-    Assert ((int) d_useList == (int)memory.size() - 1);
+    Assert((int)d_useList == (int)memory.size() - 1);
     d_useList = memory.back().getNext();
     memory.pop_back();
   }
diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp
index 9c1d4c2f1..56d0c59cc 100644
--- a/src/theory/uf/symmetry_breaker.cpp
+++ b/src/theory/uf/symmetry_breaker.cpp
@@ -86,8 +86,7 @@ bool SymmetryBreaker::Template::matchRecursive(TNode t, TNode n) {
       Debug("ufsymm:match") << "UFSYMM we have constants, failing match" << endl;
       return false;
     }
-    Assert(t.isVar() &&
-           n.isVar());
+    Assert(t.isVar() && n.isVar());
     t = find(t);
     n = find(n);
     Debug("ufsymm:match") << "UFSYMM variable match " << t << " , " << n << endl;
@@ -720,7 +719,8 @@ void SymmetryBreaker::selectTerms(const Permutation& p) {
               Debug("ufsymm:eq") << "UFSYMM              -- yep" << endl;
             }
           }
-          Assert(j != teq.end(), "failed to find a difference between p and teq ?!");
+          Assert(j != teq.end())
+              << "failed to find a difference between p and teq ?!";
         }
       }
     } else {
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 76e6e08bc..95e3f702b 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -188,7 +188,7 @@ void TheoryUF::check(Effort level) {
 }/* TheoryUF::check() */
 
 Node TheoryUF::getOperatorForApplyTerm( TNode node ) {
-  Assert( node.getKind()==kind::APPLY_UF || node.getKind()==kind::HO_APPLY );
+  Assert(node.getKind() == kind::APPLY_UF || node.getKind() == kind::HO_APPLY);
   if( node.getKind()==kind::APPLY_UF ){
     return node.getOperator();
   }else{
@@ -197,7 +197,7 @@ Node TheoryUF::getOperatorForApplyTerm( TNode node ) {
 }
 
 unsigned TheoryUF::getArgumentStartIndexForApplyTerm( TNode node ) {
-  Assert( node.getKind()==kind::APPLY_UF || node.getKind()==kind::HO_APPLY );
+  Assert(node.getKind() == kind::APPLY_UF || node.getKind() == kind::HO_APPLY);
   return node.getKind()==kind::APPLY_UF ? 0 : 1;
 }
 
@@ -230,7 +230,7 @@ void TheoryUF::preRegisterTerm(TNode node) {
 
   // we always use APPLY_UF if not higher-order, HO_APPLY if higher-order
   //Assert( node.getKind()!=kind::APPLY_UF || !options::ufHo() );
-  Assert( node.getKind()!=kind::HO_APPLY || options::ufHo() );
+  Assert(node.getKind() != kind::HO_APPLY || options::ufHo());
 
   switch (node.getKind()) {
   case kind::EQUAL:
@@ -507,8 +507,8 @@ void TheoryUF::addSharedTerm(TNode t) {
 }
 
 bool TheoryUF::areCareDisequal(TNode x, TNode y){
-  Assert( d_equalityEngine.hasTerm(x) );
-  Assert( d_equalityEngine.hasTerm(y) );
+  Assert(d_equalityEngine.hasTerm(x));
+  Assert(d_equalityEngine.hasTerm(y));
   if( d_equalityEngine.isTriggerTerm(x, THEORY_UF) && d_equalityEngine.isTriggerTerm(y, THEORY_UF) ){
     TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_UF);
     TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_UF);
@@ -536,10 +536,10 @@ void TheoryUF::addCarePairs(TNodeTrie* t1,
         for (unsigned k = arg_start_index; k < f1.getNumChildren(); ++ k) {
           TNode x = f1[k];
           TNode y = f2[k];
-          Assert( d_equalityEngine.hasTerm(x) );
-          Assert( d_equalityEngine.hasTerm(y) );
-          Assert( !d_equalityEngine.areDisequal( x, y, false ) );
-          Assert( !areCareDisequal( x, y ) );
+          Assert(d_equalityEngine.hasTerm(x));
+          Assert(d_equalityEngine.hasTerm(y));
+          Assert(!d_equalityEngine.areDisequal(x, y, false));
+          Assert(!areCareDisequal(x, y));
           if( !d_equalityEngine.areEqual( x, y ) ){
             if( d_equalityEngine.isTriggerTerm(x, THEORY_UF) && d_equalityEngine.isTriggerTerm(y, THEORY_UF) ){
               TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_UF);
diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp
index f279aebaf..ffe3730c4 100644
--- a/src/theory/uf/theory_uf_model.cpp
+++ b/src/theory/uf/theory_uf_model.cpp
@@ -91,7 +91,9 @@ Node UfModelTreeNode::getFunctionValue(std::vector<Node>& args, int index, Node
             stk.push(val);
             val = val[2];
           } while(val.getKind() == ITE);
-          AlwaysAssert(val == defaultValue, "default values don't match when constructing function definition!");
+          AlwaysAssert(val == defaultValue)
+              << "default values don't match when constructing function "
+                 "definition!";
           while(!stk.empty()) {
             val = stk.top();
             stk.pop();
diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h
index bad4189d6..7f4c1c164 100644
--- a/src/theory/uf/theory_uf_rewriter.h
+++ b/src/theory/uf/theory_uf_rewriter.h
@@ -160,7 +160,7 @@ public:
 public: //conversion between HO_APPLY AND APPLY_UF
   // converts an APPLY_UF to a curried HO_APPLY e.g. (f a b) becomes (@ (@ f a) b)
   static Node getHoApplyForApplyUf(TNode n) {
-    Assert( n.getKind()==kind::APPLY_UF );
+    Assert(n.getKind() == kind::APPLY_UF);
     Node curr = n.getOperator();
     for( unsigned i=0; i<n.getNumChildren(); i++ ){
       curr = NodeManager::currentNM()->mkNode( kind::HO_APPLY, curr, n[i] );     
@@ -169,7 +169,7 @@ public: //conversion between HO_APPLY AND APPLY_UF
   }
   // converts a curried HO_APPLY into an APPLY_UF e.g. (@ (@ f a) b) becomes (f a b)
   static Node getApplyUfForHoApply(TNode n) {
-    Assert( n.getType().getNumChildren()==2 );
+    Assert(n.getType().getNumChildren() == 2);
     std::vector< TNode > children;
     TNode curr = decomposeHoApply( n, children, true );
     // if operator is standard
diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h
index cb373b535..f782cd618 100644
--- a/src/theory/uf/theory_uf_type_rules.h
+++ b/src/theory/uf/theory_uf_type_rules.h
@@ -145,13 +145,13 @@ class HoApplyTypeRule {
   // the typing rule for HO_APPLY terms
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
                                      bool check) {
-    Assert( n.getKind()==kind::HO_APPLY );
+    Assert(n.getKind() == kind::HO_APPLY);
     TypeNode fType = n[0].getType(check);
     if (!fType.isFunction()) {
       throw TypeCheckingExceptionPrivate(
           n, "first argument does not have function type");
     }
-    Assert( fType.getNumChildren()>=2 );
+    Assert(fType.getNumChildren() >= 2);
     if (check) {
       TypeNode aType = n[1].getType(check);
       if( !aType.isSubtypeOf( fType[0] ) ){