From: Tim King <taking@cs.nyu.edu>
Date: Thu, 15 Dec 2011 21:02:33 +0000 (+0000)
Subject: Fix to the previous commit.
X-Git-Tag: cvc5-1.0.0~8354
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f2d98d87361fc1a44e64677586f5c8d4625a4756;p=cvc5.git

Fix to the previous commit.
---

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index dfd82b960..a99d86a9c 100644
--- 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;
           }