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.