diff --git a/tests/sat/bug25.smt2 b/tests/sat/bug25.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..cdba76b4f5be00d3677575a59a6637a58f8ee1c1
--- /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)