The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_UFNRA division in the Single Query Track.
Page generated on 2019-07-23 17:56:09 +0000
Benchmarks: 26 Time Limit: 2400 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Par4 | Par4 | Par4 | MathSAT-default | Par4 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 25 | 8616.659 | 5510.484 | 25 | 23 | 2 | 1 | 1 | 0 | |
| 2018-Yicesn | 0 | 25 | 15890.008 | 15891.041 | 25 | 23 | 2 | 1 | 1 | 0 | |
| Yices 2.6.2 | 0 | 24 | 15942.9 | 15944.223 | 24 | 22 | 2 | 2 | 2 | 0 | |
| Z3n | 0 | 20 | 321.653 | 321.687 | 20 | 18 | 2 | 6 | 0 | 0 | |
| CVC4 | 0 | 12 | 34865.887 | 34871.981 | 12 | 10 | 2 | 14 | 14 | 0 | |
| MathSAT-default | 0 | 9 | 40876.429 | 40879.303 | 9 | 7 | 2 | 17 | 17 | 0 | |
| MathSAT-na-ext | 0 | 9 | 41418.613 | 41421.036 | 9 | 7 | 2 | 17 | 17 | 0 | |
| veriT+raSAT+Redlog | 0 | 0 | 62390.64 | 62401.02 | 0 | 0 | 0 | 26 | 26 | 0 | |
| Alt-Ergo | 0 | 0 | 62400.0 | 62400.0 | 0 | 0 | 0 | 26 | 26 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 26 | 10778.819 | 5391.934 | 26 | 24 | 2 | 0 | 0 | 0 | |
| 2018-Yicesn | 0 | 25 | 15890.048 | 15891.011 | 25 | 23 | 2 | 1 | 1 | 0 | |
| Yices 2.6.2 | 0 | 24 | 15943.27 | 15944.163 | 24 | 22 | 2 | 2 | 2 | 0 | |
| Z3n | 0 | 20 | 321.653 | 321.687 | 20 | 18 | 2 | 6 | 0 | 0 | |
| CVC4 | 0 | 12 | 34870.737 | 34871.071 | 12 | 10 | 2 | 14 | 14 | 0 | |
| MathSAT-default | 0 | 9 | 40878.729 | 40878.733 | 9 | 7 | 2 | 17 | 17 | 0 | |
| MathSAT-na-ext | 0 | 9 | 41420.543 | 41420.636 | 9 | 7 | 2 | 17 | 17 | 0 | |
| Alt-Ergo | 0 | 0 | 62400.0 | 62400.0 | 0 | 0 | 0 | 26 | 26 | 0 | |
| veriT+raSAT+Redlog | 0 | 0 | 62400.0 | 62400.0 | 0 | 0 | 0 | 26 | 26 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 24 | 10778.806 | 5391.445 | 24 | 24 | 0 | 2 | 0 | 0 |
| 2018-Yicesn | 0 | 23 | 15887.757 | 15888.719 | 23 | 23 | 0 | 3 | 1 | 0 |
| Yices 2.6.2 | 0 | 22 | 15940.743 | 15941.636 | 22 | 22 | 0 | 4 | 2 | 0 |
| Z3n | 0 | 18 | 321.34 | 321.375 | 18 | 18 | 0 | 8 | 0 | 0 |
| CVC4 | 0 | 10 | 34861.392 | 34861.726 | 10 | 10 | 0 | 16 | 14 | 0 |
| MathSAT-default | 0 | 7 | 40878.474 | 40878.478 | 7 | 7 | 0 | 19 | 17 | 0 |
| MathSAT-na-ext | 0 | 7 | 41420.281 | 41420.374 | 7 | 7 | 0 | 19 | 17 | 0 |
| Alt-Ergo | 0 | 0 | 57600.0 | 57600.0 | 0 | 0 | 0 | 26 | 26 | 0 |
| veriT+raSAT+Redlog | 0 | 0 | 57600.0 | 57600.0 | 0 | 0 | 0 | 26 | 26 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| MathSAT-default | 0 | 2 | 0.255 | 0.255 | 2 | 0 | 2 | 24 | 17 | 0 |
| MathSAT-na-ext | 0 | 2 | 0.261 | 0.261 | 2 | 0 | 2 | 24 | 17 | 0 |
| Z3n | 0 | 2 | 0.312 | 0.312 | 2 | 0 | 2 | 24 | 0 | 0 |
| Par4 | 0 | 2 | 0.012 | 0.489 | 2 | 0 | 2 | 24 | 0 | 0 |
| 2018-Yicesn | 0 | 2 | 2.291 | 2.291 | 2 | 0 | 2 | 24 | 1 | 0 |
| Yices 2.6.2 | 0 | 2 | 2.527 | 2.527 | 2 | 0 | 2 | 24 | 2 | 0 |
| CVC4 | 0 | 2 | 9.345 | 9.345 | 2 | 0 | 2 | 24 | 14 | 0 |
| Alt-Ergo | 0 | 0 | 4800.0 | 4800.0 | 0 | 0 | 0 | 26 | 26 | 0 |
| veriT+raSAT+Redlog | 0 | 0 | 4800.0 | 4800.0 | 0 | 0 | 0 | 26 | 26 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Z3n | 0 | 19 | 264.867 | 264.886 | 19 | 17 | 2 | 7 | 3 | 0 | |
| Par4 | 0 | 18 | 397.909 | 296.669 | 18 | 16 | 2 | 8 | 8 | 0 | |
| MathSAT-default | 0 | 9 | 486.729 | 486.733 | 9 | 7 | 2 | 17 | 17 | 0 | |
| MathSAT-na-ext | 0 | 5 | 554.545 | 554.553 | 5 | 3 | 2 | 21 | 21 | 0 | |
| 2018-Yicesn | 0 | 4 | 555.062 | 555.066 | 4 | 2 | 2 | 22 | 22 | 0 | |
| Yices 2.6.2 | 0 | 4 | 557.89 | 557.893 | 4 | 2 | 2 | 22 | 22 | 0 | |
| CVC4 | 0 | 2 | 585.345 | 585.345 | 2 | 0 | 2 | 24 | 24 | 0 | |
| Alt-Ergo | 0 | 0 | 624.0 | 624.0 | 0 | 0 | 0 | 26 | 26 | 0 | |
| veriT+raSAT+Redlog | 0 | 0 | 624.0 | 624.0 | 0 | 0 | 0 | 26 | 26 | 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.