1 files changed, 14 insertions, 23 deletions

diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index c7251d4c4..e7b1289a4 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -63,8 +63,7 @@ ConstraintType Constraint::constraintTypeOfComparison(const Comparison& cmp){
     return Equality;
   case DISTINCT:
     return Disequality;
-  default:
-    Unhandled(k);
+  default: Unhandled() << k;
   }
 }
 
@@ -322,20 +321,11 @@ void ValueCollection::add(ConstraintP c){
 
 ConstraintP ValueCollection::getConstraintOfType(ConstraintType t) const{
   switch(t){
-  case LowerBound:
-    Assert(hasLowerBound());
-    return d_lowerBound;
-  case Equality:
-    Assert(hasEquality());
-    return d_equality;
-  case UpperBound:
-    Assert(hasUpperBound());
-    return d_upperBound;
-  case Disequality:
-    Assert(hasDisequality());
-    return d_disequality;
-  default:
-    Unreachable();
+    case LowerBound: Assert(hasLowerBound()); return d_lowerBound;
+    case Equality: Assert(hasEquality()); return d_equality;
+    case UpperBound: Assert(hasUpperBound()); return d_upperBound;
+    case Disequality: Assert(hasDisequality()); return d_disequality;
+    default: Unreachable();
   }
 }
 
@@ -613,7 +603,7 @@ void ConstraintRule::print(std::ostream& out) const {
         out << "_";
       }
       out << " * (" << *antecedent << ")" << std::endl;
-      
+
       Assert((coeffs == RationalVectorCPSentinel) || coeffIterator > 0);
       --p;
       coeffIterator = (coeffs != RationalVectorCPSentinel) ? coeffIterator-1 : 0;
@@ -862,7 +852,8 @@ ConstraintP ConstraintDatabase::getConstraint(ArithVar v, ConstraintType t, cons
       pair<SortedConstraintMapIterator, bool> negInsertAttempt;
       negInsertAttempt = scm.insert(make_pair(negC->getValue(), ValueCollection()));
       Assert(negInsertAttempt.second
-             || ! negInsertAttempt.first->second.hasConstraintOfType(negC->getType()));
+             || !negInsertAttempt.first->second.hasConstraintOfType(
+                 negC->getType()));
       negPos = negInsertAttempt.first;
     }
 
@@ -1108,7 +1099,7 @@ void Constraint::setAssumption(bool nowInConflict){
   Assert(assertedToTheTheory());
 
   d_database->pushConstraintRule(ConstraintRule(this, AssumeAP));
-  
+
   Assert(inConflict() == nowInConflict);
   if(Debug.isOn("constraint::conflictCommit") && inConflict()){
     Debug("constraint::conflictCommit") << "inConflict@setAssumption " << this << std::endl;
@@ -1149,7 +1140,6 @@ void Constraint::impliedByUnate(ConstraintCP imp, bool nowInConflict){
   Assert(imp->hasProof());
   Assert(negationHasProof() == nowInConflict);
 
-
   d_database->d_antecedents.push_back(NullConstraint);
   d_database->d_antecedents.push_back(imp);
 
@@ -1283,7 +1273,7 @@ void Constraint::impliedByFarkas(const ConstraintCPVec& a, RationalVectorCP coef
   Assert(negationHasProof() == nowInConflict);
   Assert(allHaveProof(a));
 
-  Assert( PROOF_ON() == (coeffs != RationalVectorCPSentinel) );
+  Assert(PROOF_ON() == (coeffs != RationalVectorCPSentinel));
   // !PROOF_ON() => coeffs == RationalVectorCPSentinel
   //  PROOF_ON() => coeffs->size() == a.size() + 1
   Assert(!PROOF_ON() || coeffs->size() == a.size() + 1);
@@ -1404,7 +1394,8 @@ void Constraint::assertionFringe(ConstraintCPVec& v){
           v[writePos] = vi;
           writePos++;
         }else{
-          Assert(vi->hasTrichotomyProof() || vi->hasFarkasProof() || vi->hasIntHoleProof() );
+          Assert(vi->hasTrichotomyProof() || vi->hasFarkasProof()
+                 || vi->hasIntHoleProof());
           AntecedentId p = vi->getEndAntecedent();
 
           ConstraintCP antecedent = antecedents[p];
@@ -1561,7 +1552,7 @@ ConstraintP Constraint::getStrictlyWeakerUpperBound(bool hasLiteral, bool assert
 
 ConstraintP ConstraintDatabase::getBestImpliedBound(ArithVar v, ConstraintType t, const DeltaRational& r) const {
   Assert(variableDatabaseIsSetup(v));
-  Assert(t == UpperBound ||  t == LowerBound);
+  Assert(t == UpperBound || t == LowerBound);
 
   SortedConstraintMap& scm = getVariableSCM(v);
   if(t == UpperBound){