SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2019

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

AUFLIRA (Single Query Track)

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

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

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
Par4Par4Par4 Vampire Par4

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
Par4 0 1601 196956.463 196929.57616015415478272 10
Z3n 0 1600 114014.906 114393.63416005415468327 7
2018-Z3n 0 1600 151356.061 151704.42416005415468347 2
CVC4 0 1560 299439.485 302020.23156001560123121 0
Vampire 0 1560 328984.747 303980.273156001560123123 0
CVC4-SymBreakn 0 1559 298994.282 303708.214155901559124122 0
Alt-Ergo 0 1506 439198.367 428684.686150601506177177 0
veriT 0 1323 845872.953 845669.876132301323360289 5
SMTInterpol 0 157 3640288.714 3575591.031157015715261468 0
UltimateEliminator+Yices-2.6.1 0 0 60210.642 59844.176000168323 0
UltimateEliminator+MathSAT-5.5.4 0 0 60314.703 57557.642000168322 0
UltimateEliminator+SMTInterpol 0 0 60367.21 57226.853000168322 0

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
Par4 0 1601196956.463196929.57616015415478272 10
Z3n 0 1600114021.376114392.63416005415468327 7
2018-Z3n 0 1600151370.151151702.80416005415468347 2
Vampire 0 1563348500.047301838.783156301563120120 0
CVC4 0 1560301933.225302014.97156001560123121 0
CVC4-SymBreakn 0 1559303469.062303702.214155901559124122 0
Alt-Ergo 0 1519485607.727412866.757151901519164161 0
veriT 0 1323845923.253845658.766132301323360289 5
SMTInterpol 0 1573983938.9643464247.127157015715261315 0
UltimateEliminator+SMTInterpol 0 060367.2157226.853000168322 0
UltimateEliminator+MathSAT-5.5.4 0 060314.70357557.642000168322 0
UltimateEliminator+Yices-2.6.1 0 062605.11159843.716000168323 0

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 542508.8532460.40654540162972 10
2018-Z3n 0 542461.5782461.58354540162947 2
Z3n 0 542463.9182461.83454540162927 7
UltimateEliminator+Yices-2.6.1 0 0185.004121.574000168323 0
UltimateEliminator+SMTInterpol 0 0210.37128.334000168322 0
UltimateEliminator+MathSAT-5.5.4 0 0207.372138.587000168322 0
CVC4 0 0128411.319128401.4820001683121 0
CVC4-SymBreakn 0 0128449.249128450.6490001683122 0
veriT 0 0129751.662129751.6590001683289 5
Alt-Ergo 0 0144930.81130434.440001683161 0
Vampire 0 0139200.09131993.910001683120 0
SMTInterpol 0 0132000.0132000.000016831315 0

UNSAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Vampire 0 156353299.95713844.873156301563120120 0
CVC4 0 156017521.90617613.488156001560123121 0
CVC4-SymBreakn 0 155919019.81319251.565155901559124122 0
Par4 0 154738447.6138469.1715470154713672 10
Z3n 0 154636477.37336477.59715460154613727 7
2018-Z3n 0 154638119.45938122.27615460154613747 2
Alt-Ergo 0 1519184676.917126432.317151901519164161 0
veriT 0 1323561386.111561120.787132301323360289 5
SMTInterpol 0 1573696542.6443177978.561157015715261315 0
UltimateEliminator+SMTInterpol 0 059925.82556954.069000168322 0
UltimateEliminator+MathSAT-5.5.4 0 059882.9257265.647000168322 0
UltimateEliminator+Yices-2.6.1 0 062190.99659569.552000168323 0

24 seconds Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
Par4 0 16012124.4632097.57616015415478272 10
Z3n 0 16001909.931907.31916005415468365 7
2018-Z3n 0 16002175.5082175.60916005415468381 2
Vampire 0 15169638.9915659.215151601516167167 0
CVC4-SymBreakn 0 14904782.0054781.607149001490193193 0
CVC4 0 14894790.3924788.378148901489194194 0
Alt-Ergo 0 14835536.6585058.654148301483200200 0
veriT 0 130113585.59613548.749130101301382377 5
SMTInterpol 0 13837575.40137406.221138013815451545 0
UltimateEliminator+SMTInterpol 0 06498.5594318.984000168327 0
UltimateEliminator+Yices-2.6.1 0 06329.9264536.488000168328 0
UltimateEliminator+MathSAT-5.5.4 0 06464.7464648.706000168327 0

n Non-competing.
Abstained: Total of benchmarks in logics in this division that solver chose to abstain from. For SAT/UNSAT scores, this column also includes benchmarks not known to be SAT/UNSAT.