Add unit tests for BitVector, minor BV rewrite fix (#1622)

This commit adds unit tests for the BitVector class and adds some additional argument checks. Additionally, it fixes a minor issue in the ZeroExtendUltConst rule if the zero_extend was by 0 bits. In that case, the rule was calling BitVector::extract() with high < low.

1 files changed, 6 insertions, 3 deletions

diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index d91067d1e..a4be19253 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -1303,10 +1303,13 @@ inline bool RewriteRule<ZeroExtendUltConst>::applies(TNode node) {
       t = node[1][0];
       c = node[0];
     }
-    BitVector bv_c = c.getConst<BitVector>();
-    BitVector bv_max =
-        BitVector(utils::getSize(c)).setBit(utils::getSize(t) - 1);
 
+    if (utils::getSize(t) == utils::getSize(c))
+    {
+      return false;
+    }
+
+    BitVector bv_c = c.getConst<BitVector>();
     BitVector c_hi = c.getConst<BitVector>().extract(utils::getSize(c) - 1,
                                                      utils::getSize(t));
     BitVector zero = BitVector(c_hi.getSize(), Integer(0));