[SMT-LIB] Benchmark Conformance: log in AUFLIRA/nasa/

[Tjark Weber]

Dear Cesare,

On Wed, 2010-11-03 at 00:31 -0500, Cesare Tinelli wrote:
> Personally, I'm neutral on this and I'd be happy to modify the
> declarations of AUFLIRA and AUFNIRA in either direction. Before
> proceeding then, it'd be good to hear from this community.
> 
> Any comments?

I am inclined to agree with Nikolaj and David that there should be no
implicit conversions.  They complicate parsing; the present conformance
issue proves that the details are easy to get wrong; and their benefits
seem marginal, considering that SMT-LIB is generated and read by
automated tools more often than by human beings.

Instead of (log (to_real 330)), one could simply write (log 330.0).

Regards,
Tjark