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

LIA (Single Query Track)

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

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

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
CVC4CVC4CVC4 CVC4 CVC4

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Z3n 0 300 14.903 14.90530014915100 0
2018-Z3n 0 300 15.366 15.38730014915100 0
CVC4 0 300 37.661 37.56230014915100 0
Vampire 0 139 388493.95 386943.8211393136161161 0
SMTInterpol 0 105 212145.383 211506.94310589719581 0
UltimateEliminator+SMTInterpol 0 79 369450.547 368747.947792950221152 0
UltimateEliminator+MathSAT-5.5.4 0 78 369012.387 368474.22782949222153 0
veriT 0 69 6417.036 6407.376690692311 0
ProB 0 47 409637.564 420203.791471730253161 0
UltimateEliminator+Yices-2.6.1 0 41 203967.219 203312.91741103125982 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Z3n 0 300 14.903 14.90530014915100 0
2018-Z3n 0 300 15.366 15.38730014915100 0
CVC4 0 300 37.661 37.56230014915100 0
Vampire 0 140 400402.59 386287.4611403137160160 0
SMTInterpol 0 105 212145.383 211506.94310589719581 0
UltimateEliminator+SMTInterpol 0 79 369450.547 368747.947792950221152 0
UltimateEliminator+MathSAT-5.5.4 0 78 369012.387 368474.22782949222153 0
veriT 0 69 6417.206 6407.286690692311 0
ProB 0 47 409662.554 420197.431471730253161 0
UltimateEliminator+Yices-2.6.1 0 41 203967.219 203312.91741103125982 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Z3n 0 149 8.063 8.06414914901510 0
2018-Z3n 0 149 8.368 8.37714914901510 0
CVC4 0 149 30.741 30.69414914901510 0
UltimateEliminator+MathSAT-5.5.4 0 29 288510.339 288296.92429290271153 0
UltimateEliminator+SMTInterpol 0 29 289019.58 288731.87129290271152 0
ProB 0 17 278015.743 283350.27517170283161 0
UltimateEliminator+Yices-2.6.1 0 10 176705.516 176254.3991010029082 0
SMTInterpol 0 8 172052.431 171676.00988029281 0
Vampire 0 3 357600.684 350354.183330297160 0
veriT 0 0 4716.419 4706.4890003001 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Z3n 0 151 6.841 6.84115101511490 0
CVC4 0 151 6.919 6.86915101511490 0
2018-Z3n 0 151 6.999 7.0115101511490 0
Vampire 0 137 42801.907 35933.2781370137163160 0
SMTInterpol 0 97 40092.952 39830.9349709720381 0
veriT 0 69 1700.786 1700.796690692311 0
UltimateEliminator+SMTInterpol 0 50 80430.968 80016.07650050250152 0
UltimateEliminator+MathSAT-5.5.4 0 49 80502.047 80177.29649049251153 0
UltimateEliminator+Yices-2.6.1 0 31 27261.703 27058.5173103126982 0
ProB 0 30 131646.811 136847.15630030270161 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Z3n 0 300 14.903 14.90530014915100 0
2018-Z3n 0 300 15.366 15.38730014915100 0
CVC4 0 300 37.661 37.56230014915100 0
Vampire 0 137 4331.2 4034.031373134163163 0
SMTInterpol 0 105 3494.334 3245.851105897195120 0
veriT 0 69 1052.108 1041.945690692317 0
UltimateEliminator+SMTInterpol 0 69 4492.431 4222.22692445231162 0
UltimateEliminator+MathSAT-5.5.4 0 69 4504.356 4262.009692445231162 0
ProB 0 46 4870.59 4874.276461630254195 0
UltimateEliminator+Yices-2.6.1 0 41 3211.013 2807.8441103125993 0

n Non-competing.