diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2019-09-06 15:28:07 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-09-06 15:28:07 -0700 |
commit | 91a5055015a97935d19b3dbf18062e189268a1f9 (patch) | |
tree | fb1fd19d80fb89d71286b462927540c0648d7551 /test/regress/regress0/bv/fuzz20.smt | |
parent | 7fc142a10140bba5a732237e3adf8fe6729d90e7 (diff) |
Remove SMT1 parser. (#3228)
This commit removes the SMT1 parser infrastructure and adds the SMT2 translations of the SMT1 regression tests. For now this commit removes regression test regress3/pp-regfile.smt since the SMT2 translation has a file size of 887M (vs. 172K for the SMT1 version).
Fixes #2948 and fixes #1313.
Diffstat (limited to 'test/regress/regress0/bv/fuzz20.smt')
-rw-r--r-- | test/regress/regress0/bv/fuzz20.smt | 191 |
1 files changed, 0 insertions, 191 deletions
diff --git a/test/regress/regress0/bv/fuzz20.smt b/test/regress/regress0/bv/fuzz20.smt deleted file mode 100644 index b7b493c82..000000000 --- a/test/regress/regress0/bv/fuzz20.smt +++ /dev/null @@ -1,191 +0,0 @@ -(benchmark fuzzsmt -:logic QF_BV -:status unsat -:extrafuns ((v0 BitVec[4])) -:extrafuns ((v1 BitVec[4])) -:extrafuns ((v2 BitVec[4])) -:formula -(let (?e3 bv2[4]) -(let (?e4 bv6[4]) -(let (?e5 bv8[4]) -(let (?e6 bv7[4]) -(let (?e7 bv3[4]) -(let (?e8 (bvmul v2 v2)) -(let (?e9 (bvnand ?e3 v0)) -(let (?e10 (bvnot v0)) -(let (?e11 (bvor ?e6 v1)) -(let (?e12 (zero_extend[0] v1)) -(let (?e13 (bvor v2 v0)) -(let (?e14 (bvlshr v2 ?e11)) -(let (?e15 (rotate_right[0] ?e8)) -(let (?e16 (ite (distinct ?e14 ?e15) bv1[1] bv0[1])) -(let (?e17 (bvnor ?e11 (sign_extend[3] ?e16))) -(let (?e18 (bvshl ?e3 ?e15)) -(let (?e19 (bvashr ?e9 ?e5)) -(let (?e20 (ite (bvule ?e3 ?e12) bv1[1] bv0[1])) -(let (?e21 (bvnot ?e16)) -(let (?e22 (bvadd ?e8 ?e15)) -(let (?e23 (ite (bvsgt ?e12 ?e9) bv1[1] bv0[1])) -(let (?e24 (zero_extend[0] v1)) -(let (?e25 (bvxor ?e14 v1)) -(let (?e26 (ite (bvsle ?e8 ?e25) bv1[1] bv0[1])) -(let (?e27 (bvashr (sign_extend[3] ?e26) v0)) -(let (?e28 (rotate_right[1] ?e27)) -(let (?e29 (bvashr ?e22 ?e22)) -(let (?e30 (bvadd ?e3 ?e28)) -(let (?e31 (bvneg ?e27)) -(let (?e32 (ite (distinct ?e5 ?e5) bv1[1] bv0[1])) -(let (?e33 (ite (bvslt (zero_extend[3] ?e16) ?e30) bv1[1] bv0[1])) -(let (?e34 (rotate_left[0] ?e21)) -(let (?e35 (bvmul ?e9 ?e11)) -(let (?e36 (ite (distinct ?e18 ?e27) bv1[1] bv0[1])) -(let (?e37 (bvand (zero_extend[3] ?e20) v0)) -(let (?e38 (rotate_left[1] ?e8)) -(let (?e39 (repeat[1] ?e22)) -(let (?e40 (ite (distinct ?e5 ?e17) bv1[1] bv0[1])) -(let (?e41 (bvxnor (sign_extend[3] ?e40) v0)) -(let (?e42 (bvor v0 ?e7)) -(let (?e43 (ite (bvsgt ?e24 ?e15) bv1[1] bv0[1])) -(let (?e44 (bvnot ?e33)) -(let (?e45 (bvsub ?e24 ?e11)) -(let (?e46 (bvsub ?e26 ?e44)) -(let (?e47 (bvneg ?e29)) -(let (?e48 (ite (bvsgt ?e37 ?e7) bv1[1] bv0[1])) -(let (?e49 (bvlshr ?e29 ?e14)) -(let (?e50 (ite (bvsgt ?e18 ?e4) bv1[1] bv0[1])) -(flet ($e51 (bvsle ?e20 ?e21)) -(flet ($e52 (bvsle ?e3 ?e41)) -(flet ($e53 (bvult ?e39 ?e39)) -(flet ($e54 (bvsgt (sign_extend[3] ?e32) ?e35)) -(flet ($e55 (= (zero_extend[3] ?e20) ?e18)) -(flet ($e56 (bvugt ?e41 ?e6)) -(flet ($e57 (bvsge ?e41 ?e38)) -(flet ($e58 (bvugt ?e5 ?e25)) -(flet ($e59 (bvult ?e12 ?e30)) -(flet ($e60 (bvslt ?e11 ?e8)) -(flet ($e61 (bvugt ?e35 ?e15)) -(flet ($e62 (bvugt ?e47 ?e17)) -(flet ($e63 (= ?e17 (zero_extend[3] ?e33))) -(flet ($e64 (bvsge (sign_extend[3] ?e43) v0)) -(flet ($e65 (bvugt ?e6 ?e5)) -(flet ($e66 (bvugt (sign_extend[3] ?e43) ?e30)) -(flet ($e67 (bvsgt (sign_extend[3] ?e34) ?e22)) -(flet ($e68 (= ?e13 ?e12)) -(flet ($e69 (bvslt ?e45 ?e4)) -(flet ($e70 (distinct ?e19 (sign_extend[3] ?e50))) -(flet ($e71 (distinct ?e47 v0)) -(flet ($e72 (bvsgt ?e8 (sign_extend[3] ?e36))) -(flet ($e73 (bvule ?e25 ?e8)) -(flet ($e74 (bvsgt ?e10 ?e3)) -(flet ($e75 (distinct ?e31 ?e10)) -(flet ($e76 (= ?e29 ?e8)) -(flet ($e77 (= v0 (zero_extend[3] ?e21))) -(flet ($e78 (bvsgt ?e49 v1)) -(flet ($e79 (bvsgt ?e19 ?e35)) -(flet ($e80 (bvule ?e16 ?e21)) -(flet ($e81 (bvslt ?e14 ?e10)) -(flet ($e82 (distinct ?e35 ?e14)) -(flet ($e83 (= ?e25 ?e3)) -(flet ($e84 (distinct ?e29 (zero_extend[3] ?e20))) -(flet ($e85 (bvult ?e22 (zero_extend[3] ?e23))) -(flet ($e86 (bvugt ?e23 ?e16)) -(flet ($e87 (bvult (sign_extend[3] ?e34) ?e35)) -(flet ($e88 (bvule ?e29 (zero_extend[3] ?e46))) -(flet ($e89 (bvsgt ?e13 (sign_extend[3] ?e32))) -(flet ($e90 (bvugt ?e42 ?e31)) -(flet ($e91 (bvuge ?e47 (zero_extend[3] ?e34))) -(flet ($e92 (distinct ?e42 ?e28)) -(flet ($e93 (= ?e44 ?e20)) -(flet ($e94 (bvsle ?e35 (zero_extend[3] ?e34))) -(flet ($e95 (bvule ?e42 ?e12)) -(flet ($e96 (bvsgt (zero_extend[3] ?e23) v1)) -(flet ($e97 (bvule v2 (sign_extend[3] ?e16))) -(flet ($e98 (bvuge (sign_extend[3] ?e43) ?e37)) -(flet ($e99 (bvult ?e28 ?e3)) -(flet ($e100 (bvugt ?e19 (zero_extend[3] ?e26))) -(flet ($e101 (= ?e27 ?e7)) -(flet ($e102 (bvsge ?e18 ?e14)) -(flet ($e103 (bvsgt ?e31 ?e18)) -(flet ($e104 (= (zero_extend[3] ?e50) ?e9)) -(flet ($e105 (bvult ?e39 v0)) -(flet ($e106 (distinct ?e19 v1)) -(flet ($e107 (bvsle ?e4 ?e4)) -(flet ($e108 (= ?e26 ?e46)) -(flet ($e109 (bvsle ?e35 ?e3)) -(flet ($e110 (bvuge ?e10 ?e14)) -(flet ($e111 (distinct ?e5 (zero_extend[3] ?e44))) -(flet ($e112 (bvule v1 ?e27)) -(flet ($e113 (bvugt ?e41 (zero_extend[3] ?e23))) -(flet ($e114 (bvule (sign_extend[3] ?e33) ?e11)) -(flet ($e115 (bvugt ?e48 ?e34)) -(flet ($e116 (= ?e47 ?e45)) -(flet ($e117 (bvugt ?e12 v0)) -(flet ($e118 (bvslt ?e41 ?e5)) -(flet ($e119 (bvsge (sign_extend[3] ?e21) ?e38)) -(flet ($e120 (bvugt ?e42 ?e47)) -(flet ($e121 (bvslt ?e18 (zero_extend[3] ?e16))) -(flet ($e122 (bvsge ?e4 ?e45)) -(flet ($e123 (bvslt ?e37 (sign_extend[3] ?e48))) -(flet ($e124 (bvugt ?e28 (zero_extend[3] ?e21))) -(flet ($e125 (bvuge ?e30 ?e19)) -(flet ($e126 (bvsgt ?e35 ?e22)) -(flet ($e127 (bvuge (zero_extend[3] ?e34) ?e13)) -(flet ($e128 (bvsgt ?e5 ?e3)) -(flet ($e129 (bvslt ?e24 (zero_extend[3] ?e44))) -(flet ($e130 (bvule ?e48 ?e33)) -(flet ($e131 (distinct ?e10 (zero_extend[3] ?e50))) -(flet ($e132 (bvsle (sign_extend[3] ?e32) ?e28)) -(flet ($e133 (bvugt ?e3 v1)) -(flet ($e134 (= (sign_extend[3] ?e33) ?e42)) -(flet ($e135 (distinct ?e21 ?e46)) -(flet ($e136 (bvsle ?e15 ?e41)) -(flet ($e137 (bvsle (sign_extend[3] ?e40) v2)) -(flet ($e138 -(and - (or (not $e65) (not $e121) $e55) - (or $e98 $e77 (not $e80)) - (or (not $e135) $e133 $e66) - (or (not $e74) (not $e104) (not $e66)) - (or (not $e120) (not $e65) $e125) - (or (not $e117) $e132 $e129) - (or $e76 (not $e106) (not $e55)) - (or $e128 (not $e79) $e83) - (or $e80 (not $e96) (not $e107)) - (or (not $e72) $e70 (not $e79)) - (or $e114 $e118 (not $e94)) - (or $e54 (not $e128) $e78) - (or $e79 $e79 $e126) - (or $e116 $e69 (not $e52)) - (or $e111 $e99 $e62) - (or $e108 (not $e126) $e131) - (or $e71 $e96 (not $e121)) - (or (not $e70) (not $e60) $e89) - (or (not $e57) $e128 (not $e73)) - (or (not $e118) (not $e59) (not $e81)) - (or $e112 (not $e102) $e91) - (or (not $e66) (not $e74) (not $e63)) - (or $e134 (not $e111) (not $e134)) - (or (not $e126) (not $e70) $e137) - (or $e76 $e124 $e74) - (or (not $e108) $e96 $e65) - (or $e122 (not $e92) $e59) - (or (not $e107) (not $e136) (not $e123)) - (or (not $e76) (not $e53) (not $e118)) - (or (not $e105) (not $e121) $e85) - (or (not $e99) $e102 $e106) - (or (not $e61) $e121 $e90) - (or (not $e53) (not $e77) (not $e54)) - (or (not $e72) $e76 (not $e114)) - (or (not $e104) $e101 (not $e105)) - (or $e128 (not $e129) $e84) - (or (not $e95) (not $e128) (not $e130)) - (or (not $e90) $e129 $e133) - (or $e131 $e72 (not $e82)) - (or $e128 (not $e113) (not $e120)) - (or (not $e80) (not $e87) (not $e59)) - (or $e57 $e123 $e118) - (or (not $e109) $e73 $e81) -)) -$e138 -))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) - |