diff options
Diffstat (limited to 'src/theory')
| -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)); } |