From 15a15f5c9fa65df13dfb2fe6b3bf3fc3604ddacc Mon Sep 17 00:00:00 2001 From: Tim King Date: Wed, 25 Jun 2014 10:46:40 -0400 Subject: Fixing the previous bugfix. --- src/theory/arith/theory_arith_private.cpp | 17 +++++++---------- 1 file changed, 7 insertions(+), 10 deletions(-) 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 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())){ -- cgit v1.2.3