SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Competitions by Year

SMT-COMP 2020

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

AUFNIRA (Single Query Track)

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

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

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
CVC4Vampire Vampire Vampire

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
CVC4 0 59 284619.164 289703.2459059241237 0
Vampire 0 59 292109.1 289978.78759059241241 0
2019-Par4n 0 59 296107.865 292682.97159356241239 2
Alt-Ergo 0 39 299182.073 297365.75839039261246 1
z3n 0 38 198406.437 200470.0473843426292 4
UltimateEliminator+MathSAT 0 0 5842.497 6208.7530003004 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Vampire 0 61 301426.23 289632.90761061239239 0
CVC4 0 59 289546.994 289689.0159059241237 0
2019-Par4n 0 59 296107.865 292682.97159356241239 2
Alt-Ergo 0 40 310623.263 296479.42140040260245 1
z3n 0 38 199078.357 200465.8373843426292 4
UltimateEliminator+MathSAT 0 0 5842.497 6208.7530003004 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
z3n 0 4 0.166 0.16744029692 4
2019-Par4n 0 3 1200.02 1200.052330297239 2
UltimateEliminator+MathSAT 0 0 13.785 9.7350003004 0
CVC4 0 0 2761.162 2764.754000300237 0
Alt-Ergo 0 0 3600.14 3600.051000300245 1
Vampire 0 0 4800.0 4800.0000300239 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Vampire 0 61 19426.16 11239.41761061239239 0
CVC4 0 59 15583.39 15721.82159059241237 0
2019-Par4n 0 56 21307.845 17882.91956056244239 2
Alt-Ergo 0 40 36554.003 33506.11440040260245 1
z3n 0 34 23231.372 23437.2863403426692 4
UltimateEliminator+MathSAT 0 0 1434.22 1601.6750003004 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Vampire 0 51 6597.193 6137.14251051249249 0
2019-Par4n 0 42 6207.875 6203.77442339258256 2
CVC4 0 39 6252.871 6249.50239039261258 0
z3n 0 38 5826.7 5826.70538434262238 4
Alt-Ergo 0 35 6370.143 6193.58935035265254 1
UltimateEliminator+MathSAT 0 0 1198.772 874.340003007 0

n Non-competing.