1 files changed, 34 insertions, 0 deletions
diff --git a/test/regress/regress0/rewriterules/native_arrays.smt2 b/test/regress/regress0/rewriterules/native_arrays.smt2
new file mode 100644
index 000000000..1be13167d
--- /dev/null
+++ b/test/regress/regress0/rewriterules/native_arrays.smt2
@@ -0,0 +1,34 @@
+;; This example can't be done if we don't access the EqualityEngine of
+;; the theory of arrays
+
+(set-logic AUFLIA)
+(set-info :status unsat)
+
+(declare-sort Index 0)
+(declare-sort Element 0)
+
+;;A dumb predicate for a simple example
+(declare-fun P (Element) Bool)
+
+(assert-rewrite ((?i1 Index) (?i2 Index) (?e Element) (?a (Array Index Element))) ()
+                (P (select (store ?a ?i1 ?e) ?i2)) true () )
+
+(declare-fun a1 () (Array Index Element))
+(declare-fun a2 () (Array Index Element))
+(declare-fun a3 () (Array Index Element))
+(declare-fun i1 () Index)
+(declare-fun i2 () Index)
+(declare-fun e1 () Element)
+
+(assert (not (=>  (or (= a1 (store a2 i1 e1)) (= a1 (store a3 i1 e1))) (P (select a1 i2)) )))
+(check-sat)
+(exit)
+
+
+;; (declare-fun a1 () (Array Index Element))
+;; (declare-fun a2 () (Array Index Element))
+;; (declare-fun i1 () Index)
+;; (assert (= (store a1 i1 (select a2 i1)) (store a2 i1 (select a1 i1))))
+;; (assert (not (= a1 a2)))
+;; (check-sat)
+;; (exit)