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/fuzz25.smt | |
parent | 022a5e927ecab4f217b3f26529b09e569bd35d94 (diff) |
failing bv examples
Diffstat (limited to 'test/regress/regress0/bv/fuzz25.smt')
-rw-r--r-- | test/regress/regress0/bv/fuzz25.smt | 356 |
1 files changed, 356 insertions, 0 deletions
diff --git a/test/regress/regress0/bv/fuzz25.smt b/test/regress/regress0/bv/fuzz25.smt new file mode 100644 index 000000000..1193a62e1 --- /dev/null +++ b/test/regress/regress0/bv/fuzz25.smt @@ -0,0 +1,356 @@ +(benchmark fuzzsmt +:logic QF_BV +:status unknown +: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 +)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + |