(benchmark mathsat
:logic QF_UFLIA
:extrafuns ((arg1 Int))
:extrafuns ((adr_lo Int))
:extrafuns ((select_format Int Int))
:extrafuns ((x Int))
:status sat
:formula
(let (?n1 (select_format arg1))
(flet ($n2 (= ?n1 adr_lo))
(let (?n3 0)
(flet ($n4 (= ?n3 x))
(let (?n5 4)
(let (?n6 (select_format ?n5))
(flet ($n7 (= adr_lo ?n6))
(let (?n8 3)
(let (?n9 (select_format ?n8))
(flet ($n10 (= adr_lo ?n9))
(let (?n11 2)
(let (?n12 (select_format ?n11))
(flet ($n13 (= adr_lo ?n12))
(let (?n14 1)
(let (?n15 (select_format ?n3))
(flet ($n16 (= ?n14 ?n15))
(let (?n17 (select_format ?n14))
(flet ($n18 (= ?n3 ?n17))
(flet ($n19 (or $n16 $n18))
(flet ($n20 (or $n13 $n19))
(flet ($n21 (or $n10 $n20))
(flet ($n22 (or $n7 $n21))
(flet ($n23 (or $n4 $n22))
(flet ($n24 (= adr_lo ?n8))
(flet ($n25 (< arg1 ?n5))
(flet ($n26 (>= arg1 ?n3))
(flet ($n27 (and $n25 $n26))
(flet ($n28 (and $n24 $n27))
(flet ($n29 (and $n23 $n28))
(flet ($n30 (and $n2 $n29))
$n30
)))))))))))))))))))))))))))))))