The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_BV division in the Challenge Track (non-incremental).
Page generated on 2019-07-23 17:57:29 +0000
Benchmarks: 7 Time Limit: 43200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Boolector | Minkeyrink Solver MT | Minkeyrink Solver MT | — | Minkeyrink Solver MT |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2018-Boolectorn | 0 | 7 | 607.673 | 607.763 | 7 | 7 | 0 | 0 | 0 | 0 | |
| Boolector | 0 | 7 | 708.912 | 708.962 | 7 | 7 | 0 | 0 | 0 | 0 | |
| Yices 2.6.2 CaDiCal | 0 | 7 | 716.181 | 716.265 | 7 | 7 | 0 | 0 | 0 | 0 | |
| Minkeyrink Solver MT | 0 | 7 | 767.592 | 443.43 | 7 | 7 | 0 | 0 | 0 | 0 | |
| Yices 2.6.2 New Bvsolver | 0 | 7 | 1111.014 | 1111.251 | 7 | 7 | 0 | 0 | 0 | 0 | |
| Minkeyrink Solver | 0 | 7 | 1150.653 | 1150.725 | 7 | 7 | 0 | 0 | 0 | 0 | |
| 2018-Minkeyrink MTn | 0 | 7 | 1324.014 | 536.015 | 7 | 7 | 0 | 0 | 0 | 0 | |
| Poolector | 0 | 7 | 2367.829 | 640.2 | 7 | 7 | 0 | 0 | 0 | 0 | |
| Yices 2.6.2 Cryptominisat | 0 | 7 | 8453.778 | 8454.789 | 7 | 7 | 0 | 0 | 0 | 0 | |
| Yices 2.6.2 | 0 | 7 | 12696.426 | 12697.884 | 7 | 7 | 0 | 0 | 0 | 0 | |
| Z3n | 0 | 7 | 31544.226 | 31546.583 | 7 | 7 | 0 | 0 | 0 | 0 | |
| STP-minisat | 0 | 7 | 43053.772 | 43054.445 | 7 | 7 | 0 | 0 | 0 | 0 | |
| STP | 0 | 7 | 43468.136 | 43471.548 | 7 | 7 | 0 | 0 | 0 | 0 | |
| STP-mergesat-fixedn | 0 | 6 | 8134.53 | 8135.15 | 6 | 6 | 0 | 1 | 1 | 0 | |
| STP-portfolio-fixedn | 0 | 6 | 10278.826 | 8184.243 | 6 | 6 | 0 | 1 | 1 | 0 | |
| CVC4 | 0 | 6 | 44063.069 | 44064.673 | 6 | 6 | 0 | 1 | 1 | 0 | |
| STP-mt | 0 | 6 | 44113.041 | 43499.469 | 6 | 6 | 0 | 1 | 1 | 0 | |
| STP-mergesat | 0 | 0 | 42262.973 | 42266.205 | 0 | 0 | 0 | 7 | 0 | 0 | |
| STP-riss | 0 | 0 | 42962.673 | 42969.068 | 0 | 0 | 0 | 7 | 0 | 0 | |
| STP-portfolio | 0 | 0 | 44986.465 | 44248.771 | 0 | 0 | 0 | 7 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Minkeyrink Solver MT | 0 | 7 | 767.592 | 443.43 | 7 | 7 | 0 | 0 | 0 | 0 | |
| 2018-Minkeyrink MTn | 0 | 7 | 1324.014 | 536.015 | 7 | 7 | 0 | 0 | 0 | 0 | |
| 2018-Boolectorn | 0 | 7 | 607.673 | 607.763 | 7 | 7 | 0 | 0 | 0 | 0 | |
| Poolector | 0 | 7 | 2367.829 | 640.2 | 7 | 7 | 0 | 0 | 0 | 0 | |
| Boolector | 0 | 7 | 708.912 | 708.962 | 7 | 7 | 0 | 0 | 0 | 0 | |
| Yices 2.6.2 CaDiCal | 0 | 7 | 716.181 | 716.265 | 7 | 7 | 0 | 0 | 0 | 0 | |
| Yices 2.6.2 New Bvsolver | 0 | 7 | 1111.014 | 1111.251 | 7 | 7 | 0 | 0 | 0 | 0 | |
| Minkeyrink Solver | 0 | 7 | 1150.653 | 1150.725 | 7 | 7 | 0 | 0 | 0 | 0 | |
| Yices 2.6.2 Cryptominisat | 0 | 7 | 8453.778 | 8454.789 | 7 | 7 | 0 | 0 | 0 | 0 | |
| Yices 2.6.2 | 0 | 7 | 12696.426 | 12697.884 | 7 | 7 | 0 | 0 | 0 | 0 | |
| Z3n | 0 | 7 | 31544.226 | 31546.583 | 7 | 7 | 0 | 0 | 0 | 0 | |
| STP-minisat | 0 | 7 | 43053.772 | 43054.445 | 7 | 7 | 0 | 0 | 0 | 0 | |
| STP | 0 | 7 | 43468.136 | 43471.548 | 7 | 7 | 0 | 0 | 0 | 0 | |
| STP-mergesat-fixedn | 0 | 6 | 8134.53 | 8135.15 | 6 | 6 | 0 | 1 | 1 | 0 | |
| STP-portfolio-fixedn | 0 | 6 | 10278.826 | 8184.243 | 6 | 6 | 0 | 1 | 1 | 0 | |
| STP-mt | 0 | 6 | 44113.041 | 43499.469 | 6 | 6 | 0 | 1 | 1 | 0 | |
| CVC4 | 0 | 6 | 44064.469 | 44064.573 | 6 | 6 | 0 | 1 | 1 | 0 | |
| STP-mergesat | 0 | 0 | 42262.973 | 42266.205 | 0 | 0 | 0 | 7 | 0 | 0 | |
| STP-riss | 0 | 0 | 42962.673 | 42969.068 | 0 | 0 | 0 | 7 | 0 | 0 | |
| STP-portfolio | 0 | 0 | 44986.465 | 44248.771 | 0 | 0 | 0 | 7 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Minkeyrink Solver MT | 0 | 7 | 767.592 | 443.43 | 7 | 7 | 0 | 0 | 0 | 0 |
| 2018-Minkeyrink MTn | 0 | 7 | 1324.014 | 536.015 | 7 | 7 | 0 | 0 | 0 | 0 |
| 2018-Boolectorn | 0 | 7 | 607.673 | 607.763 | 7 | 7 | 0 | 0 | 0 | 0 |
| Poolector | 0 | 7 | 2367.829 | 640.2 | 7 | 7 | 0 | 0 | 0 | 0 |
| Boolector | 0 | 7 | 708.912 | 708.962 | 7 | 7 | 0 | 0 | 0 | 0 |
| Yices 2.6.2 CaDiCal | 0 | 7 | 716.181 | 716.265 | 7 | 7 | 0 | 0 | 0 | 0 |
| Yices 2.6.2 New Bvsolver | 0 | 7 | 1111.014 | 1111.251 | 7 | 7 | 0 | 0 | 0 | 0 |
| Minkeyrink Solver | 0 | 7 | 1150.653 | 1150.725 | 7 | 7 | 0 | 0 | 0 | 0 |
| Yices 2.6.2 Cryptominisat | 0 | 7 | 8453.778 | 8454.789 | 7 | 7 | 0 | 0 | 0 | 0 |
| Yices 2.6.2 | 0 | 7 | 12696.426 | 12697.884 | 7 | 7 | 0 | 0 | 0 | 0 |
| Z3n | 0 | 7 | 31544.226 | 31546.583 | 7 | 7 | 0 | 0 | 0 | 0 |
| STP-minisat | 0 | 7 | 43053.772 | 43054.445 | 7 | 7 | 0 | 0 | 0 | 0 |
| STP | 0 | 7 | 43468.136 | 43471.548 | 7 | 7 | 0 | 0 | 0 | 0 |
| STP-mergesat-fixedn | 0 | 6 | 8134.53 | 8135.15 | 6 | 6 | 0 | 1 | 1 | 0 |
| STP-portfolio-fixedn | 0 | 6 | 10278.826 | 8184.243 | 6 | 6 | 0 | 1 | 1 | 0 |
| STP-mt | 0 | 6 | 44113.041 | 43499.469 | 6 | 6 | 0 | 1 | 1 | 0 |
| CVC4 | 0 | 6 | 44064.469 | 44064.573 | 6 | 6 | 0 | 1 | 1 | 0 |
| STP-mergesat | 0 | 0 | 42262.973 | 42266.205 | 0 | 0 | 0 | 7 | 0 | 0 |
| STP-riss | 0 | 0 | 42962.673 | 42969.068 | 0 | 0 | 0 | 7 | 0 | 0 |
| STP-portfolio | 0 | 0 | 44986.465 | 44248.771 | 0 | 0 | 0 | 7 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2018-Boolectorn | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 7 | 0 | 0 |
| 2018-Minkeyrink MTn | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 7 | 0 | 0 |
| Boolector | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 7 | 0 | 0 |
| CVC4 | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 7 | 1 | 0 |
| Minkeyrink Solver | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 7 | 0 | 0 |
| Minkeyrink Solver MT | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 7 | 0 | 0 |
| Poolector | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 7 | 0 | 0 |
| STP | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 7 | 0 | 0 |
| STP-mergesat | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 7 | 0 | 0 |
| STP-minisat | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 7 | 0 | 0 |
| STP-mt | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 7 | 1 | 0 |
| STP-portfolio | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 7 | 0 | 0 |
| STP-riss | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 7 | 0 | 0 |
| Yices 2.6.2 | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 7 | 0 | 0 |
| Yices 2.6.2 CaDiCal | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 7 | 0 | 0 |
| Yices 2.6.2 Cryptominisat | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 7 | 0 | 0 |
| Yices 2.6.2 New Bvsolver | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 7 | 0 | 0 |
| Z3n | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 7 | 0 | 0 |
| STP-mergesat-fixedn | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 7 | 1 | 0 |
| STP-portfolio-fixedn | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 7 | 1 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Minkeyrink Solver MT | 0 | 4 | 194.556 | 129.72 | 4 | 4 | 0 | 3 | 3 | 0 | |
| STP-mt | 0 | 3 | 136.029 | 117.555 | 3 | 3 | 0 | 4 | 4 | 0 | |
| 2018-Minkeyrink MTn | 0 | 3 | 203.363 | 133.496 | 3 | 3 | 0 | 4 | 4 | 0 | |
| Minkeyrink Solver | 0 | 2 | 143.674 | 143.676 | 2 | 2 | 0 | 5 | 5 | 0 | |
| Z3n | 0 | 2 | 145.367 | 145.367 | 2 | 2 | 0 | 5 | 5 | 0 | |
| 2018-Boolectorn | 0 | 2 | 156.169 | 156.176 | 2 | 2 | 0 | 5 | 5 | 0 | |
| Poolector | 0 | 2 | 263.006 | 156.362 | 2 | 2 | 0 | 5 | 5 | 0 | |
| STP | 0 | 1 | 150.84 | 150.842 | 1 | 1 | 0 | 6 | 6 | 0 | |
| Boolector | 0 | 1 | 159.007 | 159.009 | 1 | 1 | 0 | 6 | 6 | 0 | |
| STP-minisat | 0 | 1 | 160.925 | 160.925 | 1 | 1 | 0 | 6 | 6 | 0 | |
| Yices 2.6.2 CaDiCal | 0 | 1 | 161.719 | 161.718 | 1 | 1 | 0 | 6 | 6 | 0 | |
| STP-mergesat | 0 | 0 | 65.273 | 65.305 | 0 | 0 | 0 | 7 | 1 | 0 | |
| STP-riss | 0 | 0 | 69.073 | 74.668 | 0 | 0 | 0 | 7 | 1 | 0 | |
| STP-portfolio | 0 | 0 | 162.852 | 161.132 | 0 | 0 | 0 | 7 | 6 | 0 | |
| CVC4 | 0 | 0 | 168.0 | 168.0 | 0 | 0 | 0 | 7 | 7 | 0 | |
| Yices 2.6.2 | 0 | 0 | 168.0 | 168.0 | 0 | 0 | 0 | 7 | 7 | 0 | |
| Yices 2.6.2 Cryptominisat | 0 | 0 | 168.0 | 168.0 | 0 | 0 | 0 | 7 | 7 | 0 | |
| Yices 2.6.2 New Bvsolver | 0 | 0 | 168.0 | 168.0 | 0 | 0 | 0 | 7 | 7 | 0 | |
| STP-mergesat-fixedn | 0 | 0 | 168.0 | 168.0 | 0 | 0 | 0 | 7 | 7 | 0 | |
| STP-portfolio-fixedn | 0 | 0 | 168.0 | 168.0 | 0 | 0 | 0 | 7 | 7 | 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.