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

UFDTLIRA (Single Query Track)

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

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

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

Winners

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

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
CVC4 0 2533 4953.858 4954.82525336924647414 0
Alt-Ergo 0 2462 138483.55 133884.894246202462812101 4
UltimateEliminator+MathSAT 0 0 10826.928 7409.41800032740 0
Vampire 29 2750 694675.493 628923.5992750102740524495 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
CVC4 0 2533 4955.088 4954.62525336924647414 0
Alt-Ergo 0 2463 138826.56 133074.278246302463811100 4
UltimateEliminator+MathSAT 0 0 10826.928 7409.41800032740 0
Vampire 29 2751 714410.153 628462.5472751102741523494 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
CVC4 0 69 1.285 1.2776969032054 0
UltimateEliminator+MathSAT 0 0 248.52 160.3400032740 0
Alt-Ergo 0 0 1209.459 1203.5160003274100 4
Vampire 29 10 40901.659 39381.417101003264494 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Vampire 0 2741 107107.864 40696.82274102741533494 0
CVC4 0 2464 4940.21 4939.7922464024648104 0
Alt-Ergo 0 2463 60897.71 57187.223246302463811100 4
UltimateEliminator+MathSAT 0 0 9063.277 6214.21100032740 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
CVC4 0 2533 251.088 250.62525336924647414 0
Alt-Ergo 0 2462 4894.803 3986.83246202462812133 4
UltimateEliminator+MathSAT 0 0 10826.928 7409.41800032740 0
Vampire 28 2343 35296.192 29391.507234302343931903 0

n Non-competing.