Fixing the previous bugfix.

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index f6ac951bc2e0498755081b33b441f8520013a754..30fc25306184557eef6ae41b2ae005e5034e8a00 100644 (file)
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -2146,6 +2146,9 @@ bool TheoryArithPrivate::replayLog(ApproximateSimplex* approx){
     d_currentPropagationList.resize(enteringPropN);
   }
 
+  /* It is not clear what the d_qflraStatus is at this point */
+  d_qflraStatus = Result::SAT_UNKNOWN;
+
   Assert(d_replayVariables.empty());
   Assert(d_replayConstraints.empty());
 
@@ -2288,6 +2291,7 @@ void TheoryArithPrivate::tryBranchCut(ApproximateSimplex* approx, int nid, Branc
 
       SimplexDecisionProcedure& simplex = selectSimplex(true);
       simplex.findModel(false);
+      // Can change d_qflraStatus
 
       d_linEq.stopTrackingBoundCounts();
       d_partialModel.startQueueingBoundCounts();
@@ -2563,6 +2567,7 @@ std::vector<ConstraintCPVec> TheoryArithPrivate::replayLogRec(ApproximateSimplex
 
         SimplexDecisionProcedure& simplex = selectSimplex(true);
         simplex.findModel(false);
+       // can change d_qflraStatus
 
         d_linEq.stopTrackingBoundCounts();
         d_partialModel.startQueueingBoundCounts();
@@ -2964,18 +2969,10 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){
         if(mipRes == MipClosed){
           d_likelyIntegerInfeasible = true;
           replayLog(approx);
+         AlwaysAssert(anyConflict() || d_qflraStatus != Result::SAT);
 
          if(!anyConflict()){
-           //start up simplex
-           d_partialModel.stopQueueingBoundCounts();
-           UpdateTrackingCallback utcb(&d_linEq);
-           d_partialModel.processBoundsQueue(utcb);
-           d_linEq.startTrackingBoundCounts();
-           //call simplex
-           solveRelaxationOrPanic(effortLevel);
-           // shutdown simplex
-           d_linEq.stopTrackingBoundCounts();
-           d_partialModel.startQueueingBoundCounts();
+           solveRealRelaxation(effortLevel);
          }
         }
         if(!(anyConflict() || !d_approxCuts.empty())){