summaryrefslogtreecommitdiff
path: root/test/regress/regress0/uf/euf_simp06.smt
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/uf/euf_simp06.smt')
-rw-r--r--test/regress/regress0/uf/euf_simp06.smt11
1 files changed, 0 insertions, 11 deletions
diff --git a/test/regress/regress0/uf/euf_simp06.smt b/test/regress/regress0/uf/euf_simp06.smt
deleted file mode 100644
index 020bafdff..000000000
--- a/test/regress/regress0/uf/euf_simp06.smt
+++ /dev/null
@@ -1,11 +0,0 @@
-(benchmark euf_simp6.smt
-
- :status unsat
- :difficulty { unknown }
- :category { crafted }
- :logic QF_UF
- :extrasorts (A)
- :extrafuns ((x A))
- :extrafuns ((f A A))
- :formula (let (?cvc_1 (f x)) (let (?cvc_0 (f ?cvc_1)) (not (implies (and (= ?cvc_0 x) (= (f (f (f ?cvc_0))) x)) (= ?cvc_1 x)))))
-)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback