From: Tim King <taking@cs.nyu.edu>
Date: Wed, 25 Jun 2014 14:46:40 +0000 (-0400)
Subject: Fixing the previous bugfix.
X-Git-Tag: cvc5-1.0.0~6700^2~3
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=15a15f5c9fa65df13dfb2fe6b3bf3fc3604ddacc;p=cvc5.git

Fixing the previous bugfix.
---

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index f6ac951bc..30fc25306 100644
--- 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())){