SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Previous Competitions
SMT-LIB

SMT-COMP 2019

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

UFDT (Single Query Track)

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

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

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

Winners

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

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
CVC4 0 531 2530904.251 2572747.26753111941210161016 0
2018-CVC4n 0 524 2501494.731 2524970.85752411740710231023 0
Vampire 0 415 2815750.367 2741769.3934155735811321132 0
Alt-Ergo 0 358 2688207.92 2671802.402358035811891061 49

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
CVC4 0 531 2569194.511 2572700.61753111941210161016 0
2018-CVC4n 0 524 2522848.211 2524926.06752411740710231023 0
Vampire 0 434 3060141.567 2718249.8074345837611131113 0
Alt-Ergo 0 372 2876046.16 2652558.061372037211751046 49

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
CVC4 0 119 187244.669 190394.12119119014281016 0
2018-CVC4n 0 117 140962.56 142742.238117117014301023 0
Vampire 0 58 296449.028 245203.0675858014891113 0
Alt-Ergo 0 0 250175.238 231943.87400015471046 49

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
CVC4 0 412 113949.842 114306.496412041211351016 0
2018-CVC4n 0 407 113885.651 114183.83407040711401023 0
Vampire 0 376 330089.529 205198.92376037611711113 0
Alt-Ergo 0 372 280927.181 199851.698372037211751046 49

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Alt-Ergo 0 337 29045.785 27809.545337033712101090 49
2018-CVC4n 0 327 29573.65 29573.583327332412201220 0
CVC4 0 326 29551.074 29550.992326332312211221 0
Vampire 0 277 35508.944 31772.901277027712701270 0

n Non-competing.