merged master into branch

diff --cc src/theory/bv/bitblast_strategies.cpp
Simple merge

diff --cc src/util/bitvector.h
index 5df632ff495244b6c2e94817747d2596dce6689b,4cbcba50eb73d71265f28240e84ad1124fd67281..c9661c0c72069e5ad892ce9d656f2901e4b6ba6f
--- 1/src/util/bitvector.h
--- 2/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@@ -178,34 -178,25 +178,39 @@@ public
      Integer prod = d_value * y.d_value;
      return BitVector(d_size, prod);
    }
-   BitVector unsignedDiv (const BitVector& y) const {
 +
 +  BitVector setBit(uint32_t i) const {
 +    CheckArgument(i < d_size, i);
 +    Integer res = d_value.setBit(i);
 +    return BitVector(d_size, res); 
 +  }
 +
 +  bool isBitSet(uint32_t i) const {
 +    CheckArgument(i < d_size, i); 
 +    return d_value.isBitSet(i); 
 +  }
 +  
+   /** 
+    * Total division function that returns 0 when the denominator is 0.  
+    */
+   BitVector unsignedDivTotal (const BitVector& y) const {
++
      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, 0u);
      }
      CheckArgument(d_value >= 0, this);
      CheckArgument(y.d_value > 0, y);
      return BitVector(d_size, d_value.floorDivideQuotient(y.d_value)); 
    }
- 
-   BitVector unsignedRem(const BitVector& y) const {
++  
+   /** 
+    * Total division function that returns 0 when the denominator is 0.  
+    */
+   BitVector unsignedRemTotal(const BitVector& y) const {
      CheckArgument(d_size == y.d_size, y);
-     // TODO: decide whether we really want these semantics
      if (y.d_value == 0) {
-       return BitVector(d_size, d_value);
+       return BitVector(d_size, 0u);
      }
      CheckArgument(d_value >= 0, this);
      CheckArgument(y.d_value > 0, y);

diff --cc src/util/integer_cln_imp.h
Simple merge

diff --cc src/util/integer_gmp_imp.h
Simple merge