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/fuzz_1.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/fuzz_1.smt')
-rw-r--r-- | test/regress/regress0/fuzz_1.smt | 32 |
1 files changed, 0 insertions, 32 deletions
diff --git a/test/regress/regress0/fuzz_1.smt b/test/regress/regress0/fuzz_1.smt deleted file mode 100644 index 22cdd2307..000000000 --- a/test/regress/regress0/fuzz_1.smt +++ /dev/null @@ -1,32 +0,0 @@ -(benchmark fuzzsmt -:logic QF_LRA -:status unsat -:extrafuns ((v0 Real)) -:formula -(let (?e1 11) -(let (?e2 1) -(let (?e3 (* v0 ?e2)) -(let (?e4 (/ ?e1 (~ ?e1))) -(flet ($e5 (< v0 ?e4)) -(flet ($e6 (< ?e3 ?e3)) -(let (?e7 (ite $e5 ?e3 ?e4)) -(let (?e8 (ite $e5 ?e3 ?e3)) -(let (?e9 (ite $e6 v0 ?e4)) -(flet ($e10 (< ?e3 ?e7)) -(flet ($e11 (< v0 ?e9)) -(flet ($e12 (= ?e8 ?e4)) -(flet ($e13 (and $e10 $e6)) -(flet ($e14 (implies $e12 $e5)) -(flet ($e15 (iff $e14 $e14)) -(flet ($e16 (iff $e11 $e11)) -(flet ($e17 (iff $e16 $e16)) -(flet ($e18 (not $e13)) -(flet ($e19 (or $e18 $e18)) -(flet ($e20 (if_then_else $e15 $e15 $e17)) -(flet ($e21 (not $e20)) -(flet ($e22 (not $e19)) -(flet ($e23 (xor $e21 $e21)) -(flet ($e24 (xor $e23 $e22)) -$e24 -))))))))))))))))))))))))) - |