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

[Tjark Weber]

On Wed, 2010-10-13 at 13:24 +0100, Tjark Weber wrote:
> As far as I can tell, this is not valid.  Logic AUFLIRA is based on
> theory Reals_Ints, which declares NUMERALs to be of sort Int (while
> DECIMALs are of sort Real).  The :extensions in AUFLIRA permit implicit
> conversion from Int to Real only for binary operators; they do not apply
> to the unary function log.  Hence, (log 330) is ill-typed.

A related issue affects a number of benchmarks in AUFLIRA/nasa and
AUFNIRA/nasa.  In these benchmarks, the array update function (store)
and a user-declared function divide of type ((Real Real) Real) are
applied to numerals.  Again, AUFLIRA/AUFNIRA do not admit implicit
conversions from Int to Real (because store is ternary, and because
divide is passed two Int arguments, which would both need to be
converted).

Regards,
Tjark