fix for bug660 and bug658 due to incorrect bit-blasting of divison by zero

diff --git a/src/theory/bv/bitblast_strategies_template.h b/src/theory/bv/bitblast_strategies_template.h
index 62c92c0a81818d42616129cf3757cff0e79ef7ae..0990c2f291684803bfe59a23222daf220a4dfa73 100644 (file)
--- a/src/theory/bv/bitblast_strategies_template.h
+++ b/src/theory/bv/bitblast_strategies_template.h
@@ -536,8 +536,8 @@ void DefaultUdivBB (TNode node, std::vector<T>& q, TBitblaster<T>* bb) {
   T b_is_0 = mkAnd(iszero); 
   
   for (unsigned i = 0; i < q.size(); ++i) {
-    q[i] = mkIte(b_is_0, mkTrue<T>(), q[i]);
-    r[i] = mkIte(b_is_0, mkTrue<T>(), r[i]);
+    q[i] = mkIte(b_is_0, mkTrue<T>(), q[i]); // a udiv 0 is 11..11
+    r[i] = mkIte(b_is_0, a[i], r[i]);        // a urem 0 is a
   }
 
   // cache the remainder in case we need it later
@@ -564,8 +564,8 @@ void DefaultUremBB (TNode node, std::vector<T>& rem, TBitblaster<T>* bb) {
   T b_is_0 = mkAnd(iszero); 
   
   for (unsigned i = 0; i < q.size(); ++i) {
-    q[i] = mkIte(b_is_0, a[i], q[i]);
-    rem[i] = mkIte(b_is_0, a[i], rem[i]);
+    q[i] = mkIte(b_is_0, mkTrue<T>(), q[i]); // a udiv 0 is 11..11
+    rem[i] = mkIte(b_is_0, a[i], rem[i]);    // a urem 0 is a
   }
 
   // cache the quotient in case we need it later