diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-10-13 17:44:19 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-10-13 17:44:19 -0500 |
commit | 9da056f71c0c4a8ed5afd01c300e9c86cfcf5601 (patch) | |
tree | 9cc4ed5a09640c3dbb8df9cbaf242ade0f8acc4f /test/regress/regress0/bv | |
parent | 7e750757ac9832b70b5c6ca1d15e17cddbd2e6c0 (diff) |
Merging bv parts of ajr/bvExt branch, minor additions to ExtTheory.
Diffstat (limited to 'test/regress/regress0/bv')
-rw-r--r-- | test/regress/regress0/bv/bv2nat-ground-c.smt2 | 15 | ||||
-rw-r--r-- | test/regress/regress0/bv/bv2nat-ground.smt2 | 16 | ||||
-rw-r--r-- | test/regress/regress0/bv/cmu-rdk-3.smt2 | 9 |
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) |