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