minimized example

diff --git a/test/regress/regress0/arrays/Makefile.am b/test/regress/regress0/arrays/Makefile.am
index 2e302f1ee5ac279aba54368dd686df6ceaeaa537..e3b30827ce215819f0f54d290bb79da33de521d0 100644 (file)
--- 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 (file)
index 0000000..aa803d0
--- /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
+)))))))))))