From 7ac9d35366c0d5ed5aee5d26862f39a2c98bd521 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Sun, 14 Jun 2015 23:37:59 +0200
Subject: [PATCH] Handing the case in replay where a cut is directly in
 conflict with an existing bound.

---
 src/theory/arith/theory_arith_private.cpp | 7 +++++--
 1 file 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;
-- 
2.30.2