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/bug239.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/bug239.smt')
-rw-r--r-- | test/regress/regress0/bug239.smt | 185 |
1 files changed, 0 insertions, 185 deletions
diff --git a/test/regress/regress0/bug239.smt b/test/regress/regress0/bug239.smt deleted file mode 100644 index b80f56c44..000000000 --- a/test/regress/regress0/bug239.smt +++ /dev/null @@ -1,185 +0,0 @@ -(benchmark fuzzsmt -:logic QF_LRA -:status sat -:extrafuns ((v0 Real)) -:extrafuns ((v1 Real)) -:extrafuns ((v2 Real)) -:formula -(let (?e3 5) -(let (?e4 0) -(let (?e5 2) -(let (?e6 (+ v0 v1)) -(let (?e7 (* v1 ?e3)) -(let (?e8 (~ v0)) -(let (?e9 (- v2 v1)) -(let (?e10 (- v0 ?e9)) -(let (?e11 (* v0 (~ ?e3))) -(let (?e12 (/ ?e4 (~ ?e3))) -(let (?e13 (+ ?e8 ?e7)) -(let (?e14 (/ ?e4 (~ ?e5))) -(flet ($e15 (<= v2 ?e7)) -(flet ($e16 (<= ?e11 ?e11)) -(flet ($e17 (= ?e11 ?e13)) -(flet ($e18 (<= ?e7 ?e14)) -(flet ($e19 (> ?e14 v1)) -(flet ($e20 (< v0 ?e10)) -(flet ($e21 (= ?e8 ?e11)) -(flet ($e22 (>= ?e8 ?e13)) -(flet ($e23 (< ?e10 v2)) -(flet ($e24 (>= ?e10 ?e8)) -(flet ($e25 (= ?e6 ?e7)) -(flet ($e26 (distinct ?e12 ?e11)) -(flet ($e27 (distinct ?e10 ?e9)) -(let (?e28 (ite $e27 ?e13 ?e6)) -(let (?e29 (ite $e21 v2 ?e28)) -(let (?e30 (ite $e26 ?e12 ?e12)) -(let (?e31 (ite $e18 ?e28 v0)) -(let (?e32 (ite $e20 ?e9 ?e10)) -(let (?e33 (ite $e22 ?e11 ?e28)) -(let (?e34 (ite $e17 ?e8 ?e13)) -(let (?e35 (ite $e26 ?e14 v1)) -(let (?e36 (ite $e21 ?e14 ?e30)) -(let (?e37 (ite $e19 ?e7 ?e11)) -(let (?e38 (ite $e25 v1 ?e8)) -(let (?e39 (ite $e22 ?e28 ?e28)) -(let (?e40 (ite $e25 v0 ?e14)) -(let (?e41 (ite $e24 ?e37 v2)) -(let (?e42 (ite $e16 ?e6 v2)) -(let (?e43 (ite $e19 ?e11 ?e7)) -(let (?e44 (ite $e23 ?e36 v2)) -(let (?e45 (ite $e20 v1 ?e7)) -(let (?e46 (ite $e15 ?e45 ?e13)) -(flet ($e47 (= ?e32 ?e9)) -(flet ($e48 (< ?e41 v0)) -(flet ($e49 (distinct ?e14 ?e43)) -(flet ($e50 (distinct ?e8 ?e10)) -(flet ($e51 (> ?e8 ?e37)) -(flet ($e52 (< v1 ?e11)) -(flet ($e53 (< ?e30 ?e8)) -(flet ($e54 (< v2 ?e12)) -(flet ($e55 (>= ?e8 ?e31)) -(flet ($e56 (= ?e12 ?e44)) -(flet ($e57 (= ?e45 v0)) -(flet ($e58 (= ?e36 ?e39)) -(flet ($e59 (= ?e31 v0)) -(flet ($e60 (< ?e9 ?e43)) -(flet ($e61 (distinct ?e14 ?e44)) -(flet ($e62 (= ?e45 ?e29)) -(flet ($e63 (<= ?e12 ?e9)) -(flet ($e64 (>= ?e41 ?e28)) -(flet ($e65 (<= ?e11 v0)) -(flet ($e66 (< ?e29 ?e14)) -(flet ($e67 (< ?e44 v2)) -(flet ($e68 (< ?e40 ?e45)) -(flet ($e69 (> ?e34 ?e7)) -(flet ($e70 (= ?e38 ?e30)) -(flet ($e71 (>= ?e36 ?e31)) -(flet ($e72 (= ?e32 ?e38)) -(flet ($e73 (<= ?e30 ?e42)) -(flet ($e74 (= ?e11 ?e9)) -(flet ($e75 (> ?e40 ?e7)) -(flet ($e76 (distinct ?e39 ?e41)) -(flet ($e77 (< ?e11 ?e28)) -(flet ($e78 (distinct ?e31 ?e45)) -(flet ($e79 (= ?e45 ?e11)) -(flet ($e80 (>= ?e11 ?e42)) -(flet ($e81 (< ?e12 ?e7)) -(flet ($e82 (>= ?e11 ?e41)) -(flet ($e83 (<= ?e8 v0)) -(flet ($e84 (< ?e8 ?e8)) -(flet ($e85 (> ?e30 v2)) -(flet ($e86 (= ?e9 ?e30)) -(flet ($e87 (= ?e33 ?e7)) -(flet ($e88 (<= ?e32 ?e44)) -(flet ($e89 (<= ?e36 ?e33)) -(flet ($e90 (distinct ?e45 ?e45)) -(flet ($e91 (distinct ?e14 ?e44)) -(flet ($e92 (<= v1 ?e12)) -(flet ($e93 (>= v0 ?e12)) -(flet ($e94 (>= ?e46 ?e29)) -(flet ($e95 (> ?e14 ?e6)) -(flet ($e96 (>= v2 ?e14)) -(flet ($e97 (>= ?e39 ?e44)) -(flet ($e98 (>= ?e38 ?e28)) -(flet ($e99 (> v2 ?e9)) -(flet ($e100 (<= ?e42 ?e33)) -(flet ($e101 (= ?e30 ?e29)) -(flet ($e102 (= ?e9 v0)) -(flet ($e103 (distinct ?e37 ?e40)) -(flet ($e104 (= ?e43 ?e14)) -(flet ($e105 (<= ?e35 ?e13)) -(flet ($e106 (and $e102 $e70)) -(flet ($e107 (implies $e84 $e84)) -(flet ($e108 (implies $e69 $e60)) -(flet ($e109 (iff $e105 $e99)) -(flet ($e110 (iff $e100 $e80)) -(flet ($e111 (or $e52 $e86)) -(flet ($e112 (xor $e26 $e18)) -(flet ($e113 (or $e20 $e107)) -(flet ($e114 (not $e94)) -(flet ($e115 (or $e79 $e104)) -(flet ($e116 (not $e76)) -(flet ($e117 (if_then_else $e112 $e22 $e90)) -(flet ($e118 (xor $e77 $e57)) -(flet ($e119 (xor $e88 $e55)) -(flet ($e120 (and $e92 $e68)) -(flet ($e121 (or $e82 $e25)) -(flet ($e122 (implies $e19 $e119)) -(flet ($e123 (implies $e66 $e117)) -(flet ($e124 (if_then_else $e15 $e73 $e65)) -(flet ($e125 (iff $e64 $e103)) -(flet ($e126 (iff $e121 $e122)) -(flet ($e127 (if_then_else $e50 $e47 $e101)) -(flet ($e128 (iff $e81 $e127)) -(flet ($e129 (implies $e124 $e21)) -(flet ($e130 (iff $e87 $e129)) -(flet ($e131 (iff $e116 $e51)) -(flet ($e132 (implies $e72 $e97)) -(flet ($e133 (and $e56 $e98)) -(flet ($e134 (implies $e91 $e53)) -(flet ($e135 (xor $e133 $e114)) -(flet ($e136 (xor $e17 $e110)) -(flet ($e137 (iff $e96 $e128)) -(flet ($e138 (or $e125 $e59)) -(flet ($e139 (or $e23 $e48)) -(flet ($e140 (iff $e62 $e95)) -(flet ($e141 (not $e61)) -(flet ($e142 (and $e132 $e63)) -(flet ($e143 (xor $e109 $e131)) -(flet ($e144 (iff $e54 $e126)) -(flet ($e145 (xor $e74 $e67)) -(flet ($e146 (if_then_else $e89 $e93 $e140)) -(flet ($e147 (iff $e71 $e138)) -(flet ($e148 (and $e143 $e146)) -(flet ($e149 (xor $e147 $e142)) -(flet ($e150 (implies $e85 $e58)) -(flet ($e151 (or $e24 $e78)) -(flet ($e152 (if_then_else $e137 $e113 $e123)) -(flet ($e153 (and $e145 $e16)) -(flet ($e154 (not $e150)) -(flet ($e155 (implies $e151 $e154)) -(flet ($e156 (if_then_else $e118 $e136 $e75)) -(flet ($e157 (and $e108 $e108)) -(flet ($e158 (or $e83 $e141)) -(flet ($e159 (iff $e155 $e149)) -(flet ($e160 (iff $e158 $e156)) -(flet ($e161 (or $e115 $e130)) -(flet ($e162 (or $e157 $e160)) -(flet ($e163 (if_then_else $e152 $e153 $e139)) -(flet ($e164 (not $e144)) -(flet ($e165 (not $e27)) -(flet ($e166 (or $e148 $e162)) -(flet ($e167 (iff $e134 $e166)) -(flet ($e168 (or $e111 $e159)) -(flet ($e169 (or $e106 $e164)) -(flet ($e170 (xor $e161 $e120)) -(flet ($e171 (and $e168 $e165)) -(flet ($e172 (or $e170 $e135)) -(flet ($e173 (or $e169 $e163)) -(flet ($e174 (implies $e49 $e172)) -(flet ($e175 (xor $e174 $e173)) -(flet ($e176 (and $e171 $e175)) -(flet ($e177 (implies $e167 $e176)) -$e177 -)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) - |