diff options
author | Tim King <taking@cs.nyu.edu> | 2015-06-14 23:37:59 +0200 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2015-06-14 23:37:59 +0200 |
commit | 7ac9d35366c0d5ed5aee5d26862f39a2c98bd521 (patch) | |
tree | 1a250350a3e98d83101b8e1da5a1c36a42a4c6b0 /src/theory | |
parent | 232782d690e1dc333ebc7bec1a9302f086c947b6 (diff) |
Handing the case in replay where a cut is directly in conflict with an existing bound.
Diffstat (limited to 'src/theory')
-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; |