DOMAINS :: SMT-LIB :: ANY in extrasorts

[QPQ]

Forums QPQ
DOMAINS :: SMT-LIB ::.. ANY in extrasorts

barrett wrote at Mar 07, 2006 - 05:25 PM
---------------------------------------------------------------------
These benchmarks were translated from benchmarks in CVC format provided by Leonardo
de Moura.  In the CVC benchmarks, the following line appears:

ANY : TYPE;

which is faithfully translated into:

:extrasorts (ANY)

So, it was not intentionally introduced into the smtlib version but is an artifact of
the original cvc benchmarks.  I don't know why it occurs in those benchmarks when it
is never used.  Thank you for pointing this out.  I will hopefully have the chance to
address issues like this before we finalize the benchmarks for this year's SMT-COMP.

-Clark

---------------------------------------------------------------------

Reply to this message:
http://www.qpq.org/modules.php?op=modload&name=phpBB_14&file=index&action=reply&topic=177&forum=46

Browse thread:
http://www.qpq.org/modules.php?op=modload&name=phpBB_14&file=index&action=viewtopic&topic=177

You are receiving this Email because you are subscribed to be notified of events in forums at: http://www.qpq.org/