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

UFDTLIA (Single Query Track)

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

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

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
CVC4CVC4 CVC4 Vampire

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
CVC4 0 218 290409.33 301270.72221802188181 0
2018-CVC4n 0 216 245802.84 253041.58521602168380 0
Vampire 0 69 559145.131 553796.74969069230230 0
Alt-Ergo 0 55 588624.761 586366.7555055244241 3

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
CVC4 0 218 299670.46 301267.23221802188181 0
2018-CVC4n 0 216 251739.82 253038.45521602168380 0
Vampire 0 69 566345.341 553786.00969069230230 0
Alt-Ergo 0 58 599427.171 581788.35858058241238 3

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-CVC4n 0 0 0.0 0.000029980 0
Alt-Ergo 0 0 0.0 0.0000299238 3
CVC4 0 0 0.0 0.000029981 0
Vampire 0 0 0.0 0.0000299230 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
CVC4 0 218 107670.46 109267.23221802188181 0
2018-CVC4n 0 216 61787.33 62936.10521602168380 0
Vampire 0 69 374345.341 361786.00969069230230 0
Alt-Ergo 0 58 407427.171 389788.35858058241238 3

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Vampire 0 58 6178.411 5891.81358058241241 0
Alt-Ergo 0 53 6024.551 5937.38753053246243 3
CVC4 0 48 6052.263 6052.24648048251251 0
2018-CVC4n 0 46 6100.336 6097.71146046253253 0

n Non-competing.