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 /src | |
| parent | 9bcda83d2d322a97b5896ce160c298f6a159a2d2 (diff) | |
Fix to the previous commit.
Diffstat (limited to 'src')
| -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; } |