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

Morgan Deters mdeters at cs.nyu.edu
Fri May 20 15:29:00 EDT 2011


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/


More information about the SMT-LIB mailing list