Added some hand generated UF tests. Unfortunartely all of them work. Also fixed some cleanup stuff.

1 files changed, 29 insertions, 0 deletions

diff --git a/test/regress/regress0/uf/euf_simp02.smt b/test/regress/regress0/uf/euf_simp02.smt
new file mode 100644
index 000000000..9c7b03f6e
--- /dev/null
+++ b/test/regress/regress0/uf/euf_simp02.smt
@@ -0,0 +1,29 @@
+
+(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