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