[SMT-LIB] SMT-COMP results on QF_FP

[Martin Brain]

On Fri, 2015-12-18 at 12:08 -0800, Zhoulai wrote:
> Hello,
> 
> I have tried Z3 on the QF_FP theory, and I am looking into this year's
> SMT-COMP results as reported here:
> http://smtcomp.sourceforge.net/2015/results-QF_FP.shtml?v=1446209369
> 
> By reading the table in the link above,  Z3 should finish +30,000
> benchmarks within a total time of 10,000 seconds (i.e, < 3 hours). But I
> just tried Z3 version 4.4.2 with one single benchmark from Griggio, which
> takes already 2 hours without yielding any sat/unsat results.  Do I need to
> allocate more memory in some way to see the results as in the competition?
> I am using a Mac Os with 16G memory.

You might want to look at what the experimental set-up for the
competition is.  Normally there is a CPU time and memory limit and the
time reported if often the total for all benchmarks that finish within
the given time limit.

Cheers,
 - Martin