changed BitVector::unsignedRem to match the behavior of the bit-blasted circuit for division by 0; temporary fix for bug440

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);