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

[Morgan Deters]

Hi Tjark,

This also came up recently in conversations with Nikolaj Bjorner and
Cesar Tinelli, and I discovered the issue in CVC3's SMT-LIBv2 output
(we used CVC3 to translate older SMT-LIBv1 benchmarks and check them
for conformance).

I need now to re-process the benchmark library and post updated
benchmarks (fixing also some other reported issues); I'll let the
smt-lib list know when this is done.

Thanks,
Morgan


On Wed, Oct 13, 2010 at 02:55:52PM +0100, Tjark Weber wrote:
> 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
> 
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib

-- 
Morgan Deters
mdeters at cs.nyu.edu