From 83bb1b948dc169576d82fed4fef0b4681a680be2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Thu, 1 Apr 2021 16:10:50 +0200
Subject: [PATCH] Fixes #25

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

diff --git a/tests/sat/bug25.smt2 b/tests/sat/bug25.smt2
new file mode 100644
index 000000000..cdba76b4f
--- /dev/null
+++ b/tests/sat/bug25.smt2
@@ -0,0 +1,64 @@
+;; produced by colibri.drv ;;
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+;;; generated by SMT-LIB2 driver
+;;; SMT-LIB2 driver: bit-vectors, common part
+;;; SMT-LIB2: integer arithmetic
+
+
+(declare-sort value 0)
+
+(declare-fun valueqtint (value) Int)
+
+(define-fun to_rep ((x value)) Int (valueqtint x))
+
+
+(declare-const a (Array Int (Array Int value)))
+
+(declare-const i Int)
+(declare-const j Int)
+
+(declare-const x value)
+(declare-const y value)
+
+(assert
+  (not
+  (= (to_rep
+       (select
+         (select
+            (store
+              (store a i
+                (store
+                  (select a i)
+                  j x))
+                i
+                (store
+                  (select
+                    (store a i
+                      (store
+                        (select a i)
+                        j x))
+                    i)
+                  j y))
+              i)
+          j))
+     (to_rep
+        (select
+          (select
+            (store
+              (store a i
+                (store
+                  (select a i)
+                  j x))
+              i
+              (store
+                (select
+                  (store a i
+                    (store
+                      (select a i)
+                      j x))
+                  i)
+                j y))
+            j)
+        i)))))
+(check-sat)
-- 
GitLab