From c10c62d53ae784f22021cd172697eded385e5d69 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Sun, 25 Nov 2012 01:02:49 +0000
Subject: [PATCH] Adding a regression test from bug 462.

---
 test/regress/regress0/auflia/Makefile.am        |  3 ++-
 test/regress/regress0/auflia/error72.delta2.smt | 12 ++++++++++++
 2 files changed, 14 insertions(+), 1 deletion(-)
 create mode 100644 test/regress/regress0/auflia/error72.delta2.smt

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