2 files changed, 24 insertions, 2 deletions
diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp
index fbf9a45ee..c25c40c22 100644
--- a/src/theory/bv/bitblast_strategies.cpp
+++ b/src/theory/bv/bitblast_strategies.cpp
@@ -648,6 +648,17 @@ void DefaultUdivBB (TNode node, Bits& q, Bitblaster* bb) {
 
   Bits r;
   uDivModRec(a, b, q, r, getSize(node)); 
+  // adding a special case for division by 0
+  std::vector<Node> iszero; 
+  for (unsigned i = 0; i < b.size(); ++i) {
+    iszero.push_back(utils::mkNode(kind::IFF, b[i], utils::mkFalse())); 
+  }
+  Node b_is_0 = utils::mkAnd(iszero); 
+  
+  for (unsigned i = 0; i < q.size(); ++i) {
+    q[i] = utils::mkNode(kind::ITE, b_is_0, utils::mkFalse(), q[i]);
+    r[i] = utils::mkNode(kind::ITE, b_is_0, utils::mkFalse(), r[i]);
+  }
 
   // cache the remainder in case we need it later
   Node remainder = mkNode(kind::BITVECTOR_UREM_TOTAL, node[0], node[1]);
@@ -664,6 +675,17 @@ void DefaultUremBB (TNode node, Bits& rem, Bitblaster* bb) {
 
   Bits q;
   uDivModRec(a, b, q, rem, getSize(node)); 
+  // adding a special case for division by 0
+  std::vector<Node> iszero; 
+  for (unsigned i = 0; i < b.size(); ++i) {
+    iszero.push_back(utils::mkNode(kind::IFF, b[i], utils::mkFalse())); 
+  }
+  Node b_is_0 = utils::mkAnd(iszero); 
+  
+  for (unsigned i = 0; i < q.size(); ++i) {
+    q[i] = utils::mkNode(kind::ITE, b_is_0, utils::mkFalse(), q[i]);
+    rem[i] = utils::mkNode(kind::ITE, b_is_0, utils::mkFalse(), rem[i]);
+  }
 
   // cache the quotient in case we need it later
   Node quotient = mkNode(kind::BITVECTOR_UDIV_TOTAL, node[0], node[1]);
diff --git a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
index 8b080d104..498378638 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
@@ -207,7 +207,7 @@ Node RewriteRule<EvalUdiv>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalUdiv>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector b = node[1].getConst<BitVector>();
-  BitVector res = a.unsignedDiv(b);
+  BitVector res = a.unsignedDivTotal(b);
   
   return utils::mkConst(res);
 }
@@ -222,7 +222,7 @@ Node RewriteRule<EvalUrem>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalUrem>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector b = node[1].getConst<BitVector>();
-  BitVector res = a.unsignedRem(b);
+  BitVector res = a.unsignedRemTotal(b);
   return utils::mkConst(res);
 }