SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2015

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides
Report

Participants

These solvers have been submitted to SMT-COMP 2015 or were entered non-competitively by the organizers for comparison.

Solver Main track Application track Preliminary version solver id Final version solver id Seed System description Contact(s)
AProVE X - 1229 (configuration: default) 127956425 AProVE Carsten Fuhs (c.fuhs@cs.ucl.ac.uk)
Boolector (QF_AUFBV) X - 2818 3065 42 Boolector Mathias Preiner (mathias.preiner@jku.at)
Boolector (QF_BV) X - 2819 3066 42 Boolector Mathias Preiner (mathias.preiner@jku.at)
Boolector (QF_BV incremental) - X 2820 3069 42 Boolector Mathias Preiner (mathias.preiner@jku.at)
CVC3 (Main track) X - 1262 (configuration: default) 33333 CVC3 Kshitij Bansal (kshitij@cs.nyu.edu)
CVC3 (Application track) - X 1363 33333 CVC3 Kshitij Bansal (kshitij@cs.nyu.edu)
CVC4 (Main track) X - 2877 3090 44444 CVC4 Kshitij Bansal (kshitij@cs.nyu.edu)
CVC4 (Application track) - X 2878 3091 44444 CVC4 Kshitij Bansal (kshitij@cs.nyu.edu)
CVC4 (Main track) Experimental X - 2879 3097 44444 CVC4 Kshitij Bansal (kshitij@cs.nyu.edu)
CVC4 (Application track) Experimental - X 2880 3098 44444 CVC4 Kshitij Bansal (kshitij@cs.nyu.edu)
OpenSMT2 X - 2817 (configuration: default) 3049 2817 Matteo Marescotti (matteseo@gmail.com)
OpenSMT2-parallel X - 2825 3048 2825 Matteo Marescotti (matteseo@gmail.com)
raSAT X - 2768 889 raSAT Tung Vu Xuan (tungvx@jaist.ac.jp)
SMT-RAT X - 2793 3085 0 SMT-RAT Florian Corzilius (corzilius@informatik.rwth-aachen.de)
SMT-RAT-PARL X - 2793 3086 0 SMT-RAT Florian Corzilius (corzilius@informatik.rwth-aachen.de)
SMTInterpol X X 2791 2072868739 SMTInterpol Jürgen Christ (christj@informatik.uni-freiburg.de)
STP-CryptoMiniSat4 X X 1305 0 STP Mate Soos (soos.mate@gmail.com)
STP-CryptoMiniSat4-v15 X X 2804 3059 0 STP Mate Soos (soos.mate@gmail.com)
STP-CryptoMiniSat4-mt-v15 X X 2805 3060 0 STP Mate Soos (soos.mate@gmail.com)
STP-MiniSat-v15 X X 2806 0 STP Mate Soos (soos.mate@gmail.com)
veriT X - 2864 2965 5459 veriT David Déharbe (david@dimap.ufrn.br)
Yices2 (Main track) X - 2832 (configuration: default) 3054 40278 Bruno Dutertre (bruno.dutertre@sri.com)
Yices2 (Application track) - X 2832 (configuration: incremental) 3056 40278 Bruno Dutertre (bruno.dutertre@sri.com)
Yices2-NL X - 2870 3078 0 Dejan Jovanović (dejan.jovanovic@sri.com)
Z3 (unstable) X - 2983 3147 0 Christoph Wintersteiger (cwinter@microsoft.com)
Z3 (IJCAR'14) X - 3073 3153 0 Aleksandar Zeljic (aleksandar.zeljic@it.uu.se)
Boolector (QF_BV incremental fixed)n - X - 3219 - Boolector Mathias Preiner (mathias.preiner@jku.at)
MathSAT 5 (Main track)n X - 2900 2968 - http://mathsat.fbk.eu/download.php?file=mathsat-5.3.6-linux-x86_64.tar.gz
MathSAT 5 (Application track)n - X 2900 2970 - http://mathsat.fbk.eu/download.php?file=mathsat-5.3.6-linux-x86_64.tar.gz
Z3 (4.4.0)n X X 2908 3150 - https://github.com/Z3Prover/z3/archive/z3-4.4.0.tar.gz
Total 23 13 53678630 (mod 230)

n. Non-competitive.

The opening value of the NYSE Composite Index on 2015-06-15 was 10942.51, resulting in a competition seed of 53678630 + 10942 = 53689572.

Divisions

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

Solver ALIA1,2 ANIA2 AUFLIA1 AUFLIRA1 AUFNIRA1 BV1 LIA1,2 LRA1 NIA1 NRA1 QF_ABV1 QF_ALIA1,2 QF_ANIA1,2 QF_AUFBV1 QF_AUFLIA1,2 QF_AUFNIA1 QF_AX1 QF_BV1,2 QF_BVFP1,3 QF_FP1,3 QF_IDL1 QF_LIA1,2 QF_LIRA1 QF_LRA1,2 QF_NIA1,2 QF_NIRA1 QF_NRA1 QF_RDL1 QF_UF1 QF_UFBV1 QF_UFIDL1 QF_UFLIA1,2 QF_UFLRA1,2 QF_UFNIA1,2 QF_UFNRA1 UF1 UFBV1 UFIDL1 UFLIA1 UFLRA1,2 UFNIA1
AProVE1 X
Boolector (QF_AUFBV)1 X X X
Boolector (QF_BV)1 X
Boolector (QF_BV incremental)2 X
CVC3 (Main track)1 X X X X X X X X X X X X X X X X X X X
CVC3 (Application track)2 X X X X X X X X X X X X X X X X X X 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
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
CVC4 (Main track) Experimental1 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 track) Experimental2 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
OpenSMT21 X
OpenSMT2-parallel1 X
raSAT1 X X
SMT-RAT1 X X X X X X X X
SMT-RAT-PARL1 X
SMTInterpol1,2 X X X X X X X X X X X X
STP-CryptoMiniSat41,2 X
STP-CryptoMiniSat4-v151,2 X
STP-CryptoMiniSat4-mt-v151,2 X
STP-MiniSat-v151,2 X
veriT1 X X X X X X X X X X X X X X X X X X X X
Yices2 (Main track)1 X X X X X X X X X X X X X X X X
Yices2 (Application track)2 X X X X X X X X X X X X X X X X
Yices2-NL1 X
Z3 (unstable)1 X X
Z3 (IJCAR'14)1 X X
Boolector (QF_BV incremental fixed)2 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
Z3 (4.4.0)1,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

1. Main Track.
2. Application Track.
3. Floating-point divisions are considered experimental in 2015.