Dear SMT-LIB community,
In case it is of interest for competition or other evaluation, the
is a set (7MB compressed) of benchmarks from our verification system
We use CVC4 for solving these verification conditions, with typical
-q --produce-models --incremental --print-success --lang smt2.5
so I believe they adhere to the standard.
We have more smt files for our evaluation suite, but they may fall out
of SMT-LIB standard at the moment (e.g. due to the use of extended array
In case you know someone interested to collaborate on stainless front
ends for new languages, back ends (C, WASM), better encoding of
functional, imperative and object-oriented constructs, decision
procedures, or caching of proof obligations (among other topics), I will
be happy to talk to them.
(for the Stainless team)