[SMT-LIB] New SMT-LIB release for SMT-COMP 2011---includes fixes, additions

[cok at frontiernet.net]

Hi Morgan,

A couple more:

The new QF_NIA (01.smt2 and elsewhere) has a definition of power2 where the return sort is declared Int but the expression is Bool.

AUFNIRA uses Int arguments for a user-defined function divide with Real parameters.

- David
 


----- "Morgan Deters" <mdeters at cs.nyu.edu> wrote:

> Hi Tjark, everyone,
> 
> I've made a number of benchmark corrections today to address these
> issues.
> 
> The define-funs and unary ORs in QF_BV/mcm have been fixed, along
> with
> the assertion-less CAS benchmarks (which was due to an undetected
> CVC3
> parsing issue, leading to bad translations), have been fixed.
> 
> Work on the empty sage benchmarks and the persistent real-literal bug
> is ongoing.
> 
> Morgan
> -- 
> Morgan Deters
> Research Scientist
> Courant Institute of Mathematical Sciences
> 251 Mercer St., New York, NY 10012
> mdeters at cs.nyu.edu - http://cs.nyu.edu/~mdeters/
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib