From: Tim King <taking@cs.nyu.edu>
Date: Sun, 25 Nov 2012 01:02:49 +0000 (+0000)
Subject: Adding a regression test from bug 462.
X-Git-Tag: cvc5-1.0.0~7565
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c10c62d53ae784f22021cd172697eded385e5d69;p=cvc5.git

Adding a regression test from bug 462.
---

diff --git a/test/regress/regress0/auflia/Makefile.am b/test/regress/regress0/auflia/Makefile.am
index cce2866f5..d12bb0441 100644
--- 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
index 000000000..e843e0b41
--- /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
+))))))