(benchmark fuzzsmt
:logic QF_BV
:extrafuns ((v1 BitVec[2]))
:status unknown
:formula
(let (?n1 bv0[8])
(let (?n2 bv0[2])
(let (?n3 bv0[5])
(let (?n4 (sign_extend[3] v1))
(flet ($n5 (= ?n3 ?n4))
(let (?n6 bv1[1])
(let (?n7 bv0[1])
(let (?n8 (ite $n5 ?n6 ?n7))
(let (?n9 (concat ?n8 ?n3))
(let (?n10 (concat ?n2 ?n9))
(flet ($n11 (= ?n1 ?n10))
(flet ($n12 false)
(let (?n13 bv0[4])
(let (?n14 bv1[2])
(let (?n15 (bvcomp v1 ?n14))
(flet ($n16 (bvugt ?n15 ?n7))
(let (?n17 (ite $n16 ?n6 ?n7))
(let (?n18 (sign_extend[1] ?n17))
(let (?n19 (sign_extend[2] ?n18))
(flet ($n20 (= ?n13 ?n19))
(flet ($n21 true)
(let (?n22 bv0[16])
(let (?n23 bv0[3])
(flet ($n24 (bvsle ?n2 ?n18))
(let (?n25 (ite $n24 ?n6 ?n7))
(let (?n26 (zero_extend[2] ?n25))
(flet ($n27 (distinct ?n23 ?n26))
(let (?n28 (ite $n27 ?n6 ?n7))
(let (?n29 (zero_extend[15] ?n28))
(flet ($n30 (= ?n22 ?n29))
(flet ($n31 (if_then_else $n20 $n21 $n30))
(flet ($n32 (if_then_else $n11 $n12 $n31))
$n32
)))))))))))))))))))))))))))))))))