SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2019

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

Largest Contribution Ranking - Single Query Track

Page generated on 2019-07-23 17:57:10 +0000

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
CVC4 CVC4 Par4 Par4 Vampire

Sequential Performance

Solver Correct Score Time Score Division
CVC4 0.00427411 0.01571041 QF_NIA
Vampire 0.00336154 0.0053727 UF
Par4 0.00314984 0.00521575 UFNIA
CVC4 0.00197351 0.00455372 LIA
CVC4 0.00193427 0.00079577 UFDT
Par4 0.00124067 0.00757001 LRA
CVC4 0.00115031 0.00080082 UFDTLIA
Par4 0.00095988 0.0131582 AUFLIRA
Vampire 0.00056755 0.00092622 UFLIA
CVC4 0.00052943 0.00124149 AUFDTLIA
Vampire 0.00046463 0.0033673 AUFLIA
Par4 0.00042188 0.00474538 QF_NRA
Par4 0.00029702 9.497e-05 AUFNIRA
Boolector 0.00027639 0.02393309 QF_BV
Par4 0.00018485 0.00021945 UFBV
Q3B 0.00014144 0.00285693 BV
Ctrl-Ergo 0.00012282 0.0060057 QF_LIA
Yices 2.6.2 9.934e-05 0.00200565 QF_UFIDL
Par4 8.632e-05 0.00078287 NRA
Yices 2.6.2 7.589e-05 0.00079589 QF_IDL
COLIBRI 7.563e-05 0.00054526 QF_FP
CVC4 4.808e-05 0.00158262 QF_UFNIA
Yices 2.6.2 4.095e-05 0.00019983 QF_AUFBV
CVC4 2.846e-05 0.00010053 NIA
Par4 2.53e-05 3.23e-05 UFIDL
SPASS-SATT 1.544e-05 0.00191605 QF_LRA
SMTInterpol 1.518e-05 0.00028785 ALIA
Boolector 9.51e-06 0.00886823 QF_ABV
SMTInterpol 9.49e-06 0.00100021 QF_UFLRA
SMT-RAT 9.49e-06 1.782e-05 QF_NIRA
Yices 2.6.2 8.76e-06 0.00014908 QF_RDL
Par4 7.59e-06 4.884e-05 QF_LIRA
Par4 0.0 0.01546875 QF_UF
Yices 2.6.2 0.0 0.00582613 QF_AUFLIA
Yices 2.6.2 0.0 0.0024537 QF_UFLIA
Yices 2.6.2 0.0 0.00213777 QF_AX
Yices 2.6.2 0.0 0.0011973 QF_ALIA
CVC4 0.0 0.000571 QF_UFBV
Par4 0.0 0.00012766 QF_UFNRA
CVC4 0.0 7.93e-06 QF_ANIA
Vampire 0.0 5.56e-06 UFDTNIA
MathSAT-default 0.0 3.04e-06 QF_AUFNIA
veriT 0.0 0.0 UFLRA

Parallel Performance

Solver Correct Score Time Score Division
CVC4 0.00400607 0.01290612 QF_NIA
Vampire 0.00355404 0.00443562 UF
Par4 0.00308559 0.00567552 UFNIA
CVC4 0.00195833 0.00455371 LIA
CVC4 0.00182865 0.0007447 UFDT
Par4 0.00141705 0.00838973 LRA
CVC4 0.00115031 0.0007948 UFDTLIA
Par4 0.00095988 0.0130767 AUFLIRA
Vampire 0.00073269 0.00098814 UFLIA
CVC4 0.00052943 0.00123847 AUFDTLIA
Vampire 0.00046303 0.00365399 AUFLIA
Par4 0.00042188 0.00558371 QF_NRA
Par4 0.00019801 8.018e-05 AUFNIRA
Par4 0.00018485 0.00021957 UFBV
Par4 0.00016269 0.00104863 QF_IDL
Poolector 0.00013813 0.00610465 QF_BV
Ctrl-Ergo 0.00013804 0.0085191 QF_LIA
Q3B 0.000129 0.00284458 BV
Yices 2.6.2 9.934e-05 0.00200368 QF_UFIDL
Par4 8.632e-05 0.00079113 NRA
COLIBRI 7.496e-05 0.00048183 QF_FP
CVC4 4.808e-05 0.00158258 QF_UFNIA
Yices 2.6.2 4.095e-05 0.00019986 QF_AUFBV
CVC4 2.846e-05 0.0001017 NIA
Par4 2.53e-05 3.922e-05 UFIDL
SPASS-SATT 1.544e-05 0.0011344 QF_LRA
SMTInterpol 1.518e-05 0.00028799 ALIA
Par4 1.328e-05 0.00014913 QF_UFNRA
Par4 9.51e-06 0.00794912 QF_ABV
SMTInterpol 9.49e-06 0.00118576 QF_UFLRA
SMT-RAT 9.49e-06 1.782e-05 QF_NIRA
Yices 2.6.2 8.76e-06 0.00014749 QF_RDL
Par4 7.59e-06 5.077e-05 QF_LIRA
veriT 0.0 0.00891763 QF_UF
Yices 2.6.2 0.0 0.00565019 QF_AUFLIA
Yices 2.6.2 0.0 0.00236614 QF_UFLIA
Yices 2.6.2 0.0 0.00208404 QF_AX
Yices 2.6.2 0.0 0.00110391 QF_ALIA
CVC4 0.0 0.00057017 QF_UFBV
CVC4 0.0 7.87e-06 QF_ANIA
Vampire 0.0 5.44e-06 UFDTNIA
MathSAT-default 0.0 3.04e-06 QF_AUFNIA
veriT 0.0 0.0 UFLRA

SAT Performance

Solver Correct Score Time Score Division
Par4 0.02874303 0.00092181 AUFLIRA
SMTInterpol 0.00972788 3.424e-05 UFLIA
Vampire 0.00668556 0.00243225 UF
CVC4 0.00551134 0.0003725 UFDT
CVC4 0.00414216 0.00427465 QF_NIA
CVC4 0.00354559 0.00198276 LIA
SMTInterpol 0.00242203 0.00024995 AUFLIA
Par4 0.00227713 2.759e-05 AUFNIRA
Par4 0.00213739 0.00121619 LRA
CVC4 0.00156552 0.00041883 AUFDTLIA
Par4 0.00088808 0.00019367 UFNIA
Par4 0.00088239 9.49e-06 NRA
Par4 0.00085914 0.00074438 QF_NRA
Par4 0.00040988 0.00010246 UFBV
SMTInterpol 0.00028844 1.518e-05 ALIA
Ctrl-Ergo 0.00024414 0.00032283 QF_LIA
Q3B 0.00019686 8.737e-05 BV
Poolector 0.00019671 0.00011098 QF_BV
Par4 0.00013637 0.00014877 QF_IDL
Par4 0.00010121 2.009e-05 UFIDL
COLIBRI 9.412e-05 0.00010418 QF_FP
Yices 2.6.2 4.446e-05 8.02e-06 QF_AUFBV
CVC4 3.18e-05 4.649e-05 QF_UFNIA
Par4 2.8e-05 3.947e-05 QF_LRA
CVC4 2.319e-05 5.144e-05 NIA
SMTInterpol 1.555e-05 5.96e-06 QF_UFLRA
Par4 1.439e-05 9.893e-05 QF_UFNRA
Yices 2.6.2 0.0 2.422e-05 QF_RDL
Poolector 0.0 3.11e-06 QF_ABV
Yices 2.6.2 0.0 2.91e-06 QF_UFBV
Yices 2.6.2 0.0 4.9e-07 QF_UFLIA
Yices 2.6.2 0.0 4.8e-07 QF_ALIA
Yices 2.6.2 0.0 1.9e-07 QF_AUFLIA
Yices 2.6.2 0.0 9.0e-08 QF_UF
Yices 2.6.2 0.0 4.0e-08 QF_AX
Yices 2.6.2 0.0 4.0e-08 QF_UFIDL
Yices 2.6.2 0.0 0.0 QF_LIRA
MathSAT-default 0.0 0.0 QF_AUFNIA

UNSAT Performance

Solver Correct Score Time Score Division
Par4 0.00339904 0.00450658 UFNIA
Par4 0.00301761 0.00103598 QF_NIA
Vampire 0.00186316 0.00076494 UF
CVC4 0.00115031 0.0007948 UFDTLIA
Par4 0.00095653 0.00117697 LRA
Vampire 0.00073696 0.00098024 UFLIA
CVC4 0.00055166 0.00021944 UFDT
Vampire 0.00051805 0.00186995 AUFLIA
CVC4 0.00039209 0.00039025 LIA
CVC4 0.0003074 0.00031012 QF_NRA
Par4 0.00020998 8.668e-05 QF_IDL
Vampire 0.00015526 6.373e-05 AUFNIRA
Yices 2.6.2 0.00013335 0.00039625 QF_UFIDL
Poolector 0.00010644 6.501e-05 QF_BV
Par4 0.00010587 9.278e-05 QF_LIA
Q3B 0.00010022 0.00022956 BV
Par4 7.757e-05 0.00070327 NRA
CVC4 7.298e-05 4.597e-05 QF_UFNIA
Par4 6.21e-05 5.657e-05 UFBV
COLIBRI 5.328e-05 3.889e-05 QF_FP
CVC4 5.218e-05 1.042e-05 NIA
Yices 2.6.2 4.016e-05 0.00010024 QF_AUFBV
SPASS-SATT 3.439e-05 2.355e-05 QF_LRA
Par4 3.028e-05 3.26e-05 QF_ABV
Vampire 1.839e-05 0.00032928 AUFLIRA
Yices 2.6.2 1.72e-05 1.471e-05 QF_RDL
SMT-RAT 9.49e-06 1.782e-05 QF_NIRA
Par4 8.86e-06 2.593e-05 QF_LIRA
CVC4 0.0 1.685e-05 QF_UFBV
CVC4 0.0 7.87e-06 QF_ANIA
Vampire 0.0 5.44e-06 UFDTNIA
Yices 2.6.2 0.0 1.79e-06 QF_ALIA
Yices 2.6.2 0.0 1.25e-06 QF_AUFLIA
veriT 0.0 8.4e-07 QF_UF
Yices 2.6.2 0.0 6.5e-07 QF_UFLIA
Yices 2.6.2 0.0 2.9e-07 QF_AX
Alt-Ergo 0.0 1.5e-07 ALIA
Yices 2.6.2 0.0 1.4e-07 QF_UFLRA
CVC4 0.0 1.3e-07 AUFDTLIA
Par4 0.0 1.0e-08 UFIDL
MathSAT-na-ext 0.0 0.0 QF_AUFNIA
veriT 0.0 0.0 UFLRA
MathSAT-default 0.0 0.0 QF_UFNRA

24s Performance

Solver Correct Score Time Score Division
Vampire 0.01247027 0.00618675 UF
Par4 0.00612962 0.00578198 UFNIA
Par4 0.00383819 0.00896305 QF_NIA
CVC4 0.00207978 0.00455374 LIA
Par4 0.00151092 0.01617561 AUFLIRA
Par4 0.00141212 0.0053872 LRA
Vampire 0.00127143 0.00167736 UFLIA
Vampire 0.00125658 0.00580196 AUFLIA
Vampire 0.00083977 0.00029147 UFDT
Par4 0.0006779 0.01438052 QF_BV
Par4 0.00056816 0.00385004 QF_NRA
Vampire 0.00050395 0.00012335 AUFNIRA
Yices 2.6.2 0.00032245 0.00111757 QF_LRA
CVC4 0.00031035 0.00075746 AUFDTLIA
Par4 0.0003054 0.00026397 UFBV
Vampire 0.00030038 8.395e-05 UFDTLIA
Yices 2.6.2 0.00022461 0.00188467 QF_UFIDL
COLIBRI 0.00021667 0.00056579 QF_FP
Q3B 0.00021624 0.00276962 BV
Par4 0.00021261 0.00080511 QF_IDL
Yices 2.6.2 0.00018174 0.00050895 QF_RDL
Ctrl-Ergo 0.00017358 0.00399797 QF_LIA
Par4 0.0001535 0.00017235 QF_UFNRA
Par4 8.727e-05 0.00072159 NRA
CVC4 4.808e-05 0.00158258 QF_UFNIA
CVC4 3.479e-05 6.265e-05 NIA
Yices 2.6.2 2.846e-05 0.00130973 QF_ALIA
Par4 2.76e-05 3.037e-05 UFIDL
Yices 2.6.2 2.667e-05 0.00010362 QF_AUFBV
Poolector 1.91e-05 0.00274286 QF_ABV
Yices 2.6.2 1.898e-05 0.00282803 QF_UFLIA
SMTInterpol 1.518e-05 0.00028799 ALIA
veriT 1.329e-05 0.0223922 QF_UF
Yices 2.6.2 9.52e-06 0.00173051 QF_UFLRA
Yices 2.6.2 9.49e-06 0.00613964 QF_AUFLIA
Boolector 8.64e-06 6.006e-05 QF_UFBV
Yices 2.6.2 0.0 0.00208404 QF_AX
Vampire 0.0 5.44e-06 UFDTNIA
MathSAT-default 0.0 3.04e-06 QF_AUFNIA
CVC4 0.0 2.2e-07 QF_ANIA
Yices 2.6.2 0.0 3.0e-08 QF_LIRA
veriT 0.0 0.0 UFLRA

n Non-competing.
e Experimental.