SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2020

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

LIA (Single Query Track)

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

Page generated on 2020-07-04 11:46:58 +0000

Benchmarks: 198
Time Limit: 1200 seconds
Memory Limit: 60 GB

Winners

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

Note: the division has disagreements

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
z3n 0 198 9.388 9.4211989010800 0
2019-Z3n 0 198 9.82 9.8441989010800 0
CVC4 0 198 28.427 28.3791989010800 0
UltimateEliminator+MathSAT 0 107 54687.279 54230.27210721869144 0
Vampire 0 100 117705.432 117649.5431001999898 0
SMTInterpol-fixedn 0 71 73496.382 72975.9587176412751 0
SMTInterpol 0 71 73519.75 72989.5217176412751 0
veriT 0 42 156754.891 156587.0642042156104 0
veriT+viten 0 42 184798.26 184811.87842042156153 1

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
z3n 0 198 9.388 9.4211989010800 0
2019-Z3n 0 198 9.82 9.8441989010800 0
CVC4 0 198 28.427 28.3791989010800 0
UltimateEliminator+MathSAT 0 107 54687.279 54230.27210721869144 0
Vampire 0 100 121305.582 117645.4431001999898 0
SMTInterpol-fixedn 0 71 73496.382 72975.9587176412751 0
SMTInterpol 0 71 73519.75 72989.5217176412751 0
veriT 0 42 156762.031 156584.0442042156104 0
veriT+viten 0 42 184807.49 184807.52842042156153 1

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
z3n 0 90 4.786 4.794909001080 0
2019-Z3n 0 90 4.904 4.907909001080 0
CVC4 0 90 22.638 22.62909001080 0
UltimateEliminator+MathSAT 0 21 39923.813 39594.912121017744 0
SMTInterpol-fixedn 0 7 57760.433 57415.94677019151 0
SMTInterpol 0 7 57772.377 57421.45877019151 0
Vampire 0 1 110400.273 106795.97411019798 0
veriT 0 0 99996.24 99996.887000198104 0
veriT+viten 0 0 106807.049 106807.048000198153 1

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
z3n 0 108 4.602 4.6271080108900 0
2019-Z3n 0 108 4.916 4.9371080108900 0
CVC4 0 108 5.79 5.7591080108900 0
Vampire 0 99 10905.31 10849.468990999998 0
UltimateEliminator+MathSAT 0 86 14763.466 14635.3628608611244 0
SMTInterpol-fixedn 0 64 15735.949 15560.0136406413451 0
SMTInterpol 0 64 15747.373 15568.0626406413451 0
veriT 0 42 56765.791 56587.15342042156104 0
veriT+viten 0 42 78000.441 78000.4842042156153 1

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
z3n 0 198 9.388 9.4211989010800 0
2019-Z3n 0 198 9.82 9.8441989010800 0
CVC4 0 198 28.427 28.3791989010800 0
UltimateEliminator+MathSAT 0 106 1934.805 1645.71310620869251 0
Vampire 0 100 2457.432 2401.5431001999898 0
SMTInterpol-fixedn 0 71 2249.73 2080.2777176412778 0
SMTInterpol 0 71 2266.344 2083.567176412778 0
veriT+viten 0 42 3703.49 3703.52842042156153 1
veriT 0 42 3720.59 3720.58442042156155 0

n Non-competing.