1 files changed, 48 insertions, 0 deletions
diff --git a/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta01.smt b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta01.smt
new file mode 100644
index 000000000..c7fed0c15
--- /dev/null
+++ b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta01.smt
@@ -0,0 +1,48 @@
+(benchmark mathsat
+:logic QF_UFLIA
+:extrafuns ((s_count Int Int))
+:extrafuns ((fmt1 Int))
+:extrafuns ((fmt_length Int))
+:status unsat
+:formula
+(let (?n1 0)
+(let (?n2 6)
+(let (?n3 (s_count ?n2))
+(flet ($n4 (= ?n1 ?n3))
+(let (?n5 5)
+(let (?n6 (s_count ?n5))
+(flet ($n7 (= ?n1 ?n6))
+(let (?n8 4)
+(let (?n9 (s_count ?n8))
+(flet ($n10 (= ?n1 ?n9))
+(let (?n11 3)
+(let (?n12 (s_count ?n11))
+(flet ($n13 (= ?n1 ?n12))
+(let (?n14 1)
+(let (?n15 (s_count ?n1))
+(flet ($n16 (= ?n14 ?n15))
+(let (?n17 (s_count ?n14))
+(flet ($n18 (= ?n1 ?n17))
+(flet ($n19 (and $n16 $n18))
+(let (?n20 2)
+(let (?n21 (s_count ?n20))
+(flet ($n22 (= ?n1 ?n21))
+(flet ($n23 (and $n19 $n22))
+(flet ($n24 (and $n13 $n23))
+(flet ($n25 (and $n10 $n24))
+(flet ($n26 (and $n7 $n25))
+(flet ($n27 (and $n4 $n26))
+(let (?n28 9)
+(flet ($n29 (= ?n28 fmt_length))
+(flet ($n30 (> fmt1 ?n14))
+(flet ($n31 (< fmt1 fmt_length))
+(flet ($n32 (and $n30 $n31))
+(let (?n33 (- fmt1 ?n20))
+(let (?n34 (s_count ?n33))
+(let (?n35 (+ ?n14 ?n34))
+(flet ($n36 (= ?n1 ?n35))
+(flet ($n37 (and $n32 $n36))
+(flet ($n38 (and $n29 $n37))
+(flet ($n39 (and $n27 $n38))
+$n39
+))))))))))))))))))))))))))))))))))))))))