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

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;