diff options
author | Liana Hadarean <lianahady@gmail.com> | 2015-08-20 17:21:08 +0100 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2015-08-20 18:22:46 +0100 |
commit | 92584a9a74b941bfd1cbcfbcec21a57bda4c4952 (patch) | |
tree | eaedb44488bbf683bd9c7faad35c08402802169c /src/theory/bv/bitblast_strategies_template.h | |
parent | e909e34249754bc5f021449512c9cc304802933f (diff) |
fix for bug660 and bug658 due to incorrect bit-blasting of divison by zero
Diffstat (limited to 'src/theory/bv/bitblast_strategies_template.h')
-rw-r--r-- | src/theory/bv/bitblast_strategies_template.h | 8 |
1 files changed, 4 insertions, 4 deletions
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 |