(benchmark fuzzsmt
:logic QF_BV
:extrafuns ((v2 BitVec[13]))
:extrafuns ((v1 BitVec[2]))
:status sat
:formula
(let (?n1 bv1[1])
(let (?n2 bv0[2])
(flet ($n3 (bvsge ?n2 v1))
(let (?n4 bv0[1])
(let (?n5 (ite $n3 ?n1 ?n4))
(flet ($n6 (= ?n1 ?n5))
(let (?n7 bv0[13])
(flet ($n8 (bvslt ?n7 v2))
(let (?n9 (ite $n8 ?n1 ?n4))
(let (?n10 (bvneg ?n9))
(let (?n11 (ite $n6 ?n10 ?n9))
(let (?n12 (zero_extend[12] ?n11))
(flet ($n13 (= v2 ?n12))
(flet ($n14 (= ?n1 ?n9))
(flet ($n15 (and $n13 $n14))
(flet ($n16 (not $n15))
(let (?n17 (bvashr v2 v2))
(let (?n18 (bvshl v2 ?n17))
(flet ($n19 (= ?n7 ?n18))
(let (?n20 bv1[13])
(let (?n21 (bvsub ?n20 v2))
(flet ($n22 (= ?n17 ?n21))
(let (?n23 bv1[10])
(let (?n24 (sign_extend[9] ?n11))
(flet ($n25 (= ?n23 ?n24))
(flet ($n26 (if_then_else $n19 $n22 $n25))
(flet ($n27 (bvult ?n10 ?n1))
(let (?n28 (ite $n27 ?n1 ?n4))
(flet ($n29 (= ?n11 ?n28))
(let (?n30 bv0[4])
(let (?n31 (sign_extend[3] ?n11))
(flet ($n32 (= ?n30 ?n31))
(flet ($n33 (implies $n29 $n32))
(flet ($n34 (if_then_else $n26 $n33 $n26))
(flet ($n35 (implies $n16 $n34))
$n35
))))))))))))))))))))))))))))))))))))