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