diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-11 13:54:42 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-11 13:54:42 +0000 |
commit | aabd0696722250f02e878943f534fd41c49ef5dd (patch) | |
tree | 0f14706b1c254aa8fd8fa9b888507ab9816a95d3 /test/regress/regress0/bv/fuzz28.smt | |
parent | 022a5e927ecab4f217b3f26529b09e569bd35d94 (diff) |
failing bv examples
Diffstat (limited to 'test/regress/regress0/bv/fuzz28.smt')
-rw-r--r-- | test/regress/regress0/bv/fuzz28.smt | 363 |
1 files changed, 363 insertions, 0 deletions
diff --git a/test/regress/regress0/bv/fuzz28.smt b/test/regress/regress0/bv/fuzz28.smt new file mode 100644 index 000000000..2c7a71a0f --- /dev/null +++ b/test/regress/regress0/bv/fuzz28.smt @@ -0,0 +1,363 @@ +(benchmark fuzzsmt +:logic QF_BV +:status unknown +: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 +)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + |