[SMT-LIB] Question on Syntax for Benchmarks

[Paulo J. Matos]

Hi all,

In version 1.2 you find:
:extrafuns ( <fun_symb_decli>+ )

and then (in the theories part, since it is undefined in benchmarks part):
<fun_symb_decl> ::= ( <fun_symb> <sort_symb>+ <annotation> )
                            | ( <numeral> <sort_symb> <annotation> )
                            | ( <rational> <sort_symb> <annotation> )

I guess that for benchmarks only the first part really applies (constrained):
<fun_symb_decl> ::= ( <fun_symb> <sort_symb> <annotation> )

Right?

Regards,
-- 
Paulo Jorge Matos - pocm at soton.ac.uk
http://www.personal.soton.ac.uk/pocm
PhD Student @ ECS
University of Southampton, UK