More regression tests

Author: BrunoDutertre

tests/regress/bv/issue190.smt2

@@ -0,0 +1,7 @@
+(set-logic QF_BV)
+(declare-const a (_ BitVec 6))
+(assert (= ((_ rotate_left 10) a) ((_ rotate_right 10) a)))
+(assert (distinct a #b000000))
+(assert (distinct a #b111111))
+(check-sat)
+(exit)

tests/regress/bv/issue190.smt2.gold

@@ -0,0 +1 @@
+sat

tests/regress/bv/issue190b.smt2

@@ -0,0 +1,7 @@
+(set-logic QF_BV)
+(declare-const a (_ BitVec 5))
+(assert (= ((_ rotate_left 9) a) ((_ rotate_right 9) a)))
+(assert (distinct a #b00000))
+(assert (distinct a #b11111))
+(check-sat)
+(exit)

tests/regress/bv/issue190b.smt2.gold

@@ -0,0 +1 @@
+unsat