(benchmark wchains010ue.smt
:source {
This benchmark generates write chain permutations and tries to show
via extensionality that they are equal.

Contributed by Armin Biere (armin.biere@jku.at).
}
:status unsat
:category { crafted }
:logic QF_AUFBV
:difficulty { 2 }
:extrafuns ((a1 Array[32:8]))
:extrafuns ((v6 BitVec[32]))
:extrafuns ((v7 BitVec[32]))
:extrafuns ((v8 BitVec[32]))
:extrafuns ((v9 BitVec[32]))
:extrafuns ((v10 BitVec[32]))
:extrafuns ((v11 BitVec[32]))
:extrafuns ((v12 BitVec[32]))
:extrafuns ((v13 BitVec[32]))
:extrafuns ((v14 BitVec[32]))
:extrafuns ((v15 BitVec[32]))
:formula
(let (?e2 bv0[32])
(let (?e3 bv1[32])
(let (?e4 bv2[32])
(let (?e5 bv3[32])
(let (?e16 (bvadd ?e2 v6))
(let (?e17 (extract[7:0] v6))
(let (?e18 (store a1 ?e16 ?e17))
(let (?e19 (bvadd ?e3 v6))
(let (?e20 (extract[15:8] v6))
(let (?e21 (store ?e18 ?e19 ?e20))
(let (?e22 (bvadd ?e4 v6))
(let (?e23 (extract[23:16] v6))
(let (?e24 (store ?e21 ?e22 ?e23))
(let (?e25 (bvadd ?e5 v6))
(let (?e26 (extract[31:24] v6))
(let (?e27 (store ?e24 ?e25 ?e26))
(let (?e28 (bvadd ?e2 v7))
(let (?e29 (extract[7:0] v7))
(let (?e30 (store ?e27 ?e28 ?e29))
(let (?e31 (bvadd ?e3 v7))
(let (?e32 (extract[15:8] v7))
(let (?e33 (store ?e30 ?e31 ?e32))
(let (?e34 (bvadd ?e4 v7))
(let (?e35 (extract[23:16] v7))
(let (?e36 (store ?e33 ?e34 ?e35))
(let (?e37 (bvadd ?e5 v7))
(let (?e38 (extract[31:24] v7))
(let (?e39 (store ?e36 ?e37 ?e38))
(let (?e40 (bvadd ?e2 v8))
(let (?e41 (extract[7:0] v8))
(let (?e42 (store ?e39 ?e40 ?e41))
(let (?e43 (bvadd ?e3 v8))
(let (?e44 (extract[15:8] v8))
(let (?e45 (store ?e42 ?e43 ?e44))
(let (?e46 (bvadd ?e4 v8))
(let (?e47 (extract[23:16] v8))
(let (?e48 (store ?e45 ?e46 ?e47))
(let (?e49 (bvadd ?e5 v8))
(let (?e50 (extract[31:24] v8))
(let (?e51 (store ?e48 ?e49 ?e50))
(let (?e52 (bvadd ?e2 v9))
(let (?e53 (extract[7:0] v9))
(let (?e54 (store ?e51 ?e52 ?e53))
(let (?e55 (bvadd ?e3 v9))
(let (?e56 (extract[15:8] v9))
(let (?e57 (store ?e54 ?e55 ?e56))
(let (?e58 (bvadd ?e4 v9))
(let (?e59 (extract[23:16] v9))
(let (?e60 (store ?e57 ?e58 ?e59))
(let (?e61 (bvadd ?e5 v9))
(let (?e62 (extract[31:24] v9))
(let (?e63 (store ?e60 ?e61 ?e62))
(let (?e64 (bvadd ?e2 v10))
(let (?e65 (extract[7:0] v10))
(let (?e66 (store ?e63 ?e64 ?e65))
(let (?e67 (bvadd ?e3 v10))
(let (?e68 (extract[15:8] v10))
(let (?e69 (store ?e66 ?e67 ?e68))
(let (?e70 (bvadd ?e4 v10))
(let (?e71 (extract[23:16] v10))
(let (?e72 (store ?e69 ?e70 ?e71))
(let (?e73 (bvadd ?e5 v10))
(let (?e74 (extract[31:24] v10))
(let (?e75 (store ?e72 ?e73 ?e74))
(let (?e76 (bvadd ?e2 v11))
(let (?e77 (extract[7:0] v11))
(let (?e78 (store ?e75 ?e76 ?e77))
(let (?e79 (bvadd ?e3 v11))
(let (?e80 (extract[15:8] v11))
(let (?e81 (store ?e78 ?e79 ?e80))
(let (?e82 (bvadd ?e4 v11))
(let (?e83 (extract[23:16] v11))
(let (?e84 (store ?e81 ?e82 ?e83))
(let (?e85 (bvadd ?e5 v11))
(let (?e86 (extract[31:24] v11))
(let (?e87 (store ?e84 ?e85 ?e86))
(let (?e88 (bvadd ?e2 v12))
(let (?e89 (extract[7:0] v12))
(let (?e90 (store ?e87 ?e88 ?e89))
(let (?e91 (bvadd ?e3 v12))
(let (?e92 (extract[15:8] v12))
(let (?e93 (store ?e90 ?e91 ?e92))
(let (?e94 (bvadd ?e4 v12))
(let (?e95 (extract[23:16] v12))
(let (?e96 (store ?e93 ?e94 ?e95))
(let (?e97 (bvadd ?e5 v12))
(let (?e98 (extract[31:24] v12))
(let (?e99 (store ?e96 ?e97 ?e98))
(let (?e100 (bvadd ?e2 v13))
(let (?e101 (extract[7:0] v13))
(let (?e102 (store ?e99 ?e100 ?e101))
(let (?e103 (bvadd ?e3 v13))
(let (?e104 (extract[15:8] v13))
(let (?e105 (store ?e102 ?e103 ?e104))
(let (?e106 (bvadd ?e4 v13))
(let (?e107 (extract[23:16] v13))
(let (?e108 (store ?e105 ?e106 ?e107))
(let (?e109 (bvadd ?e5 v13))
(let (?e110 (extract[31:24] v13))
(let (?e111 (store ?e108 ?e109 ?e110))
(let (?e112 (bvadd ?e2 v14))
(let (?e113 (extract[7:0] v14))
(let (?e114 (store ?e111 ?e112 ?e113))
(let (?e115 (bvadd ?e3 v14))
(let (?e116 (extract[15:8] v14))
(let (?e117 (store ?e114 ?e115 ?e116))
(let (?e118 (bvadd ?e4 v14))
(let (?e119 (extract[23:16] v14))
(let (?e120 (store ?e117 ?e118 ?e119))
(let (?e121 (bvadd ?e5 v14))
(let (?e122 (extract[31:24] v14))
(let (?e123 (store ?e120 ?e121 ?e122))
(let (?e124 (bvadd ?e2 v15))
(let (?e125 (extract[7:0] v15))
(let (?e126 (store ?e123 ?e124 ?e125))
(let (?e127 (bvadd ?e3 v15))
(let (?e128 (extract[15:8] v15))
(let (?e129 (store ?e126 ?e127 ?e128))
(let (?e130 (bvadd ?e4 v15))
(let (?e131 (extract[23:16] v15))
(let (?e132 (store ?e129 ?e130 ?e131))
(let (?e133 (bvadd ?e5 v15))
(let (?e134 (extract[31:24] v15))
(let (?e135 (store ?e132 ?e133 ?e134))
(let (?e136 (store a1 ?e124 ?e125))
(let (?e137 (store ?e136 ?e127 ?e128))
(let (?e138 (store ?e137 ?e130 ?e131))
(let (?e139 (store ?e138 ?e133 ?e134))
(let (?e140 (store ?e139 ?e112 ?e113))
(let (?e141 (store ?e140 ?e115 ?e116))
(let (?e142 (store ?e141 ?e118 ?e119))
(let (?e143 (store ?e142 ?e121 ?e122))
(let (?e144 (store ?e143 ?e100 ?e101))
(let (?e145 (store ?e144 ?e103 ?e104))
(let (?e146 (store ?e145 ?e106 ?e107))
(let (?e147 (store ?e146 ?e109 ?e110))
(let (?e148 (store ?e147 ?e88 ?e89))
(let (?e149 (store ?e148 ?e91 ?e92))
(let (?e150 (store ?e149 ?e94 ?e95))
(let (?e151 (store ?e150 ?e97 ?e98))
(let (?e152 (store ?e151 ?e76 ?e77))
(let (?e153 (store ?e152 ?e79 ?e80))
(let (?e154 (store ?e153 ?e82 ?e83))
(let (?e155 (store ?e154 ?e85 ?e86))
(let (?e156 (store ?e155 ?e64 ?e65))
(let (?e157 (store ?e156 ?e67 ?e68))
(let (?e158 (store ?e157 ?e70 ?e71))
(let (?e159 (store ?e158 ?e73 ?e74))
(let (?e160 (store ?e159 ?e52 ?e53))
(let (?e161 (store ?e160 ?e55 ?e56))
(let (?e162 (store ?e161 ?e58 ?e59))
(let (?e163 (store ?e162 ?e61 ?e62))
(let (?e164 (store ?e163 ?e40 ?e41))
(let (?e165 (store ?e164 ?e43 ?e44))
(let (?e166 (store ?e165 ?e46 ?e47))
(let (?e167 (store ?e166 ?e49 ?e50))
(let (?e168 (store ?e167 ?e28 ?e29))
(let (?e169 (store ?e168 ?e31 ?e32))
(let (?e170 (store ?e169 ?e34 ?e35))
(let (?e171 (store ?e170 ?e37 ?e38))
(let (?e172 (store ?e171 ?e16 ?e17))
(let (?e173 (store ?e172 ?e19 ?e20))
(let (?e174 (store ?e173 ?e22 ?e23))
(let (?e175 (store ?e174 ?e25 ?e26))
(let (?e176 (ite (= ?e135 ?e175) bv1[1] bv0[1]))
(let (?e177 (extract[1:0] v6))
(let (?e178 bv0[2])
(let (?e179 (ite (= ?e177 ?e178) bv1[1] bv0[1]))
(let (?e180 (bvand (bvnot ?e176) ?e179))
(let (?e181 (extract[1:0] v7))
(let (?e182 (ite (= ?e178 ?e181) bv1[1] bv0[1]))
(let (?e183 (bvand ?e180 ?e182))
(let (?e184 (extract[1:0] v8))
(let (?e185 (ite (= ?e178 ?e184) bv1[1] bv0[1]))
(let (?e186 (bvand ?e183 ?e185))
(let (?e187 (extract[1:0] v9))
(let (?e188 (ite (= ?e178 ?e187) bv1[1] bv0[1]))
(let (?e189 (bvand ?e186 ?e188))
(let (?e190 (extract[1:0] v10))
(let (?e191 (ite (= ?e178 ?e190) bv1[1] bv0[1]))
(let (?e192 (bvand ?e189 ?e191))
(let (?e193 (extract[1:0] v11))
(let (?e194 (ite (= ?e178 ?e193) bv1[1] bv0[1]))
(let (?e195 (bvand ?e192 ?e194))
(let (?e196 (extract[1:0] v12))
(let (?e197 (ite (= ?e178 ?e196) bv1[1] bv0[1]))
(let (?e198 (bvand ?e195 ?e197))
(let (?e199 (extract[1:0] v13))
(let (?e200 (ite (= ?e178 ?e199) bv1[1] bv0[1]))
(let (?e201 (bvand ?e198 ?e200))
(let (?e202 (extract[1:0] v14))
(let (?e203 (ite (= ?e178 ?e202) bv1[1] bv0[1]))
(let (?e204 (bvand ?e201 ?e203))
(let (?e205 (extract[1:0] v15))
(let (?e206 (ite (= ?e178 ?e205) bv1[1] bv0[1]))
(let (?e207 (bvand ?e204 ?e206))
(not (= ?e207 bv0[1]))
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))