1(benchmark fuzzsmt
2:logic QF_BV
3:status unsat
4:extrafuns ((v0 BitVec[4]))
5:extrafuns ((v1 BitVec[4]))
6:extrafuns ((v2 BitVec[4]))
7:extrafuns ((v3 BitVec[4]))
8:extrafuns ((v4 BitVec[4]))
9:formula
10(let (?e5 bv4[4])
11(let (?e6 bv12[4])
12(let (?e7 bv4[4])
13(let (?e8 (bvlshr ?e5 v0))
14(let (?e9 (ite (= bv1[1] (extract[1:1] ?e5)) v2 v1))
15(let (?e10 (bvsub ?e7 ?e6))
16(let (?e11 (zero_extend[0] ?e7))
17(let (?e12 (sign_extend[0] ?e9))
18(let (?e13 (bvnot ?e7))
19(let (?e14 (bvlshr ?e7 v3))
20(let (?e15 (extract[1:0] v0))
21(let (?e16 (bvneg ?e10))
22(let (?e17 (ite (= ?e9 v2) bv1[1] bv0[1]))
23(let (?e18 (bvmul ?e10 v0))
24(let (?e19 (bvadd ?e8 ?e14))
25(let (?e20 (zero_extend[0] ?e18))
26(let (?e21 (bvmul ?e8 ?e18))
27(let (?e22 (bvsub ?e11 ?e14))
28(let (?e23 (ite (bvugt v1 ?e5) bv1[1] bv0[1]))
29(let (?e24 (bvashr ?e14 ?e18))
30(let (?e25 (bvadd ?e21 ?e9))
31(let (?e26 (bvadd ?e20 ?e20))
32(let (?e27 (ite (bvslt (zero_extend[3] ?e23) v3) bv1[1] bv0[1]))
33(let (?e28 (ite (bvugt ?e9 ?e12) bv1[1] bv0[1]))
34(let (?e29 (bvnot ?e26))
35(let (?e30 (ite (bvult ?e21 ?e11) bv1[1] bv0[1]))
36(let (?e31 (bvsub v1 ?e20))
37(let (?e32 (ite (bvslt ?e19 (zero_extend[3] ?e28)) bv1[1] bv0[1]))
38(let (?e33 (rotate_right[0] ?e15))
39(let (?e34 (bvnot ?e14))
40(let (?e35 (zero_extend[0] ?e24))
41(let (?e36 (sign_extend[0] ?e22))
42(let (?e37 (ite (bvult ?e25 ?e10) bv1[1] bv0[1]))
43(let (?e38 (bvashr ?e27 ?e23))
44(let (?e39 (bvcomp v0 ?e31))
45(let (?e40 (bvand v0 ?e31))
46(let (?e41 (zero_extend[0] ?e21))
47(let (?e42 (ite (= bv1[1] (extract[0:0] ?e14)) ?e40 (sign_extend[3] ?e23)))
48(let (?e43 (sign_extend[0] ?e32))
49(let (?e44 (sign_extend[0] ?e19))
50(let (?e45 (ite (= bv1[1] (extract[2:2] ?e40)) (sign_extend[3] ?e27) ?e24))
51(let (?e46 (bvnot ?e21))
52(let (?e47 (rotate_right[3] v3))
53(let (?e48 (bvxnor (zero_extend[2] ?e15) ?e45))
54(let (?e49 (bvand ?e40 ?e46))
55(let (?e50 (ite (bvsle ?e20 ?e31) bv1[1] bv0[1]))
56(let (?e51 (bvneg ?e22))
57(let (?e52 (bvor ?e41 ?e22))
58(let (?e53 (ite (bvslt v1 ?e13) bv1[1] bv0[1]))
59(let (?e54 (bvshl ?e11 (sign_extend[3] ?e38)))
60(let (?e55 (ite (bvsge (zero_extend[3] ?e17) ?e40) bv1[1] bv0[1]))
61(let (?e56 (ite (distinct ?e52 (zero_extend[3] ?e17)) bv1[1] bv0[1]))
62(let (?e57 (bvneg ?e17))
63(let (?e58 (extract[3:0] ?e47))
64(let (?e59 (ite (bvugt ?e30 ?e17) bv1[1] bv0[1]))
65(let (?e60 (zero_extend[0] ?e48))
66(let (?e61 (bvshl (sign_extend[3] ?e59) v4))
67(flet ($e62 (bvsgt ?e60 (zero_extend[3] ?e57)))
68(flet ($e63 (bvule ?e15 (zero_extend[1] ?e38)))
69(flet ($e64 (distinct ?e16 (sign_extend[3] ?e30)))
70(flet ($e65 (= ?e25 ?e14))
71(flet ($e66 (bvsgt (sign_extend[3] ?e43) ?e10))
72(flet ($e67 (bvule (sign_extend[3] ?e39) ?e41))
73(flet ($e68 (bvult ?e25 ?e36))
74(flet ($e69 (bvugt ?e36 ?e24))
75(flet ($e70 (bvslt (zero_extend[3] ?e50) ?e12))
76(flet ($e71 (bvsle ?e25 (zero_extend[3] ?e32)))
77(flet ($e72 (bvsgt ?e37 ?e57))
78(flet ($e73 (bvuge ?e48 ?e47))
79(flet ($e74 (bvsle v2 ?e41))
80(flet ($e75 (bvule ?e48 (zero_extend[3] ?e53)))
81(flet ($e76 (bvsge (zero_extend[1] ?e28) ?e33))
82(flet ($e77 (distinct ?e33 (sign_extend[1] ?e55)))
83(flet ($e78 (bvule ?e27 ?e53))
84(flet ($e79 (= ?e55 ?e55))
85(flet ($e80 (bvule ?e55 ?e17))
86(flet ($e81 (bvuge ?e47 (sign_extend[3] ?e39)))
87(flet ($e82 (= ?e26 ?e22))
88(flet ($e83 (bvslt (sign_extend[2] ?e15) ?e35))
89(flet ($e84 (bvugt ?e23 ?e53))
90(flet ($e85 (bvslt ?e22 (zero_extend[3] ?e56)))
91(flet ($e86 (bvuge ?e10 (sign_extend[3] ?e38)))
92(flet ($e87 (bvsge ?e24 (zero_extend[3] ?e57)))
93(flet ($e88 (bvsgt ?e29 ?e21))
94(flet ($e89 (= ?e8 (sign_extend[3] ?e37)))
95(flet ($e90 (bvslt ?e41 ?e24))
96(flet ($e91 (bvsgt v3 (sign_extend[3] ?e43)))
97(flet ($e92 (= ?e57 ?e55))
98(flet ($e93 (bvsgt ?e16 (sign_extend[3] ?e28)))
99(flet ($e94 (bvsge (sign_extend[3] ?e37) v0))
100(flet ($e95 (bvsge ?e13 ?e44))
101(flet ($e96 (bvsle ?e18 ?e18))
102(flet ($e97 (bvuge ?e17 ?e38))
103(flet ($e98 (bvugt ?e51 ?e42))
104(flet ($e99 (= ?e47 ?e49))
105(flet ($e100 (bvule ?e43 ?e39))
106(flet ($e101 (bvsle ?e47 ?e45))
107(flet ($e102 (bvuge (zero_extend[3] ?e50) v3))
108(flet ($e103 (distinct ?e5 ?e34))
109(flet ($e104 (bvugt (zero_extend[3] ?e38) ?e29))
110(flet ($e105 (bvuge (sign_extend[3] ?e38) ?e58))
111(flet ($e106 (bvsge ?e28 ?e56))
112(flet ($e107 (distinct ?e51 ?e10))
113(flet ($e108 (bvsge ?e21 ?e10))
114(flet ($e109 (bvsle (zero_extend[3] ?e32) ?e5))
115(flet ($e110 (bvsle ?e7 (sign_extend[3] ?e38)))
116(flet ($e111 (bvugt ?e8 v3))
117(flet ($e112 (= ?e21 ?e49))
118(flet ($e113 (bvugt ?e34 (sign_extend[3] ?e27)))
119(flet ($e114 (bvugt (sign_extend[3] ?e50) v3))
120(flet ($e115 (= ?e25 ?e6))
121(flet ($e116 (distinct ?e13 (sign_extend[3] ?e27)))
122(flet ($e117 (bvugt ?e10 ?e7))
123(flet ($e118 (= ?e8 ?e58))
124(flet ($e119 (bvsgt ?e45 ?e42))
125(flet ($e120 (distinct ?e38 ?e53))
126(flet ($e121 (bvule (zero_extend[3] ?e50) ?e35))
127(flet ($e122 (distinct ?e51 ?e25))
128(flet ($e123 (bvslt v4 ?e44))
129(flet ($e124 (= ?e14 v0))
130(flet ($e125 (bvsge (zero_extend[1] ?e39) ?e33))
131(flet ($e126 (bvslt v0 (zero_extend[3] ?e57)))
132(flet ($e127 (bvsle ?e6 ?e36))
133(flet ($e128 (bvugt ?e13 (zero_extend[3] ?e28)))
134(flet ($e129 (bvsle ?e40 v1))
135(flet ($e130 (bvuge (sign_extend[3] ?e23) ?e44))
136(flet ($e131 (bvule (sign_extend[3] ?e56) ?e41))
137(flet ($e132 (bvule ?e20 ?e13))
138(flet ($e133 (bvult ?e6 (sign_extend[2] ?e15)))
139(flet ($e134 (bvugt ?e51 (zero_extend[3] ?e28)))
140(flet ($e135 (bvslt ?e10 (zero_extend[3] ?e57)))
141(flet ($e136 (= (zero_extend[3] ?e32) ?e14))
142(flet ($e137 (bvsge ?e29 ?e47))
143(flet ($e138 (= v3 ?e54))
144(flet ($e139 (= ?e60 ?e16))
145(flet ($e140 (bvsgt ?e24 ?e52))
146(flet ($e141 (bvuge v0 ?e34))
147(flet ($e142 (distinct v1 ?e34))
148(flet ($e143 (bvugt ?e61 v2))
149(flet ($e144 (bvsgt ?e33 (sign_extend[1] ?e27)))
150(flet ($e145 (bvsgt ?e55 ?e27))
151(flet ($e146 (bvsgt (zero_extend[3] ?e32) ?e61))
152(flet ($e147 (bvsgt ?e44 (zero_extend[3] ?e43)))
153(flet ($e148 (= ?e42 ?e45))
154(flet ($e149 (bvult ?e51 (zero_extend[3] ?e37)))
155(flet ($e150 (bvugt ?e31 ?e54))
156(flet ($e151 (bvsle ?e41 ?e22))
157(flet ($e152 (bvsge ?e20 ?e44))
158(flet ($e153 (bvsge (sign_extend[3] ?e50) ?e24))
159(flet ($e154 (distinct ?e45 ?e20))
160(flet ($e155 (= ?e29 (zero_extend[3] ?e30)))
161(flet ($e156 (bvslt ?e10 ?e44))
162(flet ($e157 (distinct ?e56 ?e30))
163(flet ($e158 (bvsle ?e17 ?e28))
164(flet ($e159 (bvuge ?e60 ?e44))
165(flet ($e160 (bvule ?e42 ?e24))
166(flet ($e161 (distinct ?e25 (sign_extend[3] ?e55)))
167(flet ($e162 (bvslt (sign_extend[3] ?e37) ?e21))
168(flet ($e163 (distinct ?e5 (sign_extend[3] ?e27)))
169(flet ($e164 (bvule ?e25 v1))
170(flet ($e165 (= v0 ?e60))
171(flet ($e166 (bvuge (sign_extend[3] ?e50) ?e26))
172(flet ($e167 (bvslt ?e58 ?e48))
173(flet ($e168 (bvsgt (sign_extend[3] ?e23) ?e42))
174(flet ($e169 (= ?e46 ?e34))
175(flet ($e170 (bvsgt ?e7 ?e20))
176(flet ($e171 (bvule ?e31 ?e12))
177(flet ($e172 (distinct ?e60 ?e18))
178(flet ($e173 (bvslt (sign_extend[3] ?e27) ?e40))
179(flet ($e174 (bvsge ?e42 ?e49))
180(flet ($e175 (bvugt ?e26 ?e11))
181(flet ($e176 (bvsgt ?e20 ?e35))
182(flet ($e177 (bvult ?e19 ?e19))
183(flet ($e178 (= ?e25 ?e10))
184(flet ($e179 (bvule (sign_extend[3] ?e23) ?e45))
185(flet ($e180 (bvslt v2 v3))
186(flet ($e181 (bvsgt ?e42 ?e42))
187(flet ($e182 (bvugt ?e58 ?e54))
188(flet ($e183 (bvsle ?e61 (zero_extend[3] ?e37)))
189(flet ($e184 (bvslt ?e60 (zero_extend[3] ?e57)))
190(flet ($e185 (distinct ?e21 (zero_extend[3] ?e27)))
191(flet ($e186 (bvule ?e58 v0))
192(flet ($e187 (= (sign_extend[3] ?e43) ?e13))
193(flet ($e188 (bvsge ?e52 (zero_extend[3] ?e50)))
194(flet ($e189 (bvsle ?e10 ?e51))
195(flet ($e190 (= ?e52 ?e29))
196(flet ($e191 (= ?e49 ?e25))
197(flet ($e192 (bvslt ?e60 ?e46))
198(flet ($e193 (bvugt ?e12 (zero_extend[2] ?e33)))
199(flet ($e194 (bvult ?e37 ?e28))
200(flet ($e195 (bvslt ?e20 (sign_extend[3] ?e30)))
201(flet ($e196 (bvult ?e8 ?e7))
202(flet ($e197 (bvsge ?e53 ?e37))
203(flet ($e198 (bvule ?e56 ?e50))
204(flet ($e199 (bvuge ?e11 ?e12))
205(flet ($e200 (bvsgt ?e24 ?e51))
206(flet ($e201 (bvsle (zero_extend[3] ?e59) ?e40))
207(flet ($e202 (bvule ?e21 ?e47))
208(flet ($e203 (bvsge ?e60 ?e11))
209(flet ($e204 (bvuge (zero_extend[3] ?e38) ?e29))
210(flet ($e205 (distinct ?e58 (sign_extend[3] ?e38)))
211(flet ($e206 (bvuge ?e11 (zero_extend[2] ?e33)))
212(flet ($e207 (bvult ?e42 ?e11))
213(flet ($e208 (distinct ?e10 ?e26))
214(flet ($e209 (bvult ?e5 ?e54))
215(flet ($e210 (bvsgt ?e21 v2))
216(flet ($e211 (bvsgt ?e49 ?e34))
217(flet ($e212 (bvuge ?e29 (zero_extend[3] ?e23)))
218(flet ($e213 (bvult ?e45 ?e35))
219(flet ($e214 (bvult ?e45 (sign_extend[3] ?e50)))
220(flet ($e215 (bvsle ?e19 ?e18))
221(flet ($e216 (= ?e9 ?e52))
222(flet ($e217
223(and
224 (or (not $e88) $e135 $e139)
225 (or $e160 (not $e134) $e82)
226 (or (not $e215) $e85 (not $e71))
227 (or $e121 (not $e131) $e147)
228 (or $e101 (not $e188) (not $e174))
229 (or $e158 $e68 (not $e167))
230 (or $e90 $e63 $e138)
231 (or $e169 $e131 $e121)
232 (or $e185 (not $e109) (not $e169))
233 (or (not $e204) (not $e197) (not $e75))
234 (or (not $e209) (not $e165) (not $e94))
235 (or (not $e182) $e189 $e142)
236 (or $e160 (not $e202) (not $e172))
237 (or $e164 $e187 $e148)
238 (or $e155 (not $e166) $e118)
239 (or (not $e102) (not $e113) $e109)
240 (or (not $e160) (not $e196) (not $e213))
241 (or $e116 $e128 (not $e80))
242 (or (not $e111) (not $e163) (not $e159))
243 (or (not $e80) $e118 $e197)
244 (or (not $e149) (not $e121) $e72)
245 (or $e64 (not $e173) $e126)
246 (or (not $e140) (not $e189) $e95)
247 (or $e98 $e78 (not $e207))
248 (or (not $e115) $e117 $e123)
249 (or (not $e112) $e204 $e193)
250 (or (not $e158) $e190 (not $e103))
251 (or $e63 $e178 $e213)
252 (or $e134 (not $e215) $e101)
253 (or $e132 $e116 $e72)
254 (or (not $e63) (not $e174) $e161)
255 (or (not $e90) (not $e120) (not $e145))
256 (or (not $e147) (not $e201) (not $e195))
257 (or (not $e157) (not $e90) $e187)
258 (or $e205 (not $e164) $e104)
259 (or $e100 $e178 $e96)
260 (or (not $e62) (not $e134) $e152)
261 (or (not $e87) (not $e146) $e150)
262 (or $e80 (not $e183) $e147)
263 (or (not $e215) (not $e110) $e193)
264 (or $e182 (not $e152) (not $e164))
265 (or (not $e93) (not $e67) (not $e82))
266 (or (not $e95) (not $e172) $e115)
267 (or (not $e216) (not $e120) (not $e92))
268 (or (not $e82) (not $e80) $e164)
269 (or $e159 (not $e208) (not $e194))
270 (or $e159 (not $e134) (not $e185))
271 (or (not $e115) (not $e119) (not $e209))
272 (or $e200 $e126 (not $e127))
273 (or $e82 $e71 $e157)
274 (or (not $e75) (not $e163) (not $e117))
275 (or $e134 $e117 $e197)
276 (or $e64 $e80 (not $e171))
277 (or (not $e197) (not $e108) (not $e156))
278 (or $e124 (not $e171) (not $e183))
279 (or (not $e159) $e110 (not $e215))
280 (or $e195 $e203 $e79)
281 (or (not $e147) $e107 $e163)
282 (or $e67 $e170 (not $e215))
283 (or (not $e94) (not $e127) (not $e124))
284 (or (not $e125) (not $e192) $e87)
285 (or $e139 (not $e86) $e88)
286 (or (not $e164) (not $e76) (not $e116))
287 (or $e120 $e116 $e180)
288 (or (not $e165) (not $e175) $e76)
289 (or (not $e117) (not $e187) (not $e159))
290 (or $e122 (not $e69) (not $e127))
291 (or $e142 $e123 $e103)
292 (or (not $e178) (not $e155) $e73)
293 (or $e139 (not $e202) $e170)
294 (or $e103 $e205 (not $e136))
295 (or (not $e86) $e115 $e87)
296 (or (not $e205) (not $e173) $e65)
297 (or (not $e67) $e69 (not $e93))
298 (or (not $e98) $e159 $e121)
299 (or (not $e136) $e132 $e90)
300 (or (not $e105) (not $e103) $e212)
301))
302$e217
303))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
304
305