diff options
author | Tim King <taking@cs.nyu.edu> | 2011-12-15 21:02:33 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2011-12-15 21:02:33 +0000 |
commit | f2d98d87361fc1a44e64677586f5c8d4625a4756 (patch) | |
tree | d65e9e073ac13d92107e6b7da4a4ed8996aa4487 | |
parent | 9bcda83d2d322a97b5896ce160c298f6a159a2d2 (diff) |
Fix to the previous commit.
-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; } |