summaryrefslogtreecommitdiff
path: root/test/regress/regress0/uf/euf_simp01.smt
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/uf/euf_simp01.smt')
-rw-r--r--test/regress/regress0/uf/euf_simp01.smt23
1 files changed, 0 insertions, 23 deletions
diff --git a/test/regress/regress0/uf/euf_simp01.smt b/test/regress/regress0/uf/euf_simp01.smt
deleted file mode 100644
index c121ae82e..000000000
--- a/test/regress/regress0/uf/euf_simp01.smt
+++ /dev/null
@@ -1,23 +0,0 @@
-
-(benchmark euf_simp1.smt
-:status sat
-: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
- (= (f x) (f z))
- (= (g y) (g 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