2 files changed, 6 insertions, 7 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 99507245d..94fc1e34c 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -622,7 +622,7 @@ int TheoryBV::getReduction(int effort, Node n, Node& nr)
   }
   else if (n.getKind() == kind::INT_TO_BITVECTOR)
   {
-    nr = utils::eliminateBv2Nat(n);
+    nr = utils::eliminateInt2Bv(n);
     return -1;
   }
   return 0;
diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index 153f785ca..a7638325c 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -1382,12 +1382,11 @@ bool RewriteRule<BitwiseSlicing>::applies(TNode node) {
     if (node[i].getKind() == kind::CONST_BITVECTOR) {
       BitVector constant = node[i].getConst<BitVector>();
       // we do not apply the rule if the constant is all 0s or all 1s
-      if (constant == BitVector(utils::getSize(node), 0u)) 
-        return false; 
-      
-      for (unsigned i = 0; i < constant.getSize(); ++i) {
-        if (!constant.isBitSet(i)) 
-          return true; 
+      if (constant == BitVector(utils::getSize(node), 0u)) return false;
+
+      for (unsigned j = 0, csize = constant.getSize(); j < csize; ++j)
+      {
+        if (!constant.isBitSet(j)) return true;
       }
       return false; 
     }