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

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 UNSATUnsolvedTimeout 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 Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 1601 196956.463 196929.57616015415478272 10
Z3n 0 1600 114021.376 114392.63416005415468327 7
2018-Z3n 0 1600 151370.151 151702.80416005415468347 2
Vampire 0 1563 348500.047 301838.783156301563120120 0
CVC4 0 1560 301933.225 302014.97156001560123121 0
CVC4-SymBreakn 0 1559 303469.062 303702.214155901559124122 0
Alt-Ergo 0 1519 485607.727 412866.757151901519164161 0
veriT 0 1323 845923.253 845658.766132301323360289 5
SMTInterpol 0 157 3983938.964 3464247.127157015715261315 0
UltimateEliminator+SMTInterpol 0 0 60367.21 57226.853000168322 0
UltimateEliminator+MathSAT-5.5.4 0 0 60314.703 57557.642000168322 0
UltimateEliminator+Yices-2.6.1 0 0 62605.111 59843.716000168323 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 54 2508.853 2460.40654540162972 10
2018-Z3n 0 54 2461.578 2461.58354540162947 2
Z3n 0 54 2463.918 2461.83454540162927 7
UltimateEliminator+Yices-2.6.1 0 0 185.004 121.574000168323 0
UltimateEliminator+SMTInterpol 0 0 210.37 128.334000168322 0
UltimateEliminator+MathSAT-5.5.4 0 0 207.372 138.587000168322 0
CVC4 0 0 128411.319 128401.4820001683121 0
CVC4-SymBreakn 0 0 128449.249 128450.6490001683122 0
veriT 0 0 129751.662 129751.6590001683289 5
Alt-Ergo 0 0 144930.81 130434.440001683161 0
Vampire 0 0 139200.09 131993.910001683120 0
SMTInterpol 0 0 132000.0 132000.000016831315 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Vampire 0 1563 53299.957 13844.873156301563120120 0
CVC4 0 1560 17521.906 17613.488156001560123121 0
CVC4-SymBreakn 0 1559 19019.813 19251.565155901559124122 0
Par4 0 1547 38447.61 38469.1715470154713672 10
Z3n 0 1546 36477.373 36477.59715460154613727 7
2018-Z3n 0 1546 38119.459 38122.27615460154613747 2
Alt-Ergo 0 1519 184676.917 126432.317151901519164161 0
veriT 0 1323 561386.111 561120.787132301323360289 5
SMTInterpol 0 157 3696542.644 3177978.561157015715261315 0
UltimateEliminator+SMTInterpol 0 0 59925.825 56954.069000168322 0
UltimateEliminator+MathSAT-5.5.4 0 0 59882.92 57265.647000168322 0
UltimateEliminator+Yices-2.6.1 0 0 62190.996 59569.552000168323 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 1601 2124.463 2097.57616015415478272 10
Z3n 0 1600 1909.93 1907.31916005415468365 7
2018-Z3n 0 1600 2175.508 2175.60916005415468381 2
Vampire 0 1516 9638.991 5659.215151601516167167 0
CVC4-SymBreakn 0 1490 4782.005 4781.607149001490193193 0
CVC4 0 1489 4790.392 4788.378148901489194194 0
Alt-Ergo 0 1483 5536.658 5058.654148301483200200 0
veriT 0 1301 13585.596 13548.749130101301382377 5
SMTInterpol 0 138 37575.401 37406.221138013815451545 0
UltimateEliminator+SMTInterpol 0 0 6498.559 4318.984000168327 0
UltimateEliminator+Yices-2.6.1 0 0 6329.926 4536.488000168328 0
UltimateEliminator+MathSAT-5.5.4 0 0 6464.746 4648.706000168327 0

n Non-competing.