(benchmark wchains010ue.smt
:logic QF_AUFBV
:extrafuns ((v6 BitVec[32]))
:extrafuns ((a1 Array[32:8]))
:extrafuns ((v15 BitVec[32]))
:status sat
:formula
(let (?n1 bv0[1])
(let (?n2 (extract[1:0] v6))
(let (?n3 bv0[2])
(flet ($n4 (= ?n2 ?n3))
(let (?n5 bv1[1])
(let (?n6 (ite $n4 ?n5 ?n1))
(let (?n7 bv0[8])
(let (?n8 (store a1 v15 ?n7))
(let (?n9 bv1[32])
(let (?n10 (bvadd ?n9 v15))
(let (?n11 (store ?n8 ?n10 ?n7))
(let (?n12 bv3[32])
(let (?n13 (bvadd ?n12 v15))
(let (?n14 (store ?n11 ?n13 ?n7))
(let (?n15 (extract[7:0] v6))
(let (?n16 (store a1 v6 ?n15))
(let (?n17 (bvadd ?n9 v6))
(let (?n18 bv1[8])
(let (?n19 (store ?n16 ?n17 ?n18))
(let (?n20 (bvadd ?n12 v6))
(let (?n21 (store ?n19 ?n20 ?n18))
(flet ($n22 (= ?n14 ?n21))
(let (?n23 (ite $n22 ?n5 ?n1))
(let (?n24 (bvnot ?n23))
(let (?n25 (bvand ?n6 ?n24))
(flet ($n26 (= ?n1 ?n25))
(flet ($n27 (not $n26))
$n27
))))))))))))))))))))))))))))