QF_NRA (Single Query Track)
Competition results for the QF_NRA
logic
in the Single Query Track.
Results were generated on 2024-07-08
Benchmarks: 3104
Time Limit: 1200 seconds
Memory Limit: 20480 GB
Winners
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|
| Z3-alpha | Z3-alpha | Z3-alpha | cvc5 | Yices2 |
Sequential Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Z3-alpha | 0 | 2813 | 52192.644516 | 52485.764498 | 2813 | 1418 | 1395 | 291 | 0 | 271 | 3 |
| cvc5 | 0 | 2788 | 104672.890546 | 104971.30112 | 2788 | 1360 | 1428 | 316 | 0 | 316 | 0 |
| Yices2 | 0 | 2693 | 21165.170495 | 21439.044798 | 2693 | 1362 | 1331 | 411 | 0 | 411 | 0 |
| SMT-RAT | 0 | 2579 | 85964.901899 | 86236.753886 | 2579 | 1289 | 1290 | 525 | 0 | 525 | 0 |
| SMTInterpol | 0 | 559 | 6717.417522 | 5175.26253 | 559 | 24 | 535 | 2545 | 0 | 4 | 0 |
Parallel Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Z3-alpha | 0 | 2813 | 52192.644516 | 52485.764498 | 2813 | 1418 | 1395 | 291 | 0 | 271 | 3 |
| cvc5 | 0 | 2788 | 104672.890546 | 104971.30112 | 2788 | 1360 | 1428 | 316 | 0 | 316 | 0 |
| Yices2 | 0 | 2693 | 21165.170495 | 21439.044798 | 2693 | 1362 | 1331 | 411 | 0 | 411 | 0 |
| SMT-RAT | 0 | 2579 | 85964.901899 | 86236.753886 | 2579 | 1289 | 1290 | 525 | 0 | 525 | 0 |
| SMTInterpol | 0 | 559 | 6717.417522 | 5175.26253 | 559 | 24 | 535 | 2545 | 0 | 4 | 0 |
SAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Z3-alpha | 0 | 1418 | 21970.518076 | 22116.46961 | 1418 | 1418 | 0 | 103 | 1583 | 101 | 0 |
| Yices2 | 0 | 1362 | 13208.247229 | 13347.030147 | 1362 | 1362 | 0 | 159 | 1583 | 159 | 0 |
| cvc5 | 0 | 1360 | 41431.725181 | 41575.083957 | 1360 | 1360 | 0 | 161 | 1583 | 161 | 0 |
| SMT-RAT | 0 | 1289 | 43736.098192 | 43872.357669 | 1289 | 1289 | 0 | 232 | 1583 | 232 | 0 |
| SMTInterpol | 0 | 24 | 5224.813613 | 4595.977156 | 24 | 24 | 0 | 1497 | 1583 | 2 | 0 |
UNSAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| cvc5 | 0 | 1428 | 63241.165366 | 63396.217163 | 1428 | 0 | 1428 | 38 | 1638 | 38 | 0 |
| Z3-alpha | 0 | 1395 | 30222.12644 | 30369.294888 | 1395 | 0 | 1395 | 71 | 1638 | 57 | 0 |
| Yices2 | 0 | 1331 | 7956.923266 | 8092.014651 | 1331 | 0 | 1331 | 135 | 1638 | 135 | 0 |
| SMT-RAT | 0 | 1290 | 42228.803707 | 42364.396217 | 1290 | 0 | 1290 | 176 | 1638 | 176 | 0 |
| SMTInterpol | 0 | 535 | 1492.603908 | 579.285374 | 535 | 0 | 535 | 931 | 1638 | 2 | 0 |
24 seconds Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Yices2 | 0 | 2584 | 1749.622742 | 2008.066364 | 2584 | 1307 | 1277 | 0 | 520 | 0 | 0 |
| cvc5 | 0 | 2516 | 2518.834207 | 2770.202723 | 2516 | 1256 | 1260 | 0 | 588 | 0 | 0 |
| Z3-alpha | 0 | 2430 | 5305.218102 | 5548.477939 | 2430 | 1278 | 1152 | 0 | 674 | 0 | 0 |
| SMT-RAT | 0 | 2272 | 3034.253293 | 3261.430637 | 2272 | 1170 | 1102 | 0 | 832 | 0 | 0 |
| SMTInterpol | 0 | 541 | 1557.042696 | 603.603746 | 541 | 6 | 535 | 2490 | 73 | 0 | 0 |