[SMT-LIB] Benchmark and rules fixes posted

Morgan Deters mdeters at cs.nyu.edu
Fri May 7 14:12:33 EDT 2010


Hi everyone,

Last night we posted corrected benchmarks for the (let ..) issue
identified by Andrej Dyck and discussed on the SMT-LIB mailing list.
And just today (Friday) an issue involving (declare-sort ..) and
affecting AUFLIA, AUFLIRA, QF_AX, QF_UF, and UFNIA, was corrected in
the posted benchmarks.

Also, as discussed on the mailing list, (exit) will be left in
benchmarks for SMT-COMP.  The posted rules for SMT-COMP have been
updated to reflect this (with no other changes).

As always, the benchmarks are available from

  http://www.smtlib.org/

and the SMT-COMP rules are available from

  http://www.smtcomp.org/

Thanks,
Morgan
-- 
Morgan Deters
mdeters at cs.nyu.edu


More information about the SMT-LIB mailing list