decision regressions, all but one fail

1 files changed, 45 insertions, 0 deletions

diff --git a/test/regress/regress0/decision/uflia-xs-09-16-3-4-1-5.delta03.smt b/test/regress/regress0/decision/uflia-xs-09-16-3-4-1-5.delta03.smt
new file mode 100644
index 000000000..6f65e83ec
--- /dev/null
+++ b/test/regress/regress0/decision/uflia-xs-09-16-3-4-1-5.delta03.smt
@@ -0,0 +1,45 @@
+(benchmark mathsat
+:logic QF_UFLIA
+:extrafuns ((fmt_length Int))
+:extrafuns ((fmt1 Int))
+:extrafuns ((arg1 Int))
+:extrafuns ((select_format Int Int))
+:status sat
+:formula
+(let (?n1 1)
+(let (?n2 (+ ?n1 fmt1))
+(let (?n3 (select_format ?n2))
+(flet ($n4 (= ?n1 ?n3))
+(let (?n5 (select_format arg1))
+(let (?n6 0)
+(flet ($n7 (= ?n5 ?n6))
+(flet ($n8 (and $n4 $n7))
+(let (?n9 7)
+(let (?n10 (select_format ?n9))
+(flet ($n11 (= ?n1 ?n10))
+(let (?n12 (select_format ?n6))
+(flet ($n13 (= ?n1 ?n12))
+(let (?n14 (select_format ?n1))
+(flet ($n15 (= ?n1 ?n14))
+(flet ($n16 (or $n13 $n15))
+(let (?n17 5)
+(let (?n18 (select_format ?n17))
+(flet ($n19 (= ?n6 ?n18))
+(flet ($n20 (or $n16 $n19))
+(let (?n21 6)
+(let (?n22 (select_format ?n21))
+(flet ($n23 (= ?n6 ?n22))
+(flet ($n24 (or $n20 $n23))
+(flet ($n25 (or $n11 $n24))
+(let (?n26 9)
+(flet ($n27 (= ?n26 fmt_length))
+(let (?n28 2)
+(let (?n29 (- fmt1 ?n28))
+(flet ($n30 (= arg1 ?n29))
+(flet ($n31 (< fmt1 fmt_length))
+(flet ($n32 (and $n30 $n31))
+(flet ($n33 (and $n27 $n32))
+(flet ($n34 (and $n25 $n33))
+(flet ($n35 (and $n8 $n34))
+$n35
+))))))))))))))))))))))))))))))))))))