[SMT-LIB] SMT-COMP results on QF_FP

Zhoulai zell08v at gmail.com
Fri Dec 18 15:08:36 EST 2015


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.

Thanks for your help.
--
Zhoulai

p.s. The mentioned smt-lib2 file is '*sin2.c.10.smt2*', which can be
downloaded from "http://www.cs.nyu.edu/~barrett/smtlib/QF_FP_Hierarchy.zip".


More information about the SMT-LIB mailing list