merge from arrays-clark branch

1 files changed, 8 insertions, 0 deletions

diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index 512f23136..5d0c301d4 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -188,12 +188,20 @@ public:
   
   BitVector unsignedDiv (const BitVector& y) const {
     Assert (d_size == y.d_size);
+    // TODO: decide whether we really want these semantics
+    if (y.d_value == 0) {
+      return BitVector(d_size, Integer(0));
+    }
     Assert (d_value >= 0 && y.d_value > 0); 
     return BitVector(d_size, d_value.floorDivideQuotient(y.d_value)); 
   }
 
   BitVector unsignedRem(const BitVector& y) const {
     Assert (d_size == y.d_size);
+    // TODO: decide whether we really want these semantics
+    if (y.d_value == 0) {
+      return BitVector(d_size, Integer(0));
+    }
     Assert (d_value >= 0 && y.d_value > 0); 
     return BitVector(d_size, d_value.floorDivideRemainder(y.d_value)); 
   }