SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2016

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides
Report

Participants

These solvers have been submitted to SMT-COMP 2016 or were entered non-competitively 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)
ABC_default X - - 7815 8091 2402498868 ABC Valeriy Balabanov (balabasik@gmail.com)
ABC_glucose X - - 7816 8092 2402498868 ABC Valeriy Balabanov (balabasik@gmail.com)
AProVE X - - 1229 (configuration: default) 483272109 AProVE Carsten Fuhs (carsten@dcs.bbk.ac.uk)
Boolector X - - 7801 8073 42 Boolector Mathias Preiner (mathias.preiner@jku.at)
Boolector (preprop) X - - 7802 8079 42 Boolector Mathias Preiner (mathias.preiner@jku.at)
CVC4 (Main track) X - - 7811 8018 823514 Clark Barrett (barrett@cs.nyu.edu)
MapleSTP X - - 7809 8069 0 Jimmy Liang (jliang@gsd.uwaterloo.ca)
MapleSTP-final - X - 7809 8270 - Jimmy Liang (jliang@gsd.uwaterloo.ca)
MapleSTP-mt X - - 7810 8070 0 Jimmy Liang (jliang@gsd.uwaterloo.ca)
MapleSTP-mt-final - X - 7810 8269 - Jimmy Liang (jliang@gsd.uwaterloo.ca)
Minkeyrink X - - 7793 8093 3828084720 Trevor Hansen (trev_abroad@yahoo.com)
OpenSMT2 (2016-05-12) X - - 7725 8700 Antti Hyvärinen (antti.hyvarinen@gmail.com)
ProB X - - 7755 7964 9247 ProB Sebastian Krings (krings@cs.uni-duesseldorf.de)
Q3B X - - 7760 8085 2784434708 Martin Jonáš (359542@mail.muni.cz)
raSAT 0.3 X - - 5594 5594 raSAT Tung Vu Xuan (tungvx@jaist.ac.jp)
raSAT 0.4 exp X - - 7814 8014 7814 raSAT Tung Vu Xuan (tungvx@jaist.ac.jp)
SMT-RAT X - - 7763 8068 17 SMT-RAT Florian Corzilius (corzilius@informatik.rwth-aachen.de)
SMTInterpol X X X 7795 8005 3536504 SMTInterpol Jochen Hoenicke (hoenicke@gmail.com)
STP-cms-exp-2016 X - - 7790 7979 0 STP Mate Soos (soos.mate@gmail.com)
STP-cms-exp-fixed-2016 - X - 7790 8244 - STP Mate Soos (soos.mate@gmail.com)
STP-cms-mt-2016 X - - 7739 7976 0 STP Mate Soos (soos.mate@gmail.com)
STP-cms-mt-fixed-2016 - X - 7739 8241 - STP Mate Soos (soos.mate@gmail.com)
STP-cms-st-2016 X - - 7738 7977 0 STP Mate Soos (soos.mate@gmail.com)
STP-cms-st-fixed-2016 - X - 7738 8242 - STP Mate Soos (soos.mate@gmail.com)
STP-minisat-st-2016 X - - 7740 7978 0 STP Mate Soos (soos.mate@gmail.com)
STP-minisat-st-fixed-2016 - X - 7740 8243 - STP Mate Soos (soos.mate@gmail.com)
toysmt X - Xn 7813 1863866937 Masahiro Sakai (masahiro.sakai@gmail.com)
Vampire X - - 7819 8097 3163 Vampire Giles Reger (giles.reger@manchester.ac.uk)
Vampire (parallel) X - - 7819 8098 3163 Vampire Giles Reger (giles.reger@manchester.ac.uk)
Yices-2.4.2 X - - 7767 8087 2004744 Bruno Dutertre (bruno.dutertre@sri.com)
Yices-2.4.2 incremental - X - 7767 8088 2004744 Bruno Dutertre (bruno.dutertre@sri.com)
CVC4 (Application track)n - X - 3091 - https://www.starexec.org/starexec/secure/details/solver.jsp?id=3091
MathSAT 5 (Main track)n X - - 7873 - http://mathsat.fbk.eu/download.php?file=mathsat-5.3.11-linux-x86_64.tar.gz
MathSAT 5 (Application track)n - X - 7874 - http://mathsat.fbk.eu/download.php?file=mathsat-5.3.11-linux-x86_64.tar.gz
MathSAT 5 (Unsat-core track)n - - X 8321 - http://mathsat.fbk.eu/download.php?file=mathsat-5.3.11-linux-x86_64.tar.gz
veriT X - Xn 7797 8013 20151003 veriT Haniel Barbosa (haniel.barbosa@inria.fr)
Z3 (4.4.1)n X X X 7875 - https://github.com/Z3Prover/z3/archive/z3-4.4.1.tar.gz
Total 27 11 5 908312613 (mod 230)

n. Non-competitive.

The opening value of the NYSE Composite Index on 2016-05-31 was 10479.88, resulting in a competition seed of 908312613 + 10479 = 908323092.

Divisions

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

Solver ALIA1,2,3 ANIA2 AUFLIA1,3 AUFLIRA1,3 AUFNIRA1,3 BV1,3 LIA1,2,3 LRA1,3 NIA1,3 NRA1,3 QF_ABV1,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,3 QF_FP1,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 UFIDL1,3 UFLIA1,3 UFLRA1,2,3 UFNIA1,3
ABC_default1 X
ABC_glucose1 X
AProVE1 X
Boolector1 X X X X X X
Boolector (preprop)1 X
CVC4 (Main track)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
MapleSTP1 X
MapleSTP-final2 X
MapleSTP-mt1 X
MapleSTP-mt-final2 X
Minkeyrink1 X
OpenSMT2 (2016-05-12)1 X X X
ProB1 X X X X
Q3B1 X X
raSAT 0.31 X X X
raSAT 0.4 exp1 X X X
SMT-RAT1 X X X X
SMTInterpol1,2,3 X X X X X X X X X X X X
STP-cms-exp-20161 X
STP-cms-exp-fixed-20162 X
STP-cms-mt-20161 X
STP-cms-mt-fixed-20162 X
STP-cms-st-20161 X
STP-cms-st-fixed-20162 X
STP-minisat-st-20161 X
STP-minisat-st-fixed-20162 X
toysmt1,3 X X X X
Vampire1 X X X X X X X X X X X X X X
Vampire (parallel)1 X X X X X X X X X X X X X X
Yices-2.4.21 X X X X X X X X X X X X X X X X X X X X X
Yices-2.4.2 incremental2 X X X X X X X
CVC4 (Application track)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
MathSAT 5 (Main track)1 X X X X X X X X X X X X X X
MathSAT 5 (Application track)2 X X X X X X X X X X X X X X
MathSAT 5 (Unsat-core track)3 X X X X X X X X X X X X X X
veriT1,3 X X X X X X X X X X X X X X X X X X X
Z3 (4.4.1)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

1. Main track.
2. Application track.
3. Unsat-core track (experimental in 2016).