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)
+