diff options
author | lianah <lianahady@gmail.com> | 2014-06-10 13:48:45 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2014-06-10 13:48:45 -0400 |
commit | 5f072a19d299191dbedc4b69c8e0eda694cfa957 (patch) | |
tree | 0ebfc27bd05d06b0cdb2fc0813b7d5649d36aee4 /src/util/bitvector.h | |
parent | db51926b5ce806754fc26c81b1b7d3e739fc4fc5 (diff) |
Merging CAV14 paper bit-vector work.
Diffstat (limited to 'src/util/bitvector.h')
-rw-r--r-- | src/util/bitvector.h | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/util/bitvector.h b/src/util/bitvector.h index e826a6704..35b052531 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -197,7 +197,8 @@ public: CheckArgument(d_size == y.d_size, y); if (y.d_value == 0) { - return BitVector(d_size, 0u); + // under division by zero return -1 + return BitVector(d_size, Integer(1).oneExtend(1, d_size - 1)); } CheckArgument(d_value >= 0, this); CheckArgument(y.d_value > 0, y); @@ -210,7 +211,7 @@ public: BitVector unsignedRemTotal(const BitVector& y) const { CheckArgument(d_size == y.d_size, y); if (y.d_value == 0) { - return BitVector(d_size, 0u); + return BitVector(d_size, d_value); } CheckArgument(d_value >= 0, this); CheckArgument(y.d_value > 0, y); |