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

[Schanda Florian]

> 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