diff options
Diffstat (limited to 'test/regress/regress0/bv/fuzz36.smt')
| -rw-r--r-- | test/regress/regress0/bv/fuzz36.smt | 274 |
1 files changed, 274 insertions, 0 deletions
diff --git a/test/regress/regress0/bv/fuzz36.smt b/test/regress/regress0/bv/fuzz36.smt new file mode 100644 index 000000000..96924c4a3 --- /dev/null +++ b/test/regress/regress0/bv/fuzz36.smt @@ -0,0 +1,274 @@ +(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 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 +)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + |