| Home | • | Rules | • | Benchmarks | • | Tools | • | Specs | • | Participants | • | Results | • | SMT-LIB | • | Previous |
|---|
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.
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 12 Jun 2018 12:25 UTC