(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
))))))))))))))))))))))))))))))))))))