Adding a regression test from bug 462.

diff --git a/test/regress/regress0/auflia/Makefile.am b/test/regress/regress0/auflia/Makefile.am
index cce2866f5cf53f488c2c46da72c89413b6db9353..d12bb04418f12d59b4c2f6820f80368d7beabffa 100644 (file)
--- a/test/regress/regress0/auflia/Makefile.am
+++ b/test/regress/regress0/auflia/Makefile.am
@@ -20,7 +20,8 @@ TESTS =       \
        fuzz03.smt \
        fuzz04.smt \
        fuzz05.smt \
-       a17.smt
+       a17.smt \
+       error72.delta2.smt
 
 EXTRA_DIST = $(TESTS)
 

diff --git a/test/regress/regress0/auflia/error72.delta2.smt b/test/regress/regress0/auflia/error72.delta2.smt
new file mode 100644 (file)
index 0000000..e843e0b
--- /dev/null
+++ b/test/regress/regress0/auflia/error72.delta2.smt
@@ -0,0 +1,12 @@
+(benchmark fuzzsmt
+:logic QF_AUFLIA
+:extrafuns ((v1 Int))
+:status sat
+:formula
+(let (?n1 0)
+(flet ($n2 (distinct v1 ?n1))
+(let (?n3 (ite $n2 v1 ?n1))
+(let (?n4 (~ ?n3))
+(flet ($n5 (>= ?n4 ?n1))
+$n5
+))))))