Adding hand minimized test for bug 450.

diff --git a/test/regress/regress0/auflia/Makefile.am b/test/regress/regress0/auflia/Makefile.am
index e35f24d13b9db8a789f0472b20f0f21197065fc4..cce2866f5cf53f488c2c46da72c89413b6db9353 100644 (file)
--- 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 (file)
index 0000000..c9c1112
--- /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)
+)
+)