1 files changed, 10 insertions, 9 deletions

diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp
index 827323302..29177d3f4 100644
--- a/src/theory/arith/fc_simplex.cpp
+++ b/src/theory/arith/fc_simplex.cpp
@@ -118,8 +118,7 @@ Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){
   }else if(d_errorSet.errorEmpty()){
     //if(verbose){ Message() << "fcFindModel("<< instance <<") fixed itself" << endl; }
     Debug("arith::findModel") << "fcFindModel("<< instance <<") fixed itself" << endl;
-    if(verbose)
-    Assert(!d_errorSet.moreSignals());
+    if (verbose) Assert(!d_errorSet.moreSignals());
     Assert(d_conflictVariables.empty());
     return Result::SAT;
   }
@@ -264,7 +263,7 @@ WitnessImprovement FCSimplexDecisionProcedure::adjustFocusShrank(const ArithVarV
 WitnessImprovement FCSimplexDecisionProcedure::focusDownToJust(ArithVar v){
   // uint32_t newErrorSize = d_errorSet.errorSize();
   // uint32_t newFocusSize = d_errorSet.focusSize();
-  Assert(d_focusSize ==  d_errorSet.focusSize());
+  Assert(d_focusSize == d_errorSet.focusSize());
   Assert(d_focusSize > 1);
   Assert(d_errorSet.inFocus(v));
 
@@ -558,7 +557,8 @@ void FCSimplexDecisionProcedure::updateAndSignal(const UpdateInfo& selected, Wit
     int prevFocusSgn = d_errorSet.popSignal();
 
     if(d_tableau.isBasic(updated)){
-      Assert(!d_variables.assignmentIsConsistent(updated) == d_errorSet.inError(updated));
+      Assert(!d_variables.assignmentIsConsistent(updated)
+             == d_errorSet.inError(updated));
       if(Debug.isOn("updateAndSignal")){debugPrintSignal(updated);}
       if(!d_variables.assignmentIsConsistent(updated)){
         if(checkBasicForConflict(updated)){
@@ -582,7 +582,8 @@ void FCSimplexDecisionProcedure::updateAndSignal(const UpdateInfo& selected, Wit
   }
   if(Debug.isOn("error")){ d_errorSet.debugPrint(Debug("error")); }
 
-  Assert(debugSelectedErrorDropped(selected, d_errorSize, d_errorSet.errorSize()));
+  Assert(
+      debugSelectedErrorDropped(selected, d_errorSize, d_errorSet.errorSize()));
 
   adjustFocusAndError(selected, focusChanges);
 }
@@ -729,7 +730,6 @@ Result::Sat FCSimplexDecisionProcedure::dualLike(){
   Assert(d_conflictVariables.empty());
   Assert(d_focusErrorVar == ARITHVAR_SENTINEL);
 
-
   d_scores.purge();
   d_focusErrorVar = constructInfeasiblityFunction(d_statistics.d_fcFocusConstructionTimer);
 
@@ -752,8 +752,8 @@ Result::Sat FCSimplexDecisionProcedure::dualLike(){
 
       d_focusSize = d_errorSet.focusSize();
 
-      Assert( d_errorSize == d_focusSize);
-      Assert( d_errorSize >= 1 );
+      Assert(d_errorSize == d_focusSize);
+      Assert(d_errorSize >= 1);
 
       d_focusErrorVar = constructInfeasiblityFunction(d_statistics.d_fcFocusConstructionTimer);
 
@@ -795,7 +795,8 @@ Result::Sat FCSimplexDecisionProcedure::dualLike(){
     if(verbose){
       debugDualLike(w,  Message(), instance, prevFocusSize, prevErrorSize);
     }
-    Assert(debugDualLike(w, Debug("dualLike"), instance, prevFocusSize, prevErrorSize));
+    Assert(debugDualLike(
+        w, Debug("dualLike"), instance, prevFocusSize, prevErrorSize));
   }