1 files changed, 0 insertions, 48 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
deleted file mode 100644
index 9dfba13d5..000000000
--- a/test/regress/regress0/decision/uflia-xs-09-16-3-4-1-5.delta03.smt
+++ /dev/null
@@ -1,48 +0,0 @@
-; COMMAND-LINE: --decision=justification
-; EXPECT: sat
-
-(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
-))))))))))))))))))))))))))))))))))))