SMT-COMP 2019

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

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

Previous Competitions

SMT-LIB

LRA (Single Query Track)

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

Page generated on 2019-07-23 17:56:09 +0000

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
Par4Par4Par4 Par4 Par4

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Z3n 0 945 223885.451 223926.7119453685775858 0
Par4 0 941 191786.877 170445.2699413715706262 0
2018-Z3n 0 931 263064.491 263064.5019313665657272 0
CVC4 0 815 527431.59 532098.4815312503188188 0
UltimateEliminator+SMTInterpol 0 654 863725.43 859053.7654222432349348 0
UltimateEliminator+MathSAT-5.5.4 0 650 871513.733 868354.119650222428353351 0
UltimateEliminator+Yices-2.6.1 0 366 129268.51 132382.00236614721963754 0
Vampire 0 223 1936562.617 1888283.8732230223780780 0
SMTInterpol 0 152 66069.515 63342.322152314985120 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 959 208579.777 157110.1299593745854444 0
Z3n 0 945 223907.291 223924.4019453685775858 0
2018-Z3n 0 931 263071.751 263062.4819313665657272 0
CVC4 0 815 530547.78 532089.07815312503188188 0
UltimateEliminator+SMTInterpol 0 654 863725.43 859053.7654222432349348 0
UltimateEliminator+MathSAT-5.5.4 0 650 871513.733 868354.119650222428353351 0
UltimateEliminator+Yices-2.6.1 0 366 134056.58 132381.40236614721963754 0
Vampire 0 228 1996128.137 1882520.7962280228775775 0
SMTInterpol 0 152 66069.515 63342.322152314985120 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 374 28756.231 16844.534374374062944 0
Z3n 0 368 34444.35 34445.772368368063558 0
2018-Z3n 0 366 41246.388 41247.195366366063772 0
CVC4 0 312 185842.04 186748.6913123120691188 0
UltimateEliminator+SMTInterpol 0 222 374836.13 373711.2712222220781348 0
UltimateEliminator+MathSAT-5.5.4 0 222 375949.478 374764.522222220781351 0
UltimateEliminator+Yices-2.6.1 0 147 102614.377 101963.856147147085654 0
SMTInterpol 0 3 50151.281 48972.237330100020 0
Vampire 0 0 931201.2 901778.120001003775 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 585 110223.546 70665.596585058541844 0
Z3n 0 577 119862.941 119878.629577057742658 0
2018-Z3n 0 565 152225.363 152215.286565056543872 0
CVC4 0 503 275105.74 275740.3795030503500188 0
UltimateEliminator+SMTInterpol 0 432 419289.3 415742.4284320432571348 0
UltimateEliminator+MathSAT-5.5.4 0 428 425964.255 423989.5994280428575351 0
Vampire 0 228 995326.937 911142.6762280228775775 0
UltimateEliminator+Yices-2.6.1 0 219 28859.549 27915.927219021978454 0
SMTInterpol 0 149 14950.363 13509.312149014985420 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 851 5341.94 4546.927851337514152152 0
Z3n 0 783 6882.257 6883.06783332451220220 0
2018-Z3n 0 749 7934.34 7920.521749319430254254 0
CVC4 0 704 7436.468 7437.749704272432299299 0
UltimateEliminator+SMTInterpol 0 577 14632.563 12400.84577204373426426 0
UltimateEliminator+MathSAT-5.5.4 0 576 13832.946 12379.637576204372427427 0
UltimateEliminator+Yices-2.6.1 0 365 5494.646 3890.21136514621963860 0
SMTInterpol 0 148 4987.587 3137.887148314585579 0
Vampire 0 141 21876.9 21012.0961410141862862 0

n Non-competing.