[SMT-LIB] A beginner's question about Wintersteiger's benchmark

[Martin Brain]

On Wed, 2015-11-25 at 18:20 -0800, Levent Erkok wrote:
> It'd be fairly easy to generate such benchmarks; but I don't know of the
> top of my head if there's a "good" collection of them anywhere.

As someone who has done this -- it's harder than you might think to
create benchmarks that are meaningful, not too easy or too hard and in
sufficient numbers / with sufficient variety that experiments using them
are significant.

> Incidentally, the benchmark you suggested has the trivial solution of "0";
> I'm guessing you had something more interesting in mind. In any case, I
> generated the attached benchmark for it using the SBV-library for Haskell;
> see attached.
> 
> (Using higher-level languages instead of SMT-Lib makes generating such
> queries much easier. There are bindings from many languages. If Haskell is
> your choice then more info on SBV is available here:
> http://leventerkok.github.io/sbv/. For this use case, there's a function
> called 'compileToSMTLib' 'that does the trick:
> https://github.com/LeventErkok/sbv/blob/cc7a6f7017859c10f1c4411112601766e835d9dc/Data/SBV/Provers/Prover.hs#L313
> )

If you want to use C then I can recommend CBMC, likewise for Ada I'd
suggest SPARK.

Cheers,
 - Martin