diff options
Diffstat (limited to 'src/lfsc/tests/array_ext2.smt2')
-rw-r--r-- | src/lfsc/tests/array_ext2.smt2 | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/src/lfsc/tests/array_ext2.smt2 b/src/lfsc/tests/array_ext2.smt2 new file mode 100644 index 0000000..67d2a09 --- /dev/null +++ b/src/lfsc/tests/array_ext2.smt2 @@ -0,0 +1,31 @@ +;; (set-logic QF_ALIA) +(set-logic QF_AUFBVLIA) + +(declare-fun bv1 () (_ BitVec 32)) +(declare-fun bv2 () (_ BitVec 32)) + +(declare-fun bv3 () (_ BitVec 32)) + + +(declare-fun a () (Array (_ BitVec 32) (_ BitVec 32))) +(declare-fun b () (Array (_ BitVec 32) (_ BitVec 32))) +(declare-fun c () (Array (_ BitVec 32) (_ BitVec 32))) +(declare-fun d () (Array (_ BitVec 32) (_ BitVec 32))) + +(assert (= #b00000000000000000000000000000000 bv1)) +(assert (= #b00000000000000000000000000000001 bv2)) +(assert (= #b00000000000000000000000000000100 bv3)) + + + +(assert (not +(=> (= c (store b bv1 bv3)) +(=> (= d (store (store b bv1 bv3) bv2 bv3)) + +(=> (= a (store d bv2 (select b bv2))) + + (= a c)))))) + + +(check-sat) + |