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.

1 files changed, 0 insertions, 29 deletions

diff --git a/test/regress/regress0/uf/euf_simp02.smt b/test/regress/regress0/uf/euf_simp02.smt
deleted file mode 100644
index 9c7b03f6e..000000000
--- a/test/regress/regress0/uf/euf_simp02.smt
+++ /dev/null
@@ -1,29 +0,0 @@
-
-(benchmark euf_simp2.smt
-:status unsat
-:logic QF_UF
-:category { crafted }
-
-:extrafuns ((x U))
-:extrafuns ((y U))
-:extrafuns ((z U))
-:extrafuns ((f U U))
-:extrafuns ((g U U))
-:extrafuns ((H U U U))
-:extrafuns ((J U U U))
-
-
-
-:formula
-(and
- (not (= x y))
- (= (f x) (f z))
- (= (g y) (g z))
- (= (g y) (g z))
- (= (g y) y)
- (= (f x) x)
- (= (f z) z)
- (= (g z) z)
- (or (not (= x z)) (not (= y z)))
- )
-)
\ No newline at end of file