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

[Zhoulai]

Thanks for your answer and contributions. Indeed, comments on your
benchmark can be very helpful.

As a non-expert in the area,  I would really appreciate comments in the
style of your blog, for example
http://www.spark-2014.org/entries/detail/smtlib-fp-benchmarks



Zhoulai

On Thu, Nov 26, 2015 at 12:40 AM, Schanda Florian <
florian.schanda at altran.com> wrote:

> > Thanks. It seems most of Wintersteiger's benchmarks  are in the style of
> > unit-test as you said. Then, is there  any floating point benchmarks in
> > SMT-LIB that seems more interesting,  e.g.,  x*x + 2*x + 1 <=1 where 'x'
> > is
> > an unknown FP number (rather than a real)?
>
> You might look at my benchmarks, they are all derived from real-world
> problems we have seen in SPARK. They are a bit processed to comply with
> smtlib-2.0 and dealing with solvers that do not support real literals
> constants; but I can post again my original set of unprocessed benchmarks
> since they contain comments?
>
>         Florian
>
>