diff options
author | Liana Hadarean <lianahady@gmail.com> | 2012-11-13 04:49:34 +0000 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2012-11-13 04:49:34 +0000 |
commit | 2cf12a56cb9c5eb539d50a39b2764a292d6fd13f (patch) | |
tree | 3578ca6339a97e4b85c83d1a9f2219aea569aca7 /src/theory/bv/bitblast_strategies.cpp | |
parent | 89081ba6a8a62a117cbfef99aa7c8e4bf0bf1b39 (diff) |
added support for division by zero for bit-vector division operators
Diffstat (limited to 'src/theory/bv/bitblast_strategies.cpp')
-rw-r--r-- | src/theory/bv/bitblast_strategies.cpp | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp index d2fbb432b..fbf9a45ee 100644 --- a/src/theory/bv/bitblast_strategies.cpp +++ b/src/theory/bv/bitblast_strategies.cpp @@ -640,7 +640,7 @@ void uDivModRec(const Bits& a, const Bits& b, Bits& q, Bits& r, unsigned rec_wid void DefaultUdivBB (TNode node, Bits& q, Bitblaster* bb) { BVDebug("bitvector-bb") << "theory::bv::DefaultUdivBB bitblasting " << node << "\n"; - Assert(node.getKind() == kind::BITVECTOR_UDIV && q.size() == 0); + Assert(node.getKind() == kind::BITVECTOR_UDIV_TOTAL && q.size() == 0); Bits a, b; bb->bbTerm(node[0], a); @@ -650,13 +650,13 @@ void DefaultUdivBB (TNode node, Bits& q, Bitblaster* bb) { uDivModRec(a, b, q, r, getSize(node)); // cache the remainder in case we need it later - Node remainder = mkNode(kind::BITVECTOR_UREM, node[0], node[1]); + Node remainder = mkNode(kind::BITVECTOR_UREM_TOTAL, node[0], node[1]); bb->cacheTermDef(remainder, r); } void DefaultUremBB (TNode node, Bits& rem, Bitblaster* bb) { BVDebug("bitvector-bb") << "theory::bv::DefaultUremBB bitblasting " << node << "\n"; - Assert(node.getKind() == kind::BITVECTOR_UREM && rem.size() == 0); + Assert(node.getKind() == kind::BITVECTOR_UREM_TOTAL && rem.size() == 0); Bits a, b; bb->bbTerm(node[0], a); @@ -666,7 +666,7 @@ void DefaultUremBB (TNode node, Bits& rem, Bitblaster* bb) { uDivModRec(a, b, q, rem, getSize(node)); // cache the quotient in case we need it later - Node quotient = mkNode(kind::BITVECTOR_UDIV, node[0], node[1]); + Node quotient = mkNode(kind::BITVECTOR_UDIV_TOTAL, node[0], node[1]); bb->cacheTermDef(quotient, q); } |