Merge branch 'master' into fix_order

3 files changed, 22 insertions, 10 deletions

diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp
index d7c580395..ec396b24e 100644
--- a/src/theory/arith/normal_form.cpp
+++ b/src/theory/arith/normal_form.cpp
@@ -528,14 +528,13 @@ Integer Polynomial::numeratorGCD() const {
 
 Integer Polynomial::denominatorLCM() const {
   Integer tmp(1);
-  for(iterator i=begin(), e=end(); i!=e; ++i){
-    const Constant& c = (*i).getConstant();
-    tmp = tmp.lcm(c.getValue().getDenominator());
+  for (iterator i = begin(), e = end(); i != e; ++i) {
+    const Integer denominator = (*i).getConstant().getValue().getDenominator();
+    tmp = tmp.lcm(denominator);
   }
   return tmp;
 }
 
-
 Constant Polynomial::getCoefficient(const VarList& vl) const{
   //TODO improve to binary search...
   for(iterator iter=begin(), myend=end(); iter != myend; ++iter){
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);
   }
 };