(benchmark dubreva005ue.smt
:logic QF_AUFBV
:extrafuns ((a1 Array[32:8]))
:status unsat
:formula
(let (?n1 bv0[1])
(let (?n2 bv0[32])
(let (?n3 bv1[8])
(let (?n4 (store a1 ?n2 ?n3))
(let (?n5 (select a1 ?n2))
(let (?n6 (bvnot ?n3))
(let (?n7 (bvand ?n5 ?n6))
(let (?n8 (bvnot ?n7))
(let (?n9 (bvand ?n3 ?n8))
(let (?n10 (store ?n4 ?n2 ?n9))
(let (?n11 (select ?n10 ?n2))
(let (?n12 (store a1 ?n2 ?n11))
(let (?n13 (select ?n12 ?n2))
(let (?n14 (store a1 ?n2 ?n13))
(let (?n15 (select ?n14 ?n2))
(let (?n16 (store a1 ?n2 ?n15))
(let (?n17 (select ?n16 ?n2))
(let (?n18 (store a1 ?n2 ?n17))
(let (?n19 (select ?n18 ?n2))
(let (?n20 (store a1 ?n2 ?n19))
(flet ($n21 (= ?n4 ?n20))
(let (?n22 bv1[1])
(let (?n23 (ite $n21 ?n22 ?n1))
(let (?n24 (bvnot ?n23))
(flet ($n25 (= ?n1 ?n24))
(flet ($n26 (not $n25))
$n26
)))))))))))))))))))))))))))