From: Tim King <taking@cs.nyu.edu>
Date: Sun, 14 Jun 2015 21:37:59 +0000 (+0200)
Subject: Handing the case in replay where a cut is directly in conflict with an existing bound.
X-Git-Tag: cvc5-1.0.0~6274
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7ac9d35366c0d5ed5aee5d26862f39a2c98bd521;p=cvc5.git

Handing the case in replay where a cut is directly in conflict with an existing bound.
---

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;