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

[Martin Brain]

On Wed, 2015-11-25 at 15:55 -0800, Zhoulai wrote:
> Thanks. It seems most of Wintersteiger's benchmarks  are in the style of
> unit-test as you said.

Yes.  Floating-point is notoriously detailed and has lots of awkward
edge cases.  Christoph kindly wrote and released a set of unit-test
style benchmarks to help everyone catch these.

>  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)?

Have a look in QF_BVFP/, QF_FP/schanda and QF_FP/griggio.

Cheers,
 - Martin