Merging bv parts of ajr/bvExt branch, minor additions to ExtTheory.

3 files changed, 40 insertions, 0 deletions

diff --git a/test/regress/regress0/bv/bv2nat-ground-c.smt2 b/test/regress/regress0/bv/bv2nat-ground-c.smt2
new file mode 100644
index 000000000..2bb09c2cf
--- /dev/null
+++ b/test/regress/regress0/bv/bv2nat-ground-c.smt2
@@ -0,0 +1,15 @@
+(set-logic QF_BVLIA)
+(set-info :status unsat)
+(declare-const a (_ BitVec 32))
+(declare-const b (_ BitVec 32))
+(declare-const c (_ BitVec 32))
+(declare-const d (_ BitVec 32))
+(declare-const e (_ BitVec 32))
+
+(assert (or (= a #x00000007) (= a #x00000005) (= a #x00000100)))
+
+(assert (not (= (bv2nat a) 7)))
+(assert (not (= (bv2nat a) 5)))
+(assert (< (bv2nat a) 10))
+
+(check-sat)
diff --git a/test/regress/regress0/bv/bv2nat-ground.smt2 b/test/regress/regress0/bv/bv2nat-ground.smt2
new file mode 100644
index 000000000..f72228b28
--- /dev/null
+++ b/test/regress/regress0/bv/bv2nat-ground.smt2
@@ -0,0 +1,16 @@
+(set-logic QF_BVLIA)
+(set-info :status unsat)
+(declare-const a (_ BitVec 32))
+(declare-const b (_ BitVec 32))
+(declare-const c (_ BitVec 32))
+(declare-const d (_ BitVec 32))
+(declare-const e (_ BitVec 32))
+
+(assert (or (= a b) (= a c) (= a d) (= a e)))
+
+(assert (not (= (bv2nat a) (bv2nat b))))
+(assert (not (= (bv2nat a) (bv2nat c))))
+(assert (not (= (bv2nat a) (bv2nat d))))
+(assert (not (= (bv2nat a) (bv2nat e))))
+
+(check-sat)
diff --git a/test/regress/regress0/bv/cmu-rdk-3.smt2 b/test/regress/regress0/bv/cmu-rdk-3.smt2
new file mode 100644
index 000000000..742dd593b
--- /dev/null
+++ b/test/regress/regress0/bv/cmu-rdk-3.smt2
@@ -0,0 +1,9 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+
+(declare-fun y () Int)
+(declare-fun x () Int)
+
+(assert (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (not (not (= (ite (= (bv2nat (bvand ((_ int2bv 3) (bv2nat (bvor ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1)))) ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1))))))) ((_ int2bv 3) 1))) 0) 1 0) 0)))) (not (= (ite (>= x 0) 1 0) 0))) (not (= (ite (>= y 0) 1 0) 0))) (not (= (ite (= x y) 1 0) 0))) (not (not (= (ite (= x 0) 1 0) 0)))) (not (not (= (ite (= y 0) 1 0) 0)))) (not (= (ite (= (bv2nat (bvand ((_ int2bv 3) (bv2nat (bvor ((_ int2bv 3) x) ((_ int2bv 3) x)))) ((_ int2bv 3) 1))) 0) 1 0) 0))) (and (= x (bv2nat ((_ int2bv 3) x))) (= 1 (bv2nat ((_ int2bv 3) 1))))) (= ((_ extract 0 0) (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1))) (_ bv0 1))) (and (= y (bv2nat ((_ int2bv 3) y))) (= 1 (bv2nat ((_ int2bv 3) 1))))) (= ((_ extract 0 0) (bvashr ((_ int2bv 3) y) ((_ int2bv 3) 1))) (_ bv0 1))) (and (= (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1))) (bv2nat ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1)))))) (= (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1))) (bv2nat ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1)))))))) (= ((_ extract 0 0) (bvor ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1)))) ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1)))))) (_ bv0 1))) (and (= (bv2nat (bvor ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1)))) ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1)))))) (bv2nat ((_ int2bv 3) (bv2nat (bvor ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1)))) ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1))))))))) (= 1 (bv2nat ((_ int2bv 3) 1))))) (= ((_ extract 0 0) (bvand ((_ int2bv 3) (bv2nat (bvor ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1)))) ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1))))))) ((_ int2bv 3) 1))) (_ bv0 1))) (and (= x (bv2nat ((_ int2bv 3) x))) (= x (bv2nat ((_ int2bv 3) x))))) (= ((_ extract 0 0) (bvor ((_ int2bv 3) x) ((_ int2bv 3) x))) (_ bv0 1))) (and (= (bv2nat (bvor ((_ int2bv 3) x) ((_ int2bv 3) x))) (bv2nat ((_ int2bv 3) (bv2nat (bvor ((_ int2bv 3) x) ((_ int2bv 3) x)))))) (= 1 (bv2nat ((_ int2bv 3) 1))))) (= ((_ extract 0 0) (bvand ((_ int2bv 3) (bv2nat (bvor ((_ int2bv 3) x) ((_ int2bv 3) x)))) ((_ int2bv 3) 1))) (_ bv0 1))))
+
+(check-sat)