From 762c8a3cf028fa7c12c2ee32d8643bd73ff2f07c Mon Sep 17 00:00:00 2001
From: Andres Notzli <andres.noetzli@gmail.com>
Date: Thu, 8 Dec 2016 14:21:28 -0800
Subject: [PATCH] Fix (inactive) `MultSlice` rewrite

The `MultSlice` rewrite was previously accepting multiplications of
three and more variables even though it was designed for multiplications
of two variables only. Fortunately, the rewrite was not actively used in
the bitvector solver. This commit strengthens the condition in
`applies()` and adds a unit test that checks that x * y * z and x * y do
not get rewritten to the same term.
---
 .../theory_bv_rewrite_rules_simplification.h   |  7 ++-----
 test/unit/theory/theory_engine_white.h         | 18 +++++++++++++++++-
 2 files changed, 19 insertions(+), 6 deletions(-)

diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index 6ef591760..871380467 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -1108,13 +1108,10 @@ Node RewriteRule<MergeSignExtend>::apply(TNode node) {
 
 template<> inline
 bool RewriteRule<MultSlice>::applies(TNode node) {
-  if (node.getKind() != kind::BITVECTOR_MULT) {
+  if (node.getKind() != kind::BITVECTOR_MULT || node.getNumChildren() != 2) {
     return false; 
   }
-  if (utils::getSize(node[0]) % 2 != 0) {
-    return false; 
-  }
-  return true; 
+  return utils::getSize(node[0]) % 2 == 0;
 }
 
 /** 
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index 978440576..9775dca1b 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -33,6 +33,7 @@
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "theory/bv/theory_bv_rewrite_rules_normalization.h"
+#include "theory/bv/theory_bv_rewrite_rules_simplification.h"
 #include "theory/rewriter.h"
 #include "theory/theory.h"
 #include "theory/theory_engine.h"
@@ -442,6 +443,21 @@ public:
     Node expected =
         d_nm->mkNode(BITVECTOR_SUB, d_nm->mkNode(BITVECTOR_MULT, x, z),
                      d_nm->mkNode(BITVECTOR_MULT, y, z));
-    TS_ASSERT(result == expected);
+    TS_ASSERT_EQUALS(result, expected);
+
+    // Try to apply MultSlice to a multiplication of two and three different
+    // variables, expect different results (x * y and x * y * z should not get
+    // rewritten to the same term).
+    expr = d_nm->mkNode(BITVECTOR_MULT, x, y, z);
+    result = expr;
+    Node expr2 = d_nm->mkNode(BITVECTOR_MULT, x, y);
+    Node result2 = expr;
+    if (RewriteRule<MultSlice>::applies(expr)) {
+      result = RewriteRule<MultSlice>::apply(expr);
+    }
+    if (RewriteRule<MultSlice>::applies(expr2)) {
+      result2 = RewriteRule<MultSlice>::apply(expr2);
+    }
+    TS_ASSERT_DIFFERS(result, result2);
   }
 };
-- 
2.30.2