The benchmarks collected in this repository use features that will be included in future SMT-LIB releases. They are not currently SMT-LIB compliant, and are not part of the official benchmark release. They are collected here to allow the community to experiment with these features.
When the non-standard features used by a problem set becomes part of the SMT-LIB standard, this set will be included in the next official benchmark release.
All benchmarks collected here follow the style guidelines of the official benchmark release.
non-incremental/AUFBVDTNIA/20240618-LibMLKEM/- uses
nat2bvandbv2nat - checked using Dolmen with
--ext=bvconv.
- uses
non-incremental/QF_AUFBV/20240117-hevm-msoos- uses
(as const - not checked with Dolmen.
- uses
non-incremental/LIA/psyco- have arithmetic expressions that are not compliant with SMT-LIB's restrictions on linear arithmetic.
non-incremental/AUFLIA/20230321-UltimateAutomizerSvcomp2023non-incremental/QF_ABV/20230321-UltimateAutomizerSvcomp2023- Use nested array sorts (such as
(Array Int (Array Int Int))) not allowed in LIA logics.
- Use nested array sorts (such as