Merge branch 'master' into fix_order

2 files changed, 5 insertions, 9 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;
 }
 
 /**