From 8b4a32e3ce10ebd28ce5f558e78a5214bfe84e82 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Mon, 19 Nov 2012 19:41:07 +0000
Subject: Adding hand minimized test for bug 450.

---
 test/regress/regress0/auflia/Makefile.am |  3 ++-
 test/regress/regress0/auflia/a17.smt     | 21 +++++++++++++++++++++
 2 files changed, 23 insertions(+), 1 deletion(-)
 create mode 100644 test/regress/regress0/auflia/a17.smt

(limited to 'test')

diff --git a/test/regress/regress0/auflia/Makefile.am b/test/regress/regress0/auflia/Makefile.am
index e35f24d13..cce2866f5 100644
--- a/test/regress/regress0/auflia/Makefile.am
+++ b/test/regress/regress0/auflia/Makefile.am
@@ -19,7 +19,8 @@ TESTS =	\
 	fuzz02.smt \
 	fuzz03.smt \
 	fuzz04.smt \
-	fuzz05.smt
+	fuzz05.smt \
+	a17.smt
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/auflia/a17.smt b/test/regress/regress0/auflia/a17.smt
new file mode 100644
index 000000000..c9c1112e4
--- /dev/null
+++ b/test/regress/regress0/auflia/a17.smt
@@ -0,0 +1,21 @@
+(benchmark fuzzsmt
+:logic QF_AUFLIA
+:extrafuns ((a Array))
+:extrafuns ((x1 Int))
+:extrafuns ((y1 Int))
+:extrafuns ((z0 Int))
+:extrapreds ((p Array))
+:status sat
+:formula
+(and
+     (>= (select (store a (+ x1 z0) 1) x1) 1)
+     (p a)
+     (p (store a (+ x1 z0) 1))
+     (p (store (store a (+ x1 z0) 1) y1 1))
+     (>= x1 1)
+     (>= z0 0)
+     (<= z0 0)
+     (<= y1 1)
+     (>= y1 1)
+)
+)
-- 
cgit v1.2.3