diff options
author | Liana Hadarean <lianahady@gmail.com> | 2012-11-12 19:38:47 +0000 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2012-11-12 19:38:47 +0000 |
commit | 069feb82d76d10bbeebcf93a00d85b7caedb2d36 (patch) | |
tree | 7a3200d9b3960795acecabda77acad66e387d07e /src | |
parent | ff1666905d56bf9dff0a22162688ac155200091c (diff) |
changed BitVector::unsignedRem to match the behavior of the bit-blasted circuit for division by 0; temporary fix for bug440
Diffstat (limited to 'src')
-rw-r--r-- | src/util/bitvector.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/util/bitvector.h b/src/util/bitvector.h index bb0099157..2c178ec2e 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -194,7 +194,7 @@ public: CheckArgument(d_size == y.d_size, y); // TODO: decide whether we really want these semantics if (y.d_value == 0) { - return BitVector(d_size, Integer(0)); + return BitVector(d_size, d_value); } CheckArgument(d_value >= 0, this); CheckArgument(y.d_value > 0, y); |