summaryrefslogtreecommitdiff
path: root/test/regress/regress0/uf/eq_diamond14.reduced.smt
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/uf/eq_diamond14.reduced.smt')
-rw-r--r--test/regress/regress0/uf/eq_diamond14.reduced.smt1
1 files changed, 0 insertions, 1 deletions
diff --git a/test/regress/regress0/uf/eq_diamond14.reduced.smt b/test/regress/regress0/uf/eq_diamond14.reduced.smt
index b41e4536d..6af6ac5be 100644
--- a/test/regress/regress0/uf/eq_diamond14.reduced.smt
+++ b/test/regress/regress0/uf/eq_diamond14.reduced.smt
@@ -32,7 +32,6 @@
:extrafuns ((y1 V))
:extrafuns ((x1 V))
:extrafuns ((y0 V))
-:status unknown
:formula
(flet ($n1 (= x0 y0))
(flet ($n2 (= y0 x1))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback