[SMT-LIB] Changes and additions to benchmarks

Clark Barrett barrett at cs.nyu.edu
Mon Nov 20 11:32:34 EST 2006


For your information, the following changes have been made to the benchmark
library:

6404 new benchmarks have been added to the set of QF_UF benchmarks.  These were
provided by Volker Sorge and are based on classification of quasi-groups.

Most of the RTCL benchmarks were moved from QF_LIA to QF_UFIDL because they are
a better fit for difference logic than linear arithmetic.

Some slight modifications were made to a number of the other QF_UFIDL
benchmarks to eliminate the use of constructs that technically are not allowed by
this logic.

-Clark


More information about the SMT-LIB mailing list