Home Rules Benchmarks Tools Specs Participants Results SMT-LIB Previous

Participants

These solvers have been submitted to SMT-COMP 2017 or were entered as non-competing solvers by the organizers for comparison.

Solver Main track Application track Unsat-core track Preliminary version solver id Final version solver id Seed System description Contact(s)
AProVE X - - 1229 (configuration: default) 935243 Carsten Fuhs (carsten@dcs.bbk.ac.uk)
Boolector X - - 11608 12020 424242 Boolector Mathias Preiner (mathias.preiner@jku.at)
Boolector+CaDiCaL X - - 11608 12034 0 Boolector Mathias Preiner (mathias.preiner@jku.at)
COLIBRI X - - 11650 12031 385141 François Bobot (francois.bobot@cea.fr)
CVC4 (Main) X - - 11622 12023 4261980 Clark Barrett (barrett@cs.stanford.edu)
CVC4 (Application) - X - 11622 12024 0 Clark Barrett (barrett@cs.stanford.edu)
CVC4 (Unsat-core) - - X 11622 12089 0 Clark Barrett (barrett@cs.stanford.edu)
MathSAT 5.4.1 (Main)n X - - 11978 - http://mathsat.fbk.eu/download.php?file=mathsat-5.4.1-linux-x86_64.tar.gz
MathSAT 5.4.1 (Application)n - X - 11979 - http://mathsat.fbk.eu/download.php?file=mathsat-5.4.1-linux-x86_64.tar.gz
MathSAT 5.4.1 (Unsat-core)n - - X 12211 - http://mathsat.fbk.eu/download.php?file=mathsat-5.4.1-linux-x86_64.tar.gz
MinkeyRink X - - 1234 11999 2355432 Trevor Hansen (trev_Abroad@yahoo.com)
opensmt2 X X - 11630 31415 Antti Hyvärinen (antti.hyvaerinen@usi.ch)
Q3B X - - 8085 11954 18661329 Martin Jonas (martin.jonas@mail.muni.cz)
Redlog X - - 11654 11892 20170704 Redlog Haniel Barbosa (haniel.barbosa@inria.fr)
SMT-RAT X - - 11282 11977 4711 SMT-RAT Gereon Kremer (gereon.kremer@cs.rwth-aachen.de)
SMTInterpol X X X 11698 1953339634 SMTInterpol Jochen Hoenicke (hoenicke@informatik.uni-freiburg.de)
STP-mt X - - 1234 12002 433324 Trevor Hansen (trev_Abroad@yahoo.com)
STP-st X - - 1234 12001 734534 Trevor Hansen (trev_Abroad@yahoo.com)
Vampire X - - 11643 12028 3648 Vampire Giles Reger (giles.reger@manchester.ac.uk)
veriT X - - 11466 11989 20151003 veriT Haniel Barbosa (haniel.barbosa@inria.fr)
veriT+Redlog X - - 11466 12005 20170605 veriT+Redlog Haniel Barbosa (haniel.barbosa@inria.fr)
veriT+raSAT+Redlog X - - 11469 19061999 veriT+raSAT+Redlog Haniel Barbosa (haniel.barbosa@inria.fr)
XSat X - - 11647 1164700 XSat Martin Velez (marvelez@ucdavis.edu)
Yices2 (Main) X - - 11652 12010 11976743 Dejan Jovanović (dejan.jovanovic@sri.com)
Yices2 (Application) - X - 11652 12011 17735201 Dejan Jovanović (dejan.jovanovic@sri.com)
Z3 (4.5.0)n X X X 12033 - https://github.com/Z3Prover/z3/archive/z3-4.5.0.tar.gz
Total 21 6 4 1018259764 (mod 230)

n. Non-competing.

The opening value of the NYSE Composite Index on 2017-06-20 was 11801.20, resulting in a competition seed of 1018259764 + 11801 = 1018271565.

Divisions

These are the logic divisions in which each solver is participating.

Solver ABVFP1 ALIA1,2,3 ANIA2 AUFBVDTLIA1 AUFDTLIA1 AUFLIA1,3 AUFLIRA1,3 AUFNIRA1,3 BV1,3 BVFP1 FP1 LIA1,2,3 LRA1,3 NIA1,3 NRA1,3 QF_ABV1,3 QF_ABVFP1,3 QF_ALIA1,2,3 QF_ANIA1,2,3 QF_AUFBV1,3 QF_AUFLIA1,2,3 QF_AUFNIA1,3 QF_AX1,3 QF_BV1,2,3 QF_BVFP1,2,3 QF_DT1 QF_FP1,2,3 QF_IDL1,3 QF_LIA1,2,3 QF_LIRA1,3 QF_LRA1,2,3 QF_NIA1,2,3 QF_NIRA1,3 QF_NRA1,3 QF_RDL1,3 QF_UF1,3 QF_UFBV1,3 QF_UFIDL1,3 QF_UFLIA1,2,3 QF_UFLRA1,2,3 QF_UFNIA1,2,3 QF_UFNRA1,3 UF1,3 UFBV1,3 UFDT1 UFDTLIA1 UFIDL1,3 UFLIA1,3 UFLRA1,2,3 UFNIA1,3
AProVE1 X
Boolector1 X X X X X
Boolector+CaDiCaL1 X
COLIBRI1 X X
CVC4 (Main)1 X x X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X
CVC4 (Application)2 X X x x x x x x X x x x x X X x X x x X x x X x X X x x x x x x X X X x x x x x x x X x
CVC4 (Unsat-core)3 X x x x X X X X X X X X X X X X X X X X x X X X X X X X X X X X X X X X X X x x X X X X
MathSAT 5.4.1 (Main)1 X X X X X X X X X X X X
MathSAT 5.4.1 (Application)2 x X x X x X X X x x X X
MathSAT 5.4.1 (Unsat-core)3 X X X X X X X X X X X X
MinkeyRink1 X
opensmt21,2 X X
Q3B1 X X
Redlog1 X X
SMT-RAT1 X X X X X X
SMTInterpol1,2,3 X X X X X X X X X X X X
STP-mt1 X
STP-st1 X
Vampire1 X X X X X X X X X X X X X X X X X
veriT1 X X X X X X X X X X X X X X X X X X
veriT+Redlog1 X X
veriT+raSAT+Redlog1 X X
XSat1 X
Yices2 (Main)1 X X X X X X X X X X X X X X X X X X X X X
Yices2 (Application)2 x X x X x X x X x X x x x x X X
Z3 (4.5.0)1,2,3 X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X

1. Main track.
2. Application track.
3. Unsat-core track.

Home Rules Benchmarks Tools Specs Participants Results SMT-LIB Previous

Last modified: Tue 05 Sep 2017 13:18 UTC
Valid XHTML 1.0 Valid CSS!