SMT-COMP 2019

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Papers
Benchmark submission
Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

Previous

SMT-LIB

ALIA (Single Query Track)

Competition results for the ALIA division in the Single Query Track.

Page generated on 2019-07-07 12:14:30 +0000

Benchmarks: 19
Time Limit: 2400 seconds
Memory Limit: 60 GB

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
SMTInterpol SMTInterpol SMTInterpol Alt-Ergo CVC4

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Timeout Memout
2018-Z3n 0 19 1.165 1.166 19 1 18 0 0 0
Z3n 0 19 1.244 1.244 19 1 18 0 0 0
SMTInterpol 0 19 1092.681 978.138 19 1 18 0 0 0
CVC4 0 18 4.744 4.735 18 0 18 1 0 0
Alt-Ergo 0 18 2409.881 2404.416 18 0 18 1 1 0
Vampire 0 13 18018.486 15312.524 13 0 13 6 6 0
veriT 0 4 35996.46 36000.729 4 0 4 15 15 0
UltimateEliminator+SMTInterpol 0 0 28908.211 28859.186 0 0 0 19 12 0
UltimateEliminator+Yices-2.6.1 0 0 28946.248 28876.786 0 0 0 19 12 0
UltimateEliminator+MathSAT-5.5.4 0 0 28949.546 28877.51 0 0 0 19 12 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Timeout Memout
2018-Z3n 0 19 1.165 1.166 19 1 18 0 0 0
Z3n 0 19 1.244 1.244 19 1 18 0 0 0
SMTInterpol 0 19 1092.681 978.138 19 1 18 0 0 0
CVC4 0 18 4.744 4.735 18 0 18 1 0 0
Alt-Ergo 0 18 2409.881 2404.416 18 0 18 1 1 0
Vampire 0 15 28678.916 14507.914 15 0 15 4 4 0
veriT 0 4 36000.07 36000.069 4 0 4 15 15 0
UltimateEliminator+Yices-2.6.1 0 0 44351.318 27591.446 0 0 0 19 9 0
UltimateEliminator+MathSAT-5.5.4 0 0 45313.206 27841.39 0 0 0 19 9 0
UltimateEliminator+SMTInterpol 0 0 39040.021 27967.956 0 0 0 19 10 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Timeout Memout
2018-Z3n 0 1 0.055 0.055 1 1 0 18 0 0
Z3n 0 1 0.056 0.056 1 1 0 18 0 0
SMTInterpol 0 1 1.383 0.59 1 1 0 18 0 0
CVC4 0 0 0.279 0.277 0 0 0 19 0 0
UltimateEliminator+SMTInterpol 0 0 3.344 2.269 0 0 0 19 10 0
UltimateEliminator+Yices-2.6.1 0 0 3.295 2.359 0 0 0 19 9 0
UltimateEliminator+MathSAT-5.5.4 0 0 3.39 2.363 0 0 0 19 9 0
Alt-Ergo 0 0 2400.0 2400.0 0 0 0 19 1 0
Vampire 0 0 2400.0 2400.0 0 0 0 19 4 0
veriT 0 0 2400.0 2400.0 0 0 0 19 15 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Timeout Memout
2018-Z3n 0 18 1.11 1.111 18 0 18 1 0 0
Z3n 0 18 1.187 1.188 18 0 18 1 0 0
Alt-Ergo 0 18 9.881 4.416 18 0 18 1 1 0
CVC4 0 18 4.465 4.458 18 0 18 1 0 0
SMTInterpol 0 18 1091.298 977.547 18 0 18 1 0 0
Vampire 0 15 26278.916 12107.914 15 0 15 4 4 0
veriT 0 4 33600.07 33600.069 4 0 4 15 15 0
UltimateEliminator+Yices-2.6.1 0 0 44348.023 27589.087 0 0 0 19 9 0
UltimateEliminator+MathSAT-5.5.4 0 0 45309.816 27839.027 0 0 0 19 9 0
UltimateEliminator+SMTInterpol 0 0 39036.677 27965.687 0 0 0 19 10 0

24s Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Timeout Memout
2018-Z3n 0 19 1.165 1.166 19 1 18 0 0 0
Z3n 0 19 1.244 1.244 19 1 18 0 0 0
CVC4 0 18 4.744 4.735 18 0 18 1 0 0
Alt-Ergo 0 18 33.881 28.416 18 0 18 1 1 0
SMTInterpol 0 14 230.497 176.726 14 1 13 5 5 0
Vampire 0 5 364.996 343.786 5 0 5 14 14 0
veriT 0 4 360.07 360.069 4 0 4 15 15 0
UltimateEliminator+SMTInterpol 0 0 344.452 332.342 0 0 0 19 13 0
UltimateEliminator+Yices-2.6.1 0 0 343.827 333.439 0 0 0 19 13 0
UltimateEliminator+MathSAT-5.5.4 0 0 344.049 333.44 0 0 0 19 13 0

n Non-competing.