diff options
Diffstat (limited to 'test/regress/regress0/bv/fuzz28.smt')
-rw-r--r-- | test/regress/regress0/bv/fuzz28.smt | 363 |
1 files changed, 0 insertions, 363 deletions
diff --git a/test/regress/regress0/bv/fuzz28.smt b/test/regress/regress0/bv/fuzz28.smt deleted file mode 100644 index 732017750..000000000 --- a/test/regress/regress0/bv/fuzz28.smt +++ /dev/null @@ -1,363 +0,0 @@ -(benchmark fuzzsmt -:logic QF_BV -:status unsat -:extrafuns ((v0 BitVec[4])) -:extrafuns ((v1 BitVec[4])) -:extrafuns ((v2 BitVec[4])) -:extrafuns ((v3 BitVec[4])) -:formula -(let (?e4 bv12[4]) -(let (?e5 bv14[4]) -(let (?e6 bv5[4]) -(let (?e7 bv6[4]) -(let (?e8 bv13[4]) -(let (?e9 (bvneg v0)) -(let (?e10 (rotate_left[0] v0)) -(let (?e11 (bvxnor v3 ?e6)) -(let (?e12 (bvnot v0)) -(let (?e13 (bvnand v0 ?e10)) -(let (?e14 (ite (bvslt v0 ?e4) bv1[1] bv0[1])) -(let (?e15 (bvnand ?e6 ?e11)) -(let (?e16 (bvadd ?e13 ?e11)) -(let (?e17 (bvadd ?e12 ?e8)) -(let (?e18 (bvcomp ?e10 ?e15)) -(let (?e19 (ite (bvsgt ?e8 ?e5) bv1[1] bv0[1])) -(let (?e20 (ite (bvugt (sign_extend[3] ?e19) ?e15) bv1[1] bv0[1])) -(let (?e21 (bvxor v2 (sign_extend[3] ?e18))) -(let (?e22 (bvadd ?e13 (zero_extend[3] ?e18))) -(let (?e23 (ite (= ?e10 ?e13) bv1[1] bv0[1])) -(let (?e24 (ite (bvslt ?e9 (sign_extend[3] ?e23)) bv1[1] bv0[1])) -(let (?e25 (ite (bvsgt ?e8 (sign_extend[3] ?e24)) bv1[1] bv0[1])) -(let (?e26 (bvxnor ?e8 (zero_extend[3] ?e14))) -(let (?e27 (zero_extend[0] ?e25)) -(let (?e28 (extract[0:0] ?e15)) -(let (?e29 (ite (= (zero_extend[3] ?e19) ?e22) bv1[1] bv0[1])) -(let (?e30 (rotate_right[1] ?e9)) -(let (?e31 (bvmul ?e10 v0)) -(let (?e32 (bvmul (zero_extend[3] ?e20) ?e10)) -(let (?e33 (bvshl ?e6 (sign_extend[3] ?e29))) -(let (?e34 (ite (bvuge ?e15 (zero_extend[3] ?e28)) bv1[1] bv0[1])) -(let (?e35 (bvmul (sign_extend[3] ?e18) ?e16)) -(let (?e36 (rotate_left[0] ?e22)) -(let (?e37 (bvshl v3 ?e15)) -(let (?e38 (ite (bvsgt ?e30 ?e8) bv1[1] bv0[1])) -(let (?e39 (bvadd ?e30 (sign_extend[3] ?e27))) -(let (?e40 (ite (bvsle v1 ?e15) bv1[1] bv0[1])) -(let (?e41 (bvlshr ?e8 (zero_extend[3] ?e14))) -(let (?e42 (ite (bvsgt ?e32 ?e22) bv1[1] bv0[1])) -(let (?e43 (rotate_right[1] ?e31)) -(let (?e44 (ite (bvsge (sign_extend[3] ?e19) ?e10) bv1[1] bv0[1])) -(let (?e45 (bvxor ?e12 ?e39)) -(let (?e46 (ite (= (zero_extend[3] ?e19) ?e4) bv1[1] bv0[1])) -(let (?e47 (zero_extend[3] ?e18)) -(let (?e48 (zero_extend[2] ?e20)) -(let (?e49 (ite (bvslt ?e16 (zero_extend[3] ?e18)) bv1[1] bv0[1])) -(let (?e50 (bvnand ?e25 ?e29)) -(let (?e51 (ite (= ?e15 ?e9) bv1[1] bv0[1])) -(let (?e52 (bvcomp ?e12 ?e6)) -(let (?e53 (concat ?e51 ?e42)) -(let (?e54 (bvnand ?e27 ?e29)) -(let (?e55 (bvnor ?e26 ?e39)) -(let (?e56 (bvand (sign_extend[3] ?e46) ?e41)) -(let (?e57 (bvnor ?e4 ?e36)) -(let (?e58 (repeat[2] ?e44)) -(let (?e59 (ite (bvslt (sign_extend[3] ?e46) ?e17) bv1[1] bv0[1])) -(let (?e60 (bvxnor (sign_extend[3] ?e20) ?e21)) -(let (?e61 (bvxnor v0 ?e35)) -(let (?e62 (bvnor ?e6 ?e60)) -(let (?e63 (ite (bvugt ?e29 ?e28) bv1[1] bv0[1])) -(let (?e64 (ite (bvule ?e23 ?e49) bv1[1] bv0[1])) -(let (?e65 (bvnot ?e23)) -(let (?e66 (repeat[1] ?e5)) -(let (?e67 (rotate_left[1] ?e17)) -(let (?e68 (ite (bvsle ?e56 ?e61) bv1[1] bv0[1])) -(let (?e69 (sign_extend[0] ?e6)) -(let (?e70 (ite (bvslt ?e31 (sign_extend[3] ?e44)) bv1[1] bv0[1])) -(let (?e71 (ite (= bv1[1] (extract[0:0] ?e17)) (zero_extend[3] ?e18) ?e41)) -(let (?e72 (bvor (zero_extend[3] ?e28) ?e12)) -(let (?e73 (bvashr ?e8 (sign_extend[3] ?e23))) -(let (?e74 (extract[0:0] ?e70)) -(let (?e75 (bvnor ?e67 ?e62)) -(let (?e76 (zero_extend[0] ?e61)) -(let (?e77 (bvlshr ?e51 ?e54)) -(let (?e78 (bvand ?e7 ?e8)) -(flet ($e79 (bvule ?e19 ?e59)) -(flet ($e80 (= ?e30 (zero_extend[3] ?e19))) -(flet ($e81 (bvult ?e28 ?e38)) -(flet ($e82 (bvslt ?e7 ?e31)) -(flet ($e83 (bvsgt ?e47 (sign_extend[3] ?e29))) -(flet ($e84 (bvslt ?e30 (sign_extend[3] ?e18))) -(flet ($e85 (= (sign_extend[3] ?e46) ?e47)) -(flet ($e86 (distinct ?e61 ?e36)) -(flet ($e87 (bvsge v3 (sign_extend[3] ?e52))) -(flet ($e88 (bvslt ?e56 ?e75)) -(flet ($e89 (bvult ?e52 ?e14)) -(flet ($e90 (bvslt ?e12 (sign_extend[3] ?e29))) -(flet ($e91 (bvslt ?e66 ?e76)) -(flet ($e92 (bvult ?e37 ?e36)) -(flet ($e93 (bvsgt ?e73 ?e69)) -(flet ($e94 (bvslt ?e33 (zero_extend[3] ?e64))) -(flet ($e95 (distinct ?e75 (sign_extend[3] ?e54))) -(flet ($e96 (bvsge ?e30 ?e75)) -(flet ($e97 (bvult (zero_extend[3] ?e25) ?e15)) -(flet ($e98 (bvsle (zero_extend[3] ?e40) v1)) -(flet ($e99 (bvsgt ?e32 ?e16)) -(flet ($e100 (bvuge (sign_extend[1] ?e54) ?e58)) -(flet ($e101 (bvuge ?e61 ?e41)) -(flet ($e102 (bvsle ?e4 ?e10)) -(flet ($e103 (bvsge ?e60 (zero_extend[1] ?e48))) -(flet ($e104 (bvugt ?e73 ?e17)) -(flet ($e105 (bvugt ?e12 (sign_extend[3] ?e18))) -(flet ($e106 (bvslt ?e11 ?e11)) -(flet ($e107 (bvugt (sign_extend[2] ?e58) v3)) -(flet ($e108 (bvuge (sign_extend[1] ?e48) ?e66)) -(flet ($e109 (distinct ?e30 ?e17)) -(flet ($e110 (bvslt ?e33 ?e43)) -(flet ($e111 (bvule ?e63 ?e25)) -(flet ($e112 (= ?e35 ?e30)) -(flet ($e113 (bvsgt ?e16 ?e33)) -(flet ($e114 (= (zero_extend[3] ?e34) ?e26)) -(flet ($e115 (distinct v0 (sign_extend[3] ?e28))) -(flet ($e116 (bvsge (zero_extend[3] ?e18) ?e6)) -(flet ($e117 (= ?e15 ?e31)) -(flet ($e118 (bvult (zero_extend[1] ?e40) ?e53)) -(flet ($e119 (distinct (sign_extend[3] ?e28) ?e30)) -(flet ($e120 (bvsge ?e16 v1)) -(flet ($e121 (bvsge (sign_extend[3] ?e19) ?e78)) -(flet ($e122 (bvule ?e59 ?e38)) -(flet ($e123 (bvugt ?e73 v2)) -(flet ($e124 (distinct ?e75 (sign_extend[3] ?e27))) -(flet ($e125 (bvslt (zero_extend[1] ?e59) ?e58)) -(flet ($e126 (bvsge ?e12 ?e21)) -(flet ($e127 (= ?e41 ?e12)) -(flet ($e128 (bvugt ?e56 v1)) -(flet ($e129 (bvsgt (zero_extend[3] ?e50) ?e45)) -(flet ($e130 (= (sign_extend[2] ?e58) ?e57)) -(flet ($e131 (bvugt ?e73 ?e10)) -(flet ($e132 (bvult ?e4 ?e47)) -(flet ($e133 (= (sign_extend[3] ?e68) ?e60)) -(flet ($e134 (bvugt (sign_extend[3] ?e74) ?e33)) -(flet ($e135 (bvult (sign_extend[3] ?e68) ?e47)) -(flet ($e136 (bvslt ?e49 ?e63)) -(flet ($e137 (bvugt ?e45 ?e13)) -(flet ($e138 (bvugt ?e51 ?e19)) -(flet ($e139 (bvslt ?e30 (sign_extend[3] ?e68))) -(flet ($e140 (distinct (zero_extend[3] ?e52) v1)) -(flet ($e141 (= ?e17 ?e60)) -(flet ($e142 (bvuge ?e40 ?e77)) -(flet ($e143 (bvsge (sign_extend[3] ?e18) ?e5)) -(flet ($e144 (bvult ?e35 (sign_extend[3] ?e27))) -(flet ($e145 (bvsgt ?e60 (zero_extend[3] ?e14))) -(flet ($e146 (bvsle ?e26 (zero_extend[3] ?e27))) -(flet ($e147 (bvule ?e72 ?e57)) -(flet ($e148 (= ?e41 (sign_extend[3] ?e59))) -(flet ($e149 (bvuge (sign_extend[3] ?e52) ?e45)) -(flet ($e150 (bvule (sign_extend[3] ?e70) v2)) -(flet ($e151 (bvslt v1 (sign_extend[3] ?e49))) -(flet ($e152 (distinct ?e22 (sign_extend[1] ?e48))) -(flet ($e153 (distinct v1 ?e15)) -(flet ($e154 (bvuge ?e5 ?e62)) -(flet ($e155 (= ?e12 v3)) -(flet ($e156 (bvsge (zero_extend[3] ?e68) ?e62)) -(flet ($e157 (bvuge ?e76 (zero_extend[3] ?e65))) -(flet ($e158 (= ?e26 ?e55)) -(flet ($e159 (bvsgt (zero_extend[3] ?e54) ?e72)) -(flet ($e160 (bvsle (sign_extend[3] ?e29) ?e41)) -(flet ($e161 (= (zero_extend[3] ?e18) v1)) -(flet ($e162 (bvsle ?e8 (sign_extend[3] ?e46))) -(flet ($e163 (bvule ?e21 (zero_extend[3] ?e65))) -(flet ($e164 (bvuge ?e36 (zero_extend[3] ?e64))) -(flet ($e165 (= (zero_extend[3] ?e18) ?e43)) -(flet ($e166 (bvugt v0 (sign_extend[3] ?e70))) -(flet ($e167 (bvslt (sign_extend[3] ?e24) ?e60)) -(flet ($e168 (bvsgt ?e10 (sign_extend[2] ?e53))) -(flet ($e169 (bvugt ?e70 ?e70)) -(flet ($e170 (bvuge (sign_extend[3] ?e34) ?e43)) -(flet ($e171 (bvult ?e65 ?e19)) -(flet ($e172 (bvult ?e71 ?e17)) -(flet ($e173 (= ?e7 (zero_extend[3] ?e64))) -(flet ($e174 (bvslt v0 ?e78)) -(flet ($e175 (bvsge ?e60 ?e78)) -(flet ($e176 (bvuge v2 ?e10)) -(flet ($e177 (bvsge ?e34 ?e40)) -(flet ($e178 (bvuge (sign_extend[3] ?e49) ?e17)) -(flet ($e179 (bvuge ?e71 (zero_extend[3] ?e14))) -(flet ($e180 (bvult ?e66 (sign_extend[3] ?e25))) -(flet ($e181 (bvsge (sign_extend[3] ?e23) v2)) -(flet ($e182 (bvsge ?e64 ?e65)) -(flet ($e183 (bvugt ?e72 ?e8)) -(flet ($e184 (bvule ?e70 ?e34)) -(flet ($e185 (distinct ?e25 ?e49)) -(flet ($e186 (bvsgt ?e41 (sign_extend[3] ?e40))) -(flet ($e187 (bvslt ?e26 (sign_extend[3] ?e42))) -(flet ($e188 (bvsgt ?e9 (sign_extend[3] ?e23))) -(flet ($e189 (distinct ?e56 ?e21)) -(flet ($e190 (bvugt ?e35 v2)) -(flet ($e191 (bvsle ?e61 ?e33)) -(flet ($e192 (bvsge (sign_extend[3] ?e46) ?e69)) -(flet ($e193 (= ?e27 ?e18)) -(flet ($e194 (bvsgt ?e75 (zero_extend[3] ?e52))) -(flet ($e195 (bvsgt ?e36 (sign_extend[3] ?e18))) -(flet ($e196 (bvsgt (zero_extend[3] ?e20) ?e15)) -(flet ($e197 (bvsge ?e78 ?e36)) -(flet ($e198 (= (sign_extend[3] ?e51) ?e4)) -(flet ($e199 (bvsge ?e47 ?e37)) -(flet ($e200 (bvsgt ?e5 (sign_extend[3] ?e51))) -(flet ($e201 (bvsgt ?e13 ?e75)) -(flet ($e202 (bvsle ?e15 ?e55)) -(flet ($e203 (bvsgt ?e47 ?e33)) -(flet ($e204 (bvsle (sign_extend[3] ?e28) v1)) -(flet ($e205 (bvsle (sign_extend[3] ?e77) ?e13)) -(flet ($e206 (bvsgt ?e48 (zero_extend[2] ?e46))) -(flet ($e207 (bvsgt (zero_extend[3] ?e52) ?e56)) -(flet ($e208 (bvule (zero_extend[3] ?e46) ?e21)) -(flet ($e209 (bvuge ?e9 (zero_extend[3] ?e40))) -(flet ($e210 (bvuge (sign_extend[3] ?e46) ?e26)) -(flet ($e211 (bvule (zero_extend[3] ?e40) ?e55)) -(flet ($e212 (distinct ?e12 v2)) -(flet ($e213 (distinct v2 ?e4)) -(flet ($e214 (bvslt ?e63 ?e65)) -(flet ($e215 (bvsge ?e28 ?e77)) -(flet ($e216 (bvsle (zero_extend[3] ?e70) ?e11)) -(flet ($e217 (bvult (sign_extend[3] ?e49) v0)) -(flet ($e218 (bvslt ?e76 ?e72)) -(flet ($e219 (bvuge ?e28 ?e14)) -(flet ($e220 (bvsgt ?e7 ?e7)) -(flet ($e221 (bvuge ?e53 (zero_extend[1] ?e28))) -(flet ($e222 (bvslt (zero_extend[3] ?e27) ?e33)) -(flet ($e223 (bvuge (sign_extend[3] ?e38) ?e57)) -(flet ($e224 (bvugt ?e44 ?e14)) -(flet ($e225 (bvugt ?e36 (sign_extend[3] ?e44))) -(flet ($e226 (bvugt ?e41 ?e41)) -(flet ($e227 (bvsge v2 ?e35)) -(flet ($e228 (distinct ?e9 v1)) -(flet ($e229 (bvuge ?e25 ?e42)) -(flet ($e230 (bvsgt (sign_extend[3] ?e40) ?e66)) -(flet ($e231 (bvule ?e24 ?e14)) -(flet ($e232 (bvsge ?e62 ?e37)) -(flet ($e233 (bvsge ?e47 ?e16)) -(flet ($e234 (bvugt ?e32 (sign_extend[3] ?e51))) -(flet ($e235 (bvule ?e6 ?e15)) -(flet ($e236 (bvuge ?e36 ?e57)) -(flet ($e237 (bvult ?e9 ?e16)) -(flet ($e238 (bvule ?e56 (zero_extend[3] ?e51))) -(flet ($e239 (bvsgt ?e15 (zero_extend[3] ?e23))) -(flet ($e240 (bvugt (zero_extend[3] ?e18) ?e21)) -(flet ($e241 (bvsge v3 (zero_extend[3] ?e40))) -(flet ($e242 (bvult ?e36 (zero_extend[3] ?e59))) -(flet ($e243 (bvugt ?e75 (zero_extend[1] ?e48))) -(flet ($e244 (bvult ?e21 ?e33)) -(flet ($e245 (= ?e32 v2)) -(flet ($e246 (bvsgt ?e21 ?e69)) -(flet ($e247 (bvsle ?e7 ?e37)) -(flet ($e248 (distinct (sign_extend[3] ?e64) ?e12)) -(flet ($e249 (distinct v0 (sign_extend[3] ?e27))) -(flet ($e250 (distinct (sign_extend[3] ?e42) ?e56)) -(flet ($e251 (bvult ?e56 ?e22)) -(flet ($e252 (bvslt ?e7 ?e6)) -(flet ($e253 (bvsle ?e31 ?e16)) -(flet ($e254 (bvslt v1 (zero_extend[3] ?e18))) -(flet ($e255 (bvuge ?e15 ?e30)) -(flet ($e256 (distinct ?e45 ?e11)) -(flet ($e257 (distinct ?e7 ?e66)) -(flet ($e258 (bvule ?e56 (zero_extend[1] ?e48))) -(flet ($e259 (bvugt ?e26 ?e55)) -(flet ($e260 (bvsle ?e39 (zero_extend[3] ?e14))) -(flet ($e261 (bvsgt ?e75 ?e67)) -(flet ($e262 -(and - (or (not $e246) $e254 $e237) - (or (not $e151) (not $e150) $e92) - (or (not $e177) (not $e178) (not $e205)) - (or $e82 (not $e127) $e187) - (or (not $e169) $e88 (not $e90)) - (or (not $e98) $e130 (not $e87)) - (or (not $e235) $e207 $e129) - (or (not $e163) (not $e207) $e109) - (or (not $e236) (not $e124) $e123) - (or (not $e194) $e261 $e178) - (or $e172 $e159 (not $e261)) - (or $e154 $e100 $e123) - (or (not $e195) $e213 $e194) - (or (not $e184) (not $e202) (not $e137)) - (or (not $e81) (not $e248) $e92) - (or $e119 $e189 $e223) - (or $e199 (not $e160) (not $e208)) - (or (not $e85) (not $e82) (not $e170)) - (or (not $e153) (not $e172) $e119) - (or (not $e182) $e151 (not $e257)) - (or (not $e243) $e224 (not $e192)) - (or (not $e79) (not $e152) (not $e100)) - (or (not $e178) $e158 $e195) - (or (not $e148) (not $e146) $e166) - (or $e235 (not $e152) (not $e255)) - (or (not $e177) (not $e237) (not $e138)) - (or $e210 (not $e191) (not $e95)) - (or $e138 $e260 (not $e232)) - (or $e180 (not $e112) (not $e96)) - (or (not $e223) (not $e215) $e137) - (or (not $e175) (not $e192) (not $e170)) - (or (not $e175) (not $e256) (not $e138)) - (or $e91 $e143 $e147) - (or $e253 $e206 $e217) - (or $e249 (not $e205) $e252) - (or $e153 $e212 $e151) - (or $e175 $e84 (not $e105)) - (or (not $e210) $e185 $e236) - (or (not $e83) $e248 $e165) - (or $e202 (not $e106) $e145) - (or (not $e129) (not $e153) (not $e235)) - (or $e253 (not $e122) (not $e174)) - (or $e191 (not $e209) (not $e235)) - (or $e256 $e216 (not $e142)) - (or $e237 (not $e132) $e81) - (or $e121 (not $e250) $e162) - (or $e175 (not $e133) (not $e82)) - (or $e217 (not $e90) (not $e220)) - (or $e210 $e188 (not $e124)) - (or (not $e153) (not $e110) $e229) - (or (not $e224) $e177 $e83) - (or (not $e233) $e170 (not $e233)) - (or (not $e152) $e241 $e178) - (or $e192 (not $e209) $e177) - (or $e191 $e143 (not $e117)) - (or (not $e133) $e91 (not $e120)) - (or (not $e227) (not $e217) $e197) - (or (not $e99) (not $e223) (not $e261)) - (or $e139 $e85 $e128) - (or $e219 (not $e156) (not $e208)) - (or (not $e112) (not $e219) $e235) - (or $e104 (not $e98) (not $e190)) - (or $e247 (not $e129) (not $e254)) - (or $e110 $e186 $e225) - (or $e215 $e170 $e135) - (or $e92 (not $e256) (not $e143)) - (or $e160 (not $e89) $e173) - (or $e238 (not $e188) (not $e144)) - (or $e164 (not $e247) (not $e87)) - (or $e83 $e251 (not $e169)) - (or (not $e149) (not $e166) $e97) - (or (not $e205) (not $e166) (not $e218)) - (or $e163 (not $e137) $e190) - (or (not $e151) (not $e207) (not $e144)) - (or (not $e110) $e84 (not $e82)) - (or $e211 (not $e105) (not $e117)) - (or $e233 $e218 (not $e188)) - (or $e165 $e197 $e235) - (or $e107 (not $e222) (not $e203)) - (or $e157 (not $e215) $e245) - (or $e140 $e151 (not $e255)) - (or $e126 $e192 (not $e225)) - (or (not $e257) (not $e143) $e213) - (or $e100 (not $e98) $e103) - (or (not $e173) $e132 $e113) - (or $e250 (not $e250) $e122) - (or $e201 $e119 $e230) - (or $e128 (not $e184) (not $e228)) - (or $e211 $e120 (not $e124)) - (or (not $e80) $e91 $e139) - (or $e205 (not $e220) $e91) -)) -$e262 -)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) - |