[SMT-LIB] Command line to produce the competition results for the QF_FP division

Zhoulai zell08v at gmail.com
Tue Jan 19 12:31:14 EST 2016


Hello,

I am trying to produce the competition results for the QF_FP division as
reported at this page:
http://smtcomp.sourceforge.net/2015/results-QF_FP.shtml?v=1446209369

I have two questions for doing so:

1. What do Z3 (FP) and Z3 (IJCAR14) refer to respectively?
2. What are the  command line options used to run these benchmarks?

For MathSat5,  I use:
mathsat <filename> for MathSat 5,

and for Z3 4.4.2, I use:
z3 --smt2 <filename> for Z3.

Are there additional options I need to put for MathSat or Z3?

I do not use the same machine as StarExec and only need to produce the
results on a local machine for comparison purpose.  Thanks for your help.

Zhoulai


More information about the SMT-LIB mailing list