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