summaryrefslogtreecommitdiff
path: root/test/regress/regress0/uf/euf_simp03.smt
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/uf/euf_simp03.smt')
-rw-r--r--test/regress/regress0/uf/euf_simp03.smt26
1 files changed, 0 insertions, 26 deletions
diff --git a/test/regress/regress0/uf/euf_simp03.smt b/test/regress/regress0/uf/euf_simp03.smt
deleted file mode 100644
index e0d6cc849..000000000
--- a/test/regress/regress0/uf/euf_simp03.smt
+++ /dev/null
@@ -1,26 +0,0 @@
-
-(benchmark euf_simp3.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 (f x)) (f (f (f x))))
- (= (f (f x)) y)
- (= (f (f (f (f x)))) z)
- (= (f x) z)
- (not (= (f x) y))
- )
-) \ No newline at end of file
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback