From: Morgan Deters <mdeters@gmail.com>
Date: Mon, 11 Jul 2011 16:53:50 +0000 (+0000)
Subject: minimized example
X-Git-Tag: cvc5-1.0.0~8506
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b16e3a3187ce721e32042f241cc718529cdd0573;p=cvc5.git

minimized example
---

diff --git a/test/regress/regress0/arrays/Makefile.am b/test/regress/regress0/arrays/Makefile.am
index 2e302f1ee..e3b30827c 100644
--- a/test/regress/regress0/arrays/Makefile.am
+++ b/test/regress/regress0/arrays/Makefile.am
@@ -13,6 +13,7 @@ TESTS =	\
 EXTRA_DIST = $(TESTS) \
 	incorrect1.smt \
 	incorrect2.smt \
+	incorrect2.minimized.smt \
 	incorrect3.smt \
 	incorrect4.smt \
 	incorrect5.smt \
diff --git a/test/regress/regress0/arrays/incorrect2.minimized.smt b/test/regress/regress0/arrays/incorrect2.minimized.smt
new file mode 100644
index 000000000..aa803d060
--- /dev/null
+++ b/test/regress/regress0/arrays/incorrect2.minimized.smt
@@ -0,0 +1,19 @@
+(benchmark fuzzsmt
+:logic QF_AX
+:extrafuns ((v3 Index))
+:extrafuns ((v4 Index))
+:extrafuns ((v2 Index))
+:status unknown
+:formula
+(flet ($n1 true)
+(flet ($n2 (= v4 v3))
+(flet ($n3 (xor $n1 $n2))
+(flet ($n4 (distinct v2 v3))
+(let (?n5 (ite $n4 v3 v4))
+(let (?n6 (ite $n4 ?n5 v3))
+(flet ($n7 (distinct v4 ?n6))
+(flet ($n8 false)
+(flet ($n9 (if_then_else $n7 $n8 $n1))
+(flet ($n10 (and $n3 $n9))
+$n10
+)))))))))))