Stainless 2021 smt2.5 benchmarks

[Viktor Kunčak]

Dear SMT-LIB community,

In case it is of interest for competition or other evaluation, the
following:

https://lara.epfl.ch/~kuncak/smt-sessions-CVC4.tar.gz

is a set (7MB compressed) of benchmarks from our verification system

https://github.com/epfl-lara/stainless
https://stainless.epfl.ch/

We use CVC4 for solving these verification conditions, with typical
options being:

-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
theory).

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.

Best regards

   Viktor Kuncak
   (for the Stainless team)