(benchmark fuzzsmt
:logic QF_BV
:extrafuns ((v0 BitVec[4]))
:extrafuns ((v1 BitVec[4]))
:extrafuns ((v2 BitVec[4]))
:extrafuns ((v3 BitVec[4]))
:extrafuns ((v4 BitVec[4]))
:extrafuns ((v5 BitVec[4]))
:status unsat
:formula
(flet ($n1 true)
(let (?n2 (extract[0:0] v2))
(let (?n3 (zero_extend[1] ?n2))
(let (?n4 (zero_extend[2] ?n3))
(let (?n5 bv0[4])
(flet ($n6 (distinct ?n5 v4))
(let (?n7 bv1[1])
(let (?n8 bv0[1])
(let (?n9 (ite $n6 ?n7 ?n8))
(let (?n10 (sign_extend[3] ?n9))
(let (?n11 (bvadd ?n4 ?n10))
(flet ($n12 (bvsle ?n11 ?n5))
(let (?n13 (ite $n12 ?n7 ?n8))
(let (?n14 (sign_extend[3] ?n13))
(let (?n15 bv11[4])
(flet ($n16 (bvsge ?n15 v5))
(let (?n17 (ite $n16 ?n7 ?n8))
(let (?n18 (zero_extend[3] ?n17))
(flet ($n19 (bvult ?n14 ?n18))
(let (?n20 (ite $n19 ?n7 ?n8))
(flet ($n21 (bvsge v2 ?n15))
(let (?n22 (ite $n21 ?n7 ?n8))
(let (?n23 (sign_extend[3] ?n22))
(let (?n24 (bvlshr v4 ?n23))
(let (?n25 (bvmul v5 ?n24))
(flet ($n26 (bvslt ?n25 v2))
(let (?n27 (ite $n26 ?n7 ?n8))
(flet ($n28 (bvsge ?n20 ?n27))
(let (?n29 (ite $n28 ?n7 ?n8))
(let (?n30 (zero_extend[3] ?n29))
(flet ($n31 (bvugt v3 ?n30))
(flet ($n32 (bvugt v0 ?n5))
(let (?n33 (ite $n32 ?n7 ?n8))
(let (?n34 (zero_extend[3] ?n33))
(flet ($n35 (bvsge v1 ?n34))
(let (?n36 (ite $n35 ?n7 ?n8))
(let (?n37 (sign_extend[3] ?n36))
(let (?n38 (bvashr v1 ?n37))
(let (?n39 bv10[4])
(flet ($n40 (bvult ?n38 ?n39))
(flet ($n41 false)
(let (?n42 (bvashr v3 ?n4))
(let (?n43 bv1[4])
(flet ($n44 (bvule ?n42 ?n43))
(let (?n45 (ite $n44 ?n7 ?n8))
(let (?n46 (zero_extend[3] ?n45))
(flet ($n47 (bvsge ?n46 ?n38))
(let (?n48 (ite $n47 ?n7 ?n8))
(let (?n49 (sign_extend[1] ?n48))
(let (?n50 bv0[2])
(flet ($n51 (bvsge ?n49 ?n50))
(let (?n52 (ite $n51 ?n7 ?n8))
(flet ($n53 (= ?n27 ?n52))
(let (?n54 (ite $n53 ?n7 ?n8))
(flet ($n55 (bvult ?n25 v1))
(let (?n56 (ite $n55 ?n7 ?n8))
(let (?n57 (bvadd ?n7 ?n56))
(let (?n58 (bvneg v4))
(flet ($n59 (bvslt ?n58 ?n5))
(let (?n60 (ite $n59 ?n7 ?n8))
(let (?n61 (bvashr ?n57 ?n60))
(let (?n62 (sign_extend[3] ?n61))
(let (?n63 (sign_extend[3] ?n54))
(flet ($n64 (bvugt ?n62 ?n63))
(let (?n65 (ite $n64 ?n7 ?n8))
(flet ($n66 (distinct ?n54 ?n65))
(flet ($n67 (not $n66))
(let (?n68 (sign_extend[3] ?n45))
(let (?n69 (bvcomp v3 ?n68))
(flet ($n70 (bvule ?n7 ?n69))
(flet ($n71 (or $n41 $n67 $n70))
(let (?n72 (sign_extend[3] ?n7))
(flet ($n73 (bvsle ?n72 ?n58))
(let (?n74 (sign_extend[3] ?n2))
(flet ($n75 (distinct ?n5 ?n74))
(let (?n76 (ite $n75 ?n7 ?n8))
(let (?n77 (sign_extend[3] ?n76))
(flet ($n78 (bvsle ?n25 ?n5))
(let (?n79 (ite $n78 ?n7 ?n8))
(let (?n80 (zero_extend[3] ?n79))
(let (?n81 (bvxnor ?n11 ?n80))
(flet ($n82 (bvsle ?n77 ?n81))
(flet ($n83 (not $n82))
(let (?n84 (extract[2:0] v3))
(let (?n85 (concat ?n84 ?n52))
(flet ($n86 (bvsle ?n85 ?n72))
(flet ($n87 (bvuge ?n5 ?n10))
(let (?n88 (ite $n87 ?n7 ?n8))
(let (?n89 (zero_extend[3] ?n88))
(let (?n90 (bvmul v4 ?n89))
(flet ($n91 (bvsgt ?n90 ?n5))
(let (?n92 (ite $n91 ?n7 ?n8))
(let (?n93 (sign_extend[3] ?n92))
(flet ($n94 (bvsgt ?n18 ?n5))
(let (?n95 (ite $n94 ?n7 ?n8))
(flet ($n96 (bvult v4 v4))
(let (?n97 (ite $n96 ?n7 ?n8))
(flet ($n98 (bvsge ?n95 ?n97))
(let (?n99 (ite $n98 ?n7 ?n8))
(let (?n100 (zero_extend[3] ?n99))
(flet ($n101 (bvsge ?n93 ?n100))
(let (?n102 (ite $n101 ?n7 ?n8))
(flet ($n103 (bvsle ?n8 ?n102))
(flet ($n104 (or $n41 $n86 $n103))
(let (?n105 (zero_extend[3] ?n20))
(flet ($n106 (bvuge ?n5 ?n105))
(flet ($n107 (bvule ?n25 ?n5))
(let (?n108 (ite $n107 ?n7 ?n8))
(let (?n109 (sign_extend[2] ?n108))
(flet ($n110 (= ?n2 ?n7))
(let (?n111 (ite $n110 ?n25 ?n42))
(flet ($n112 (bvsle ?n5 ?n111))
(let (?n113 (ite $n112 ?n7 ?n8))
(let (?n114 (extract[1:0] ?n38))
(let (?n115 (concat ?n113 ?n114))
(flet ($n116 (= ?n109 ?n115))
(flet ($n117 (and $n31 $n40 $n71 $n73 $n83 $n104 $n106 $n116))
$n117
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))