1 files changed, 27 insertions, 0 deletions
diff --git a/src/lfsc/tests/array_ext.smt2 b/src/lfsc/tests/array_ext.smt2
new file mode 100644
index 0000000..4f7586a
--- /dev/null
+++ b/src/lfsc/tests/array_ext.smt2
@@ -0,0 +1,27 @@
+;; (set-logic QF_ALIA)
+(set-logic QF_AUFBVLIA)
+
+(declare-fun a () (Array Int Int))
+(declare-fun b () (Array Int Int))
+(declare-fun c () (Array Int Int))
+(declare-fun d () (Array Int Int))
+
+;; (assert (= c (store b 0 4)))
+;; (assert (= d (store (store b 0 4) 1 4)))
+
+;; (assert (= a (store d 1 (select b 1))))
+
+;; (assert (not (= a c)))
+
+
+(assert (not
+(=> (= c (store b 0 4))
+(=> (= d (store (store b 0 4) 1 4))
+
+(=> (= a (store d 1 (select b 1)))
+    
+    (= a c))))))
+
+
+(check-sat)
+