diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-10 15:55:31 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-10 15:55:31 +0000 |
commit | c2bee2773194c51a67270535b475870d31b756c7 (patch) | |
tree | 0952b6df07e37e543936358476a57aaab94eef1c | |
parent | 48f837c9d53e2e93b14786943f9961228e0d9933 (diff) |
Fixed one more bug in rewriter
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_normalization.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index 4fa96c231..f5577e2ed 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -429,8 +429,8 @@ Node RewriteRule<SolveEq>::apply(TNode node) { // If both constants are nonzero, combine on right, otherwise leave them where they are if (rightConst != zero) { - leftConst = zero; rightConst = rightConst - leftConst; + leftConst = zero; if (rightConst != zero) { childrenRight.push_back(utils::mkConst(rightConst)); } |