From f2d98d87361fc1a44e64677586f5c8d4625a4756 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Thu, 15 Dec 2011 21:02:33 +0000
Subject: [PATCH] Fix to the previous commit.

---
 src/theory/arith/theory_arith.cpp | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

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;
           }
-- 
2.30.2