From 4153a6600430452c5221e6f795fe36e2669d2cc6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Tue, 3 Aug 2021 16:24:35 +0200
Subject: [PATCH] Add regression test for #39

---
 tests/sat/arr.smt2 | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)
 create mode 100644 tests/sat/arr.smt2

diff --git a/tests/sat/arr.smt2 b/tests/sat/arr.smt2
new file mode 100644
index 000000000..ad58211f5
--- /dev/null
+++ b/tests/sat/arr.smt2
@@ -0,0 +1,27 @@
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+
+
+(declare-sort u 0)
+
+(declare-fun to_rep (u) Int)
+
+(declare-sort t 0)
+
+(declare-fun mk ((Array Int u) Bool) t)
+
+(declare-fun get_a (t) (Array Int u))
+
+(declare-fun get_b (t) Bool)
+(declare-const rliteral u)
+
+(declare-const r t)
+
+
+(assert
+  (= (to_rep (select (get_a (mk (store (get_a r) 3 rliteral) (get_b r))) 3)) 5))
+
+(assert
+  (not
+  (= (to_rep (select (get_a (mk (store (get_a r) 3 rliteral) (get_b r))) 1)) 5)))
+(check-sat)
-- 
GitLab