diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index a4825c1c4..328a07a24 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -2639,13 +2639,16 @@ std::vector<ConstraintCPVec> TheoryArithPrivate::replayLogRec(ApproximateSimplex const ConstraintCPVec& exp = ci->getExplanation(); // success - Assert(!con->negationHasProof()); if(con->isTrue()){ Debug("approx::replayLogRec") << "not asserted?" << endl; - }else{ + }else if(!con->negationHasProof()){ con->impliedByIntHole(exp, false); replayAssert(con); Debug("approx::replayLogRec") << "cut prop" << endl; + }else { + con->impliedByIntHole(exp, true); + Debug("approx::replayLogRec") << "cut into conflict " << con << endl; + raiseConflict(con); } }else{ ++d_statistics.d_cutsProofFailed; |