SMT-COMP 2019

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Papers
Benchmark submission
Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

Previous

SMT-LIB

AUFLIRA (Single Query Track)

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

Page generated on 2019-07-07 12:14:30 +0000

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

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
Par4 Par4 Par4 Vampire Par4

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Timeout Memout
Par4 0 1601 196956.463 196929.576 1601 54 1547 82 72 10
Z3n 0 1600 114014.906 114393.634 1600 54 1546 83 27 7
2018-Z3n 0 1600 151356.061 151704.424 1600 54 1546 83 47 2
CVC4 0 1560 299439.485 302020.23 1560 0 1560 123 121 0
Vampire 0 1560 328984.747 303980.273 1560 0 1560 123 123 0
CVC4-SymBreakn 0 1559 298994.282 303708.214 1559 0 1559 124 122 0
Alt-Ergo 0 1506 439198.367 428684.686 1506 0 1506 177 177 0
veriT 0 1323 845872.953 845669.876 1323 0 1323 360 289 5
SMTInterpol 0 157 3640288.714 3575591.031 157 0 157 1526 1468 0
UltimateEliminator+Yices-2.6.1 0 0 60210.642 59844.176 0 0 0 1683 23 0
UltimateEliminator+MathSAT-5.5.4 0 0 60314.703 57557.642 0 0 0 1683 22 0
UltimateEliminator+SMTInterpol 0 0 60367.21 57226.853 0 0 0 1683 22 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Timeout Memout
Par4 0 1601 196956.463 196929.576 1601 54 1547 82 72 10
Z3n 0 1600 114021.376 114392.634 1600 54 1546 83 27 7
2018-Z3n 0 1600 151370.151 151702.804 1600 54 1546 83 47 2
Vampire 0 1563 348500.047 301838.783 1563 0 1563 120 120 0
CVC4 0 1560 301933.225 302014.97 1560 0 1560 123 121 0
CVC4-SymBreakn 0 1559 303469.062 303702.214 1559 0 1559 124 122 0
Alt-Ergo 0 1519 485607.727 412866.757 1519 0 1519 164 161 0
veriT 0 1323 845923.253 845658.766 1323 0 1323 360 289 5
SMTInterpol 0 157 3983938.964 3464247.127 157 0 157 1526 1315 0
UltimateEliminator+SMTInterpol 0 0 60367.21 57226.853 0 0 0 1683 22 0
UltimateEliminator+MathSAT-5.5.4 0 0 60314.703 57557.642 0 0 0 1683 22 0
UltimateEliminator+Yices-2.6.1 0 0 62605.111 59843.716 0 0 0 1683 23 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Timeout Memout
Par4 0 54 2508.853 2460.406 54 54 0 1629 72 10
2018-Z3n 0 54 2461.578 2461.583 54 54 0 1629 47 2
Z3n 0 54 2463.918 2461.834 54 54 0 1629 27 7
UltimateEliminator+Yices-2.6.1 0 0 185.004 121.574 0 0 0 1683 23 0
UltimateEliminator+SMTInterpol 0 0 210.37 128.334 0 0 0 1683 22 0
UltimateEliminator+MathSAT-5.5.4 0 0 207.372 138.587 0 0 0 1683 22 0
CVC4 0 0 128411.319 128401.482 0 0 0 1683 121 0
CVC4-SymBreakn 0 0 128449.249 128450.649 0 0 0 1683 122 0
veriT 0 0 129751.662 129751.659 0 0 0 1683 289 5
Alt-Ergo 0 0 144930.81 130434.44 0 0 0 1683 161 0
Vampire 0 0 139200.09 131993.91 0 0 0 1683 120 0
SMTInterpol 0 0 132000.0 132000.0 0 0 0 1683 1315 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Timeout Memout
Vampire 0 1563 53299.957 13844.873 1563 0 1563 120 120 0
CVC4 0 1560 17521.906 17613.488 1560 0 1560 123 121 0
CVC4-SymBreakn 0 1559 19019.813 19251.565 1559 0 1559 124 122 0
Par4 0 1547 38447.61 38469.17 1547 0 1547 136 72 10
Z3n 0 1546 36477.373 36477.597 1546 0 1546 137 27 7
2018-Z3n 0 1546 38119.459 38122.276 1546 0 1546 137 47 2
Alt-Ergo 0 1519 184676.917 126432.317 1519 0 1519 164 161 0
veriT 0 1323 561386.111 561120.787 1323 0 1323 360 289 5
SMTInterpol 0 157 3696542.644 3177978.561 157 0 157 1526 1315 0
UltimateEliminator+SMTInterpol 0 0 59925.825 56954.069 0 0 0 1683 22 0
UltimateEliminator+MathSAT-5.5.4 0 0 59882.92 57265.647 0 0 0 1683 22 0
UltimateEliminator+Yices-2.6.1 0 0 62190.996 59569.552 0 0 0 1683 23 0

24s Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Timeout Memout
Par4 0 1601 2124.463 2097.576 1601 54 1547 82 72 10
Z3n 0 1600 1909.93 1907.319 1600 54 1546 83 65 7
2018-Z3n 0 1600 2175.508 2175.609 1600 54 1546 83 81 2
Vampire 0 1516 9638.991 5659.215 1516 0 1516 167 167 0
CVC4-SymBreakn 0 1490 4782.005 4781.607 1490 0 1490 193 193 0
CVC4 0 1489 4790.392 4788.378 1489 0 1489 194 194 0
Alt-Ergo 0 1483 5536.658 5058.654 1483 0 1483 200 200 0
veriT 0 1301 13585.596 13548.749 1301 0 1301 382 377 5
SMTInterpol 0 138 37575.401 37406.221 138 0 138 1545 1545 0
UltimateEliminator+SMTInterpol 0 0 6498.559 4318.984 0 0 0 1683 27 0
UltimateEliminator+Yices-2.6.1 0 0 6329.926 4536.488 0 0 0 1683 28 0
UltimateEliminator+MathSAT-5.5.4 0 0 6464.746 4648.706 0 0 0 1683 27 0

n Non-competing.