The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_NRA logic in the Model Validation Track.
Page generated on 2023-07-06 16:06:00 +0000
Benchmarks: 2982 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance |
|---|---|
| Z3++ | Z3++ |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Timeout | Memout |
|---|---|---|---|---|---|---|
| Z3++ | 0 | 2803 | 26911.81 | 26806.307 | 85 | 0 |
| SMT-RAT-MCSAT | 0 | 2605 | 28708.129 | 28705.332 | 256 | 3 |
| Yices2 | 0 | 2172 | 13928.772 | 13920.287 | 239 | 0 |
| cvc5 | 0 | 2111 | 35969.615 | 35914.853 | 237 | 0 |
| cvc5-NRA-LS | 0 | 2107 | 34103.514 | 34109.773 | 4 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Timeout | Memout |
|---|---|---|---|---|---|---|
| Z3++ | 0 | 2803 | 26911.81 | 26806.307 | 85 | 0 |
| SMT-RAT-MCSAT | 0 | 2605 | 28708.129 | 28705.332 | 256 | 3 |
| Yices2 | 0 | 2172 | 13928.772 | 13920.287 | 239 | 0 |
| cvc5 | 0 | 2111 | 35969.615 | 35914.853 | 237 | 0 |
| cvc5-NRA-LS | 0 | 2107 | 34103.514 | 34109.773 | 4 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.