From e8b6775c1c43a704e4e6afdefad6378fdb200fd0 Mon Sep 17 00:00:00 2001
From: Clark Barrett <barrett@cs.nyu.edu>
Date: Mon, 14 Jun 2010 16:06:51 +0000
Subject: Started work on array theory

---
 test/regress/regress0/arr1.smt | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 test/regress/regress0/arr1.smt

(limited to 'test/regress/regress0')

diff --git a/test/regress/regress0/arr1.smt b/test/regress/regress0/arr1.smt
new file mode 100644
index 000000000..55ca99601
--- /dev/null
+++ b/test/regress/regress0/arr1.smt
@@ -0,0 +1,7 @@
+(benchmark simple_arr
+  :logic QF_AX
+  :status unsat
+  :extrafuns ((a Array))
+  :extrafuns ((i1 Index) (i2 Index))
+  :formula (not (implies (= i1 i2) (= (select a i1) (select a i2))))
+)
-- 
cgit v1.2.3