Remove a bunch of debugging/logging code from the linear solver (#7576)

This PR removes old debugging code from the linear solver.
The removed code was either redundant, already in comments, or manually disabled by a constant false.

diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp
index 89d7619cf383dcc69e6aab6c835e0e45f20d8753..fdcfb063b44c19636b17d3e41f9038a9823b1863 100644 (file)
--- a/src/theory/arith/approx_simplex.cpp
+++ b/src/theory/arith/approx_simplex.cpp
@@ -405,8 +405,6 @@ private:
   bool d_solvedRelaxation;
   bool d_solvedMIP;
 
-  static int s_verbosity;
-
   CutScratchPad d_pad;
 
   std::vector<Integer> d_denomGuesses;
@@ -524,8 +522,6 @@ private:
   double sumInfeasibilities(glp_prob* prob, bool mip) const;
 };
 
-int ApproxGLPK::s_verbosity = 0;
-
 }  // namespace arith
 }  // namespace theory
 }  // namespace cvc5
@@ -629,12 +625,6 @@ ApproxGLPK::ApproxGLPK(const ArithVariables& var,
   for(ArithVariables::var_iterator vi = d_vars.var_begin(), vi_end = d_vars.var_end(); vi != vi_end; ++vi){
     ArithVar v = *vi;
 
-    if (s_verbosity >= 2)
-    {
-      // CVC5Message() << v  << " ";
-      // d_vars.printModel(v, CVC5Message());
-    }
-
     int type;
     double lb = 0.0;
     double ub = 0.0;
@@ -764,12 +754,6 @@ ArithRatPairVec ApproxGLPK::heuristicOptCoeffs() const{
   for(ArithVariables::var_iterator vi = d_vars.var_begin(), vi_end = d_vars.var_end(); vi != vi_end; ++vi){
     ArithVar v = *vi;
 
-    if (s_verbosity >= 2)
-    {
-      CVC5Message() << v << " ";
-      d_vars.printModel(v, CVC5Message());
-    }
-
     int type;
     if(d_vars.hasUpperBound(v) && d_vars.hasLowerBound(v)){
       if(d_vars.boundsAreEqual(v)){
@@ -868,12 +852,6 @@ ArithRatPairVec ApproxGLPK::heuristicOptCoeffs() const{
 
       int dir = guessDir(r);
       if(len >= rowLengthReq){
-        if (s_verbosity >= 1)
-        {
-          CVC5Message() << "high row " << r << " " << len << " " << avgRowLength
-                        << " " << dir << endl;
-          d_vars.printModel(r, CVC5Message());
-        }
         ret.push_back(ArithRatPair(r, Rational(dir)));
       }
     }
@@ -891,12 +869,6 @@ ArithRatPairVec ApproxGLPK::heuristicOptCoeffs() const{
       double ubScore = double(bc.upperBoundCount()) / maxCount;
       double lbScore = double(bc.lowerBoundCount()) / maxCount;
       if(ubScore  >= .9 || lbScore >= .9){
-        if (s_verbosity >= 1)
-        {
-          CVC5Message() << "high col " << c << " " << bc << " " << ubScore
-                        << " " << lbScore << " " << dir << endl;
-          d_vars.printModel(c, CVC5Message());
-        }
         ret.push_back(ArithRatPair(c, Rational(c)));
       }
     }
@@ -1016,26 +988,17 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const
 
     int status = isAux ? glp_get_row_stat(prob, glpk_index)
       : glp_get_col_stat(prob, glpk_index);
-    if (s_verbosity >= 2)
-    {
-      CVC5Message() << "assignment " << vi << endl;
-    }
 
     bool useDefaultAssignment = false;
 
     switch(status){
     case GLP_BS:
-      // CVC5Message() << "basic" << endl;
       newBasis.add(vi);
       useDefaultAssignment = true;
       break;
     case GLP_NL:
     case GLP_NS:
       if(!mip){
-        if (s_verbosity >= 2)
-        {
-          CVC5Message() << "non-basic lb" << endl;
-        }
         newValues.set(vi, d_vars.getLowerBound(vi));
       }else{// intentionally fall through otherwise
         useDefaultAssignment = true;
@@ -1043,10 +1006,6 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const
       break;
     case GLP_NU:
       if(!mip){
-        if (s_verbosity >= 2)
-        {
-          CVC5Message() << "non-basic ub" << endl;
-        }
         newValues.set(vi, d_vars.getUpperBound(vi));
       }else {// intentionally fall through otherwise
         useDefaultAssignment = true;
@@ -1060,10 +1019,6 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const
     }
 
     if(useDefaultAssignment){
-      if (s_verbosity >= 2)
-      {
-        CVC5Message() << "non-basic other" << endl;
-      }
 
       double newAssign;
       if(mip){
@@ -1079,7 +1034,6 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const
           && roughlyEqual(newAssign,
                           d_vars.getLowerBound(vi).approx(SMALL_FIXED_DELTA)))
       {
-        // CVC5Message() << "  to lb" << endl;
 
         newValues.set(vi, d_vars.getLowerBound(vi));
       }
@@ -1089,22 +1043,14 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const
                    d_vars.getUpperBound(vi).approx(SMALL_FIXED_DELTA)))
       {
         newValues.set(vi, d_vars.getUpperBound(vi));
-        // CVC5Message() << "  to ub" << endl;
       }
       else
       {
         double rounded = round(newAssign);
         if (roughlyEqual(newAssign, rounded))
         {
-          // CVC5Message() << "roughly equal " << rounded << " " << newAssign <<
-          // " " << oldAssign << endl;
           newAssign = rounded;
         }
-        else
-        {
-          // CVC5Message() << "not roughly equal " << rounded << " " <<
-          // newAssign << " " << oldAssign << endl;
-        }
 
         DeltaRational proposal;
         if (std::optional maybe_new = estimateWithCFE(newAssign))
@@ -1119,28 +1065,17 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const
 
         if (roughlyEqual(newAssign, oldAssign.approx(SMALL_FIXED_DELTA)))
         {
-          // CVC5Message() << "  to prev value" << newAssign << " " << oldAssign
-          // << endl;
           proposal = d_vars.getAssignment(vi);
         }
 
         if (d_vars.strictlyLessThanLowerBound(vi, proposal))
         {
-          // CVC5Message() << "  round to lb " << d_vars.getLowerBound(vi) <<
-          // endl;
           proposal = d_vars.getLowerBound(vi);
         }
         else if (d_vars.strictlyGreaterThanUpperBound(vi, proposal))
         {
-          // CVC5Message() << "  round to ub " << d_vars.getUpperBound(vi) <<
-          // endl;
           proposal = d_vars.getUpperBound(vi);
         }
-        else
-        {
-          // CVC5Message() << "  use proposal" << proposal << " " << oldAssign
-          // << endl;
-        }
         newValues.set(vi, proposal);
       }
     }
@@ -1202,9 +1137,6 @@ LinResult ApproxGLPK::solveRelaxation(){
   parm.pricing = GLP_PT_PSE;
   parm.it_lim = d_pivotLimit;
   parm.msg_lev = GLP_MSG_OFF;
-  if(s_verbosity >= 1){
-    parm.msg_lev = GLP_MSG_ALL;
-  }
 
   glp_erase_prob(d_realProb);
   glp_copy_prob(d_realProb, d_inputProb, GLP_OFF);
@@ -1735,9 +1667,6 @@ MipResult ApproxGLPK::solveMIP(bool activelyLog){
   parm.cb_func = glpkCallback;
   parm.cb_info = &aux;
   parm.msg_lev = GLP_MSG_OFF;
-  if(s_verbosity >= 1){
-    parm.msg_lev = GLP_MSG_ALL;
-  }
 
   glp_erase_prob(d_mipProb);
   glp_copy_prob(d_mipProb, d_realProb, GLP_OFF);

diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp
index 11a9cc6f28dac494e2b6e637cb35e57ffdd68b58..fbd6b33f6c401ae236cbc3201af2539776ac8d6a 100644 (file)
--- a/src/theory/arith/attempt_solution_simplex.cpp
+++ b/src/theory/arith/attempt_solution_simplex.cpp
@@ -124,12 +124,10 @@ Result::Sat AttemptSolutionSDP::attempt(const ApproximateSimplex::Solution& sol)
     Assert(toAdd != ARITHVAR_SENTINEL);
 
     Trace("arith::forceNewBasis") << toRemove << " " << toAdd << endl;
-    // CVC5Message() << toRemove << " " << toAdd << endl;
 
     d_linEq.pivotAndUpdate(toRemove, toAdd, newValues[toRemove]);
 
     Trace("arith::forceNewBasis") << needsToBeAdded.size() << "to go" << endl;
-    // CVC5Message() << needsToBeAdded.size() << "to go" << endl;
     needsToBeAdded.remove(toAdd);
 
     bool conflict = processSignals();

diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index defcc8aff18af1b2a88ee60c6c265c8c0654aa23..2958b5f48227b834fe55dcec312bb18fda20a119 100644 (file)
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -222,8 +222,6 @@ std::ostream& operator<<(std::ostream& o, const ConstraintCPVec& v){
   return o;
 }
 
-void Constraint::debugPrint() const { CVC5Message() << *this << endl; }
-
 ValueCollection::ValueCollection()
   : d_lowerBound(NullConstraint),
     d_upperBound(NullConstraint),
@@ -699,8 +697,6 @@ bool Constraint::sanityChecking(Node n) const {
   }
 }
 
-void ConstraintRule::debugPrint() const { print(std::cerr, false); }
-
 ConstraintCP ConstraintDatabase::getAntecedent (AntecedentId p) const {
   Assert(p < d_antecedents.size());
   return d_antecedents[p];

diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index 1262181db7965b7989d1f972ab4e35c5d258918f..e335b2e55245ba9b41f012e8fe38ef614ff1c9fc 100644 (file)
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -322,7 +322,6 @@ struct ConstraintRule {
                  RationalVectorCP coeffs);
 
   void print(std::ostream& out, bool produceProofs) const;
-  void debugPrint() const;
 }; /* class ConstraintRule */
 
 class Constraint {
@@ -882,8 +881,6 @@ class Constraint {
     return d_produceProofs ? getConstraintRule().d_farkasCoefficients : nullptr;
   }
 
-  void debugPrint() const;
-
   /**
    * The proof of the node is empty.
    * The proof must be a special proof. Either

diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp
index 08e9edc79b91010d373b069cfd7ea533a84498d3..99dcc93caf170994cc2d752c9b6120402762c662 100644 (file)
--- a/src/theory/arith/dio_solver.cpp
+++ b/src/theory/arith/dio_solver.cpp
@@ -74,7 +74,6 @@ DioSolver::Statistics::Statistics()
 }
 
 bool DioSolver::queueConditions(TrailIndex t){
-  /* debugPrintTrail(t); */
   Debug("queueConditions") << !inConflict() << std::endl;
   Debug("queueConditions") << gcdIsOne(t) << std::endl;
   Debug("queueConditions") << !debugAnySubstitionApplies(t) << std::endl;
@@ -228,8 +227,13 @@ bool DioSolver::anyCoefficientExceedsMaximum(TrailIndex j) const{
     nmonos >= 2 &&
     length > d_maxInputCoefficientLength + MAX_GROWTH_RATE;
   if(Debug.isOn("arith::dio::max") && result){
-    Debug("arith::dio::max") << "about to drop:";
-    debugPrintTrail(j);
+
+    const SumPair& eq = d_trail[j].d_eq;
+    const Polynomial& proof = d_trail[j].d_proof;
+
+    Debug("arith::dio::max") << "about to drop:" << std::endl;
+    Debug("arith::dio::max") << "d_trail[" << j << "].d_eq = " << eq.getNode() << std::endl;
+    Debug("arith::dio::max") << "d_trail[" << j << "].d_proof = " << proof.getNode() << std::endl;
   }
   return result;
 }
@@ -776,14 +780,6 @@ bool DioSolver::gcdIsOne(DioSolver::TrailIndex i){
   return eq.gcd() == Integer(1);
 }
 
-void DioSolver::debugPrintTrail(DioSolver::TrailIndex i) const{
-  const SumPair& eq = d_trail[i].d_eq;
-  const Polynomial& proof = d_trail[i].d_proof;
-
-  CVC5Message() << "d_trail[" << i << "].d_eq = " << eq.getNode() << endl;
-  CVC5Message() << "d_trail[" << i << "].d_proof = " << proof.getNode() << endl;
-}
-
 void DioSolver::subAndReduceCurrentFByIndex(DioSolver::SubIndex subIndex){
   size_t N = d_currentF.size();
 

diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h
index 6be26e85448abaef5497aa776d396ca9afa7ec0c..054fceb469a947af5a36740ac6701c436943fa65 100644 (file)
--- a/src/theory/arith/dio_solver.h
+++ b/src/theory/arith/dio_solver.h
@@ -383,9 +383,6 @@ private:
    */
   SumPair purifyIndex(TrailIndex i);
 
-
-  void debugPrintTrail(TrailIndex i) const;
-
 public:
   bool hasMoreDecompositionLemmas() const{
     return !d_decompositionLemmaQueue.empty();

diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp
index ea7773f768905c13b45b1586a2d05aad747b66e2..147d0a1ffdfa995f7283a2060557acbf54c73dbc 100644 (file)
--- a/src/theory/arith/dual_simplex.cpp
+++ b/src/theory/arith/dual_simplex.cpp
@@ -89,7 +89,6 @@ Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){
 
   Result::Sat result = Result::SAT_UNKNOWN;
 
-  static const bool verbose = false;
   exactResult |= d_varOrderPivotLimit < 0;
 
   uint32_t checkPeriod = options().arith.arithSimplexCheckPeriod;
@@ -105,22 +104,6 @@ Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){
         result = Result::UNSAT;
       }
     }
-
-    if (verbose && numDifferencePivots > 0)
-    {
-      if (result == Result::UNSAT)
-      {
-        CVC5Message() << "diff order found unsat" << endl;
-      }
-      else if (d_errorSet.errorEmpty())
-      {
-        CVC5Message() << "diff order found model" << endl;
-      }
-      else
-      {
-        CVC5Message() << "diff order missed" << endl;
-      }
-    }
   }
   Assert(!d_errorSet.moreSignals());
 
@@ -141,21 +124,6 @@ Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){
       {
         result = Result::UNSAT;
       }
-      if (verbose)
-      {
-        if (result == Result::UNSAT)
-        {
-          CVC5Message() << "restricted var order found unsat" << endl;
-        }
-        else if (d_errorSet.errorEmpty())
-        {
-          CVC5Message() << "restricted var order found model" << endl;
-        }
-        else
-        {
-          CVC5Message() << "restricted var order missed" << endl;
-        }
-      }
     }
   }
 

diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp
index 54d19000b0acf33331c8c545fc32220fd8f26649..5b9f37f93b64657ae9742b9e4e014c53bc1f86c1 100644 (file)
--- a/src/theory/arith/fc_simplex.cpp
+++ b/src/theory/arith/fc_simplex.cpp
@@ -74,15 +74,10 @@ Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){
   d_pivots = 0;
   static thread_local unsigned int instance = 0;
   instance = instance + 1;
-  static const bool verbose = false;
 
   if(d_errorSet.errorEmpty() && !d_errorSet.moreSignals()){
     Debug("arith::findModel") << "fcFindModel("<< instance <<") trivial" << endl;
     Assert(d_conflictVariables.empty());
-    // if (verbose)
-    //{
-    //  CVC5Message() << "fcFindModel(" << instance << ") trivial" << endl;
-    //}
     return Result::SAT;
   }
 
@@ -94,20 +89,11 @@ Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){
 
   if(initialProcessSignals()){
     d_conflictVariables.purge();
-    if (verbose)
-    {
-      CVC5Message() << "fcFindModel(" << instance << ") early conflict" << endl;
-    }
     Debug("arith::findModel") << "fcFindModel("<< instance <<") early conflict" << endl;
     Assert(d_conflictVariables.empty());
     return Result::UNSAT;
   }else if(d_errorSet.errorEmpty()){
-    // if (verbose)
-    //{
-    //  CVC5Message() << "fcFindModel(" << instance << ") fixed itself" << endl;
-    //}
     Debug("arith::findModel") << "fcFindModel("<< instance <<") fixed itself" << endl;
-    if (verbose) Assert(!d_errorSet.moreSignals());
     Assert(d_conflictVariables.empty());
     return Result::SAT;
   }
@@ -132,28 +118,12 @@ Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){
 
     if(result ==  Result::UNSAT){
       ++(d_statistics.d_fcFoundUnsat);
-      if (verbose)
-      {
-        CVC5Message() << "fc found unsat";
-      }
     }else if(d_errorSet.errorEmpty()){
       ++(d_statistics.d_fcFoundSat);
-      if (verbose)
-      {
-        CVC5Message() << "fc found model";
-      }
     }else{
       ++(d_statistics.d_fcMissed);
-      if (verbose)
-      {
-        CVC5Message() << "fc missed";
-      }
     }
   }
-  if (verbose)
-  {
-    CVC5Message() << "(" << instance << ") pivots " << d_pivots << endl;
-  }
 
   Assert(!d_errorSet.moreSignals());
   if(result == Result::SAT_UNKNOWN && d_errorSet.errorEmpty()){
@@ -508,28 +478,9 @@ bool debugUpdatedBasic(const UpdateInfo& selected, ArithVar updated){
 void FCSimplexDecisionProcedure::updateAndSignal(const UpdateInfo& selected, WitnessImprovement w){
   ArithVar nonbasic = selected.nonbasic();
 
-  static bool verbose = false;
-
   Debug("updateAndSignal") << "updateAndSignal " << selected << endl;
 
   stringstream ss;
-  if(verbose){
-    d_errorSet.debugPrint(ss);
-    if(selected.describesPivot()){
-      ArithVar leaving = selected.leaving();
-      ss << "leaving " << leaving
-         << " " << d_tableau.basicRowLength(leaving)
-         << " " << d_linEq.debugBasicAtBoundCount(leaving)
-         << endl;
-    }
-    if(degenerate(w) && selected.describesPivot()){
-      ArithVar leaving = selected.leaving();
-      CVC5Message() << "degenerate " << leaving << ", atBounds "
-                    << d_linEq.basicsAtBounds(selected) << ", len "
-                    << d_tableau.basicRowLength(leaving) << ", bc "
-                    << d_linEq.debugBasicAtBoundCount(leaving) << endl;
-    }
-  }
 
   if(selected.describesPivot()){
     ConstraintP limiting = selected.limiting();
@@ -573,11 +524,6 @@ void FCSimplexDecisionProcedure::updateAndSignal(const UpdateInfo& selected, Wit
     }
   }
 
-  if (verbose)
-  {
-    CVC5Message() << "conflict variable " << selected << endl;
-    CVC5Message() << ss.str();
-  }
   if(Debug.isOn("error")){ d_errorSet.debugPrint(Debug("error")); }
 
   Assert(
@@ -715,7 +661,6 @@ bool FCSimplexDecisionProcedure::debugDualLike(WitnessImprovement w, ostream& ou
 
 Result::Sat FCSimplexDecisionProcedure::dualLike(){
   static int instance = 0;
-  static bool verbose = false;
 
   TimerStat::CodeTimer codeTimer(d_statistics.d_fcTimer);
 
@@ -787,15 +732,14 @@ Result::Sat FCSimplexDecisionProcedure::dualLike(){
         w = selectFocusImproving();
       }
     }
+    Debug("dualLike") << "witnessImprovement: " << w << endl;
     Assert(d_focusSize == d_errorSet.focusSize());
     Assert(d_errorSize == d_errorSet.errorSize());
 
-    if (verbose)
-    {
-      debugDualLike(w, CVC5Message(), instance, prevFocusSize, prevErrorSize);
-    }
     Assert(debugDualLike(
         w, Debug("dualLike"), instance, prevFocusSize, prevErrorSize));
+    Debug("dualLike") << "Focus size " << d_focusSize << " (was " << prevFocusSize << ")" << endl;
+    Debug("dualLike") << "Error size " << d_errorSize << " (was " << prevErrorSize << ")" << endl;
   }
 
 

diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp
index 8e7588847d92e1683db33e4f59246b513b9b26d5..ab6339fd50456db6de431d5094ac04bd2e42c881 100644 (file)
--- a/src/theory/arith/linear_equality.cpp
+++ b/src/theory/arith/linear_equality.cpp
@@ -167,12 +167,10 @@ void LinearEqualityModule::forceNewBasis(const DenseSet& newBasis){
     Assert(toAdd != ARITHVAR_SENTINEL);
 
     Trace("arith::forceNewBasis") << toRemove << " " << toAdd << endl;
-    CVC5Message() << toRemove << " " << toAdd << endl;
     d_tableau.pivot(toRemove, toAdd, d_trackCallback);
     d_basicVariableUpdates(toAdd);
 
     Trace("arith::forceNewBasis") << needsToBeAdded.size() << "to go" << endl;
-    CVC5Message() << needsToBeAdded.size() << "to go" << endl;
     needsToBeAdded.remove(toAdd);
   }
 }

diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp
index d6cdb3a1341fe1017c4cbbbad170dbfbadc8b545..5a834ad424dfdfa2c6bb5a2664a07783d69d3bf9 100644 (file)
--- a/src/theory/arith/soi_simplex.cpp
+++ b/src/theory/arith/soi_simplex.cpp
@@ -80,7 +80,6 @@ Result::Sat SumOfInfeasibilitiesSPD::findModel(bool exactResult){
   d_pivots = 0;
   static thread_local unsigned int instance = 0;
   instance = instance + 1;
-  static const bool verbose = false;
 
   if(d_errorSet.errorEmpty() && !d_errorSet.moreSignals()){
     Debug("soi::findModel") << "soiFindModel("<< instance <<") trivial" << endl;
@@ -96,10 +95,6 @@ Result::Sat SumOfInfeasibilitiesSPD::findModel(bool exactResult){
 
   if(initialProcessSignals()){
     d_conflictVariables.purge();
-    if (verbose)
-    {
-      CVC5Message() << "fcFindModel(" << instance << ") early conflict" << endl;
-    }
     Debug("soi::findModel") << "fcFindModel("<< instance <<") early conflict" << endl;
     Assert(d_conflictVariables.empty());
     return Result::UNSAT;
@@ -130,28 +125,12 @@ Result::Sat SumOfInfeasibilitiesSPD::findModel(bool exactResult){
 
     if(result ==  Result::UNSAT){
       ++(d_statistics.d_soiFoundUnsat);
-      if (verbose)
-      {
-        CVC5Message() << "fc found unsat";
-      }
     }else if(d_errorSet.errorEmpty()){
       ++(d_statistics.d_soiFoundSat);
-      if (verbose)
-      {
-        CVC5Message() << "fc found model";
-      }
     }else{
       ++(d_statistics.d_soiMissed);
-      if (verbose)
-      {
-        CVC5Message() << "fc missed";
-      }
     }
   }
-  if (verbose)
-  {
-    CVC5Message() << "(" << instance << ") pivots " << d_pivots << endl;
-  }
 
   Assert(!d_errorSet.moreSignals());
   if(result == Result::SAT_UNKNOWN && d_errorSet.errorEmpty()){
@@ -345,29 +324,8 @@ void SumOfInfeasibilitiesSPD::debugPrintSignal(ArithVar updated) const{
 void SumOfInfeasibilitiesSPD::updateAndSignal(const UpdateInfo& selected, WitnessImprovement w){
   ArithVar nonbasic = selected.nonbasic();
 
-  static bool verbose = false;
-
   Debug("updateAndSignal") << "updateAndSignal " << selected << endl;
 
-  stringstream ss;
-  if(verbose){
-    d_errorSet.debugPrint(ss);
-    if(selected.describesPivot()){
-      ArithVar leaving = selected.leaving();
-      ss << "leaving " << leaving
-         << " " << d_tableau.basicRowLength(leaving)
-         << " " << d_linEq.debugBasicAtBoundCount(leaving)
-         << endl;
-    }
-    if(degenerate(w) && selected.describesPivot()){
-      ArithVar leaving = selected.leaving();
-      CVC5Message() << "degenerate " << leaving << ", atBounds "
-                    << d_linEq.basicsAtBounds(selected) << ", len "
-                    << d_tableau.basicRowLength(leaving) << ", bc "
-                    << d_linEq.debugBasicAtBoundCount(leaving) << endl;
-    }
-  }
-
   if(selected.describesPivot()){
     ConstraintP limiting = selected.limiting();
     ArithVar basic = limiting->getVariable();
@@ -410,11 +368,6 @@ void SumOfInfeasibilitiesSPD::updateAndSignal(const UpdateInfo& selected, Witnes
     }
   }
 
-  if (verbose)
-  {
-    CVC5Message() << "conflict variable " << selected << endl;
-    CVC5Message() << ss.str();
-  }
   if(Debug.isOn("error")){ d_errorSet.debugPrint(Debug("error")); }
 
   //Assert(debugSelectedErrorDropped(selected, d_errorSize, d_errorSet.errorSize()));
@@ -944,8 +897,7 @@ bool SumOfInfeasibilitiesSPD::debugSOI(WitnessImprovement w, ostream& out, int i
 
 Result::Sat SumOfInfeasibilitiesSPD::sumOfInfeasibilities(){
   static int instance = 0;
-  static bool verbose = false;
-
+  
   TimerStat::CodeTimer codeTimer(d_statistics.d_soiTimer);
 
   Assert(d_sgnDisagreements.empty());
@@ -968,15 +920,11 @@ Result::Sat SumOfInfeasibilitiesSPD::sumOfInfeasibilities(){
     // - conflict
     // - budget was exhausted
     // - focus went down
-    Debug("dualLike") << "selectFocusImproving " << endl;
     WitnessImprovement w = soiRound();
+    Debug("dualLike") << "selectFocusImproving -> " << w << endl;
 
     Assert(d_errorSize == d_errorSet.errorSize());
 
-    if (verbose)
-    {
-      debugSOI(w, CVC5Message(), instance);
-    }
     Assert(debugSOI(w, Debug("dualLike"), instance));
   }