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

UFDT (Single Query Track)

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

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

Benchmarks: 1223
Time Limit: 1200 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 420 1014599.95 1026503.857420101319803803 0
2019-CVC4n 0 400 1052619.543 1075890.88640083317823823 0
Vampire 0 289 1145764.967 1127406.2982890289934934 0
Alt-Ergo 0 286 1059548.866 1051576.1192860286937856 18
UltimateEliminator+MathSAT 0 0 3996.763 2815.69200012230 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
CVC4 0 420 1024172.89 1026466.907420101319803803 0
2019-CVC4n 0 400 1074414.77 1075841.18640083317823823 0
Vampire 0 327 1226988.307 1113189.02132714313896896 0
Alt-Ergo 0 296 1114919.496 1045077.2322960296927846 18
UltimateEliminator+MathSAT 0 0 3996.763 2815.69200012230 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
CVC4 0 101 46891.639 49061.87110110101122803 0
2019-CVC4n 0 83 92433.841 93578.963838301140823 0
Vampire 0 14 159981.61 120977.842141401209896 0
UltimateEliminator+MathSAT 0 0 337.099 250.02800012230 0
Alt-Ergo 0 0 79377.302 79262.6820001223846 18

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
CVC4 0 319 62881.252 63005.0363190319904803 0
2019-CVC4n 0 317 67580.929 67862.2233170317906823 0
Vampire 0 313 145406.587 77820.1493130313910896 0
Alt-Ergo 0 296 105411.867 79571.6222960296927846 18
UltimateEliminator+MathSAT 0 0 1165.814 811.63500012230 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Alt-Ergo 0 265 22771.587 21884.6712650265958879 18
2019-CVC4n 0 258 23376.306 23375.2392585253965965 0
CVC4 0 255 23468.693 23468.7592555250968968 0
Vampire 0 235 27037.1 24578.2542350235988988 0
UltimateEliminator+MathSAT 0 0 4017.481 2811.95100012231 0

n Non-competing.