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

UF (Single Query Track)

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

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

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

Winners

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

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Vampire 0 973 1643803.315 1597569.86297339557813181318 0
CVC4 0 963 1758897.314 1773146.51696333862513281328 0
2019-CVC4n 0 944 1910988.621 1935250.83394432262213471347 0
2018-Vampiren 0 840 1813228.808 1759401.07984037846214511451 0
veriT 0 588 2077365.21 2077660.348588058817031677 25
veriT+viten 0 548 2086625.231 2086813.985548054817431496 235
Alt-Ergo 0 509 2080431.516 2062072.741509050917821674 38
z3n 0 413 1726958.333 1727292.9724136335018781108 40
SMTInterpol-fixedn 0 105 2612731.006 2612205.548105258021862174 0
UltimateEliminator+MathSAT 0 0 8276.599 5505.55300022910 0
SMTInterpol 1 104 2612727.736 2612212.162104257921872174 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Vampire 0 1008 1702696.105 1580071.11100839960912831283 0
2018-Vampiren 0 963 2340432.818 1683107.23896338058313281328 0
CVC4 0 963 1769821.134 1773088.02696333862513281328 0
2019-CVC4n 0 946 1930178.236 1935088.21394632462213451345 0
veriT 0 588 2077587.71 2077592.118588058817031677 25
veriT+viten 0 548 2086772.061 2086757.405548054817431496 235
Alt-Ergo 0 531 2162172.196 2048035.975531053117601650 38
z3n 0 413 1727169.923 1727245.9224136335018781108 40
SMTInterpol-fixedn 0 105 2648041.906 2604284.502105258021862151 0
UltimateEliminator+MathSAT 0 0 8276.599 5505.55300022910 0
SMTInterpol 1 104 2644135.176 2604052.602104257921872152 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Vampire 0 399 48599.724 20509.544399399018921283 0
2018-Vampiren 0 380 58114.677 38901.72380380019111328 0
CVC4 0 338 236920.444 239970.226338338019531328 0
2019-CVC4n 0 324 383250.437 387934.826324324019671345 0
z3n 0 63 312126.677 312138.9526363022281108 40
SMTInterpol 0 25 449505.582 445652.6582525022662152 0
SMTInterpol-fixedn 0 25 449545.292 445696.9262525022662151 0
UltimateEliminator+MathSAT 0 0 1438.868 974.19700022910 0
Alt-Ergo 0 0 434927.964 416704.77400022911650 38
veriT 0 0 489600.0 489600.000022911677 25
veriT+viten 0 0 489600.0 489600.000022911496 235

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
CVC4 0 625 90500.69 90717.8625062516661328 0
2019-CVC4n 0 622 104527.798 104753.386622062216691345 0
Vampire 0 609 204495.741 117177.895609060916821283 0
veriT 0 588 146160.29 146164.41588058817031677 25
2018-Vampiren 0 583 476247.331 203368.288583058317081328 0
veriT+viten 0 548 162687.138 162671.795548054817431496 235
Alt-Ergo 0 531 262274.905 199806.169531053117601650 38
z3n 0 350 311738.15 311748.339350035019411108 40
SMTInterpol-fixedn 0 80 729656.704 720418.5888008022112151 0
UltimateEliminator+MathSAT 0 0 2477.378 1636.73200022910 0
SMTInterpol 1 79 727004.724 720615.3477907922122152 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Vampire 0 793 41101.055 37348.41779332347014981498 0
2018-Vampiren 0 708 42853.115 39306.87170833837015831583 0
veriT+viten 0 534 43041.1 43025.434534053417571521 235
2019-CVC4n 0 516 42998.979 42976.385162748917751775 0
CVC4 0 515 42996.77 42994.0155152748817761776 0
veriT 0 467 44252.743 44252.679467046718241799 25
Alt-Ergo 0 466 46210.435 43425.886466046618251728 38
z3n 0 380 46234.752 46226.2283805932119111871 40
SMTInterpol-fixedn 0 99 52664.167 52501.65199257421922182 0
UltimateEliminator+MathSAT 0 0 8276.599 5505.55300022910 0
SMTInterpol 1 98 52674.453 52501.12698257321932182 0

n Non-competing.