Stainless 2021 smt2.5 benchmarks

Skip to first unread message

Viktor Kunčak

May 3, 2021, 4:51:46 PM5/3/21
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
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

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)
Reply all
Reply to author
0 new messages