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