[SMT-COMP] benchmarks posted

Clark Barrett barrett at cs.nyu.edu
Wed May 21 00:38:31 EDT 2008


A final set of benchmarks has been posted on the SMT-LIB website.  No more
benchmarks beyond those posted will be considered for the competition.

However, corrections may be made to these benchmarks until June 1.  Please let
us know if you find any errors.

A large number of benchmarks have been submitted in a new division, UFNIA
(quantifiers, uninterpreted functions, and non-linear integer arithmetic).
These benchmarks are very similar to those in AUFLIA except that in a few
places a term is multiplied by a bound variable, so they are not quite linear.

We are looking for feedback as to whether these benchmarks should be included
in their own division in the competition.  Please let us know if you have a
solver that could compete on these benchmarks.

-SMT-COMP organizers


More information about the SMT-COMP mailing list