summaryrefslogtreecommitdiff
path: root/test/regress/regress0/uf/euf_simp02.smt
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/uf/euf_simp02.smt')
-rw-r--r--test/regress/regress0/uf/euf_simp02.smt29
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback