(benchmark fuzzsmt
:logic QF_AUFBV
:extrafuns ((v1 BitVec[3]))
:extrafuns ((a2 Array[13:3]))
:status unsat
:formula
(let (?n1 bv0[3])
(flet ($n2 (bvsgt v1 v1))
(let (?n3 bv1[1])
(let (?n4 bv0[1])
(let (?n5 (ite $n2 ?n3 ?n4))
(let (?n6 (sign_extend[2] ?n5))
(flet ($n7 (bvslt ?n6 v1))
(let (?n8 (ite $n7 ?n3 ?n4))
(let (?n9 (sign_extend[2] ?n8))
(let (?n10 bv0[13])
(let (?n11 (select a2 ?n10))
(let (?n12 (bvshl ?n9 ?n11))
(flet ($n13 (= ?n1 ?n12))
(flet ($n14 (not $n13))
(let (?n15 (bvnot ?n8))
(let (?n16 (zero_extend[10] ?n15))
(let (?n17 bv0[11])
(flet ($n18 (= ?n16 ?n17))
(flet ($n19 (not $n18))
(let (?n20 (repeat[2] ?n15))
(let (?n21 (zero_extend[9] ?n20))
(flet ($n22 (bvult ?n17 ?n21))
(flet ($n23 (and $n19 $n22))
(flet ($n24 (and $n14 $n23))
$n24
)))))))))))))))))))))))))