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

[Tjark Weber]

Certain benchmarks in AUFLIRA/nasa/ declare a function

  (declare-fun log (Real) Real)

and apply this function to a numeral: e.g., (log 330) at line 64, column
95 in benchmark AUFLIRA/nasa/fol_simplify/gauss_init_0057.fof.smt2.

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.

I believe that in total, this issue affects at least 549 benchmarks in
AUFLIRA/nasa.

A possible solution would be to write arguments to log as decimals:
e.g., (log 330.0).  Alternatively, one could augment the definition of
AUFLIRA to permit implicit conversion also for unary functions, or even
for functions of arbitrary arity.

Regards,
Tjark