From: Liana Hadarean <lianahady@gmail.com>
Date: Thu, 20 Aug 2015 16:21:08 +0000 (+0100)
Subject: fix for bug660 and bug658 due to incorrect bit-blasting of divison by zero
X-Git-Tag: cvc5-1.0.0~6252^2~14
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=92584a9a74b941bfd1cbcfbcec21a57bda4c4952;p=cvc5.git

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 62c92c0a8..0990c2f29 100644
--- 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