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

[Zhoulai]

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