From c2bee2773194c51a67270535b475870d31b756c7 Mon Sep 17 00:00:00 2001
From: Clark Barrett <barrett@cs.nyu.edu>
Date: Sun, 10 Jun 2012 15:55:31 +0000
Subject: [PATCH] Fixed one more bug in rewriter

---
 src/theory/bv/theory_bv_rewrite_rules_normalization.h | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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));
     }
-- 
2.30.2