Fix to the previous commit.

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index dfd82b960ba9da2b679c633fe9612ab921db7327..a99d86a9c386da122a4e1bb767bf37c9c738f670 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -937,8 +937,10 @@ void TheoryArith::propagate(Effort e) {
             propagated = true;
           }else{
             Node exp = d_differenceManager.explain(toProp);
-            Node lp = flattenAnd(exp.andNode(exp));
-            d_out->conflict(exp);
+            Node lp = flattenAnd(exp.andNode(notNormalized));
+            Debug("arith::propagate") << "propagate conflict" << lp << endl;
+            d_out->conflict(lp);
+
             propagated = true;
             break;
           }