diff options
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 6 |
1 files 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; } |