From: Tim King <taking@cs.nyu.edu>
Date: Mon, 19 Nov 2012 19:41:07 +0000 (+0000)
Subject: Adding hand minimized test for bug 450.
X-Git-Tag: cvc5-1.0.0~7573
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8b4a32e3ce10ebd28ce5f558e78a5214bfe84e82;p=cvc5.git

Adding hand minimized test for bug 450.
---

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)
+)
+)