From 92584a9a74b941bfd1cbcfbcec21a57bda4c4952 Mon Sep 17 00:00:00 2001 From: Liana Hadarean Date: Thu, 20 Aug 2015 17:21:08 +0100 Subject: [PATCH] fix for bug660 and bug658 due to incorrect bit-blasting of divison by zero --- src/theory/bv/bitblast_strategies_template.h | 8 ++++---- 1 file 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& q, TBitblaster* bb) { T b_is_0 = mkAnd(iszero); for (unsigned i = 0; i < q.size(); ++i) { - q[i] = mkIte(b_is_0, mkTrue(), q[i]); - r[i] = mkIte(b_is_0, mkTrue(), r[i]); + q[i] = mkIte(b_is_0, mkTrue(), 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& rem, TBitblaster* 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(), 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 -- 2.30.2