changed BitVector::unsignedRem to match the behavior of the bit-blasted circuit for...

diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index bb0099157186c5a33705656ebc3dfd4c88a2c031..2c178ec2e2dab71cd4bdf752138f7d8fee1edcbc 100644 (file)
--- 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);