QF_NIA (Single Query Track)
Competition results for the QF_NIA
logic
in the Single Query Track.
Results were generated on 2024-07-08
Benchmarks: 12274
Time Limit: 1200 seconds
Memory Limit: 20480 GB
Winners
| winner_seq | winner_par | winner_sat | winner_unsat | winner_24s |
|---|
| Z3-alpha | Z3-alpha | Z3-alpha | Z3-alpha | Yices2 |
Sequential Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Z3-alpha | 0 | 9755 | 337609.107286 | 338661.508879 | 9755 | 6451 | 3304 | 2519 | 0 | 2453 | 2 |
| Yices2 | 0 | 8556 | 97393.170971 | 98274.336471 | 8556 | 5651 | 2905 | 3718 | 0 | 3705 | 8 |
| cvc5 | 0 | 8420 | 1.739186187166e+06 | 1.740423816734e+06 | 8420 | 5898 | 2522 | 3854 | 0 | 3591 | 259 |
| SMTInterpol | 0 | 78 | 897.967329 | 523.388999 | 78 | 5 | 73 | 12196 | 0 | 15 | 3 |
Parallel Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Z3-alpha | 0 | 9755 | 337609.107286 | 338661.508879 | 9755 | 6451 | 3304 | 2519 | 0 | 2453 | 2 |
| Yices2 | 0 | 8556 | 97393.170971 | 98274.336471 | 8556 | 5651 | 2905 | 3718 | 0 | 3705 | 8 |
| cvc5 | 0 | 8420 | 1.739186187166e+06 | 1.740423816734e+06 | 8420 | 5898 | 2522 | 3854 | 0 | 3591 | 259 |
| SMTInterpol | 0 | 78 | 897.967329 | 523.388999 | 78 | 5 | 73 | 12196 | 0 | 15 | 3 |
SAT Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Z3-alpha | 0 | 6451 | 242542.052848 | 243240.062693 | 6451 | 6451 | 0 | 617 | 5206 | 590 | 0 |
| cvc5 | 0 | 5898 | 1.640312874576e+06 | 1.641275049034e+06 | 5898 | 5898 | 0 | 1170 | 5206 | 1049 | 121 |
| Yices2 | 0 | 5651 | 66470.875696 | 67054.711756 | 5651 | 5651 | 0 | 1417 | 5206 | 1417 | 0 |
| SMTInterpol | 0 | 5 | 414.124196 | 259.325135 | 5 | 5 | 0 | 7063 | 5206 | 5 | 0 |
UNSAT Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Z3-alpha | 0 | 3304 | 95067.054438 | 95421.446187 | 3304 | 0 | 3304 | 242 | 8728 | 242 | 0 |
| Yices2 | 0 | 2905 | 30922.295275 | 31219.624715 | 2905 | 0 | 2905 | 641 | 8728 | 634 | 7 |
| cvc5 | 0 | 2522 | 98873.31259 | 99148.7677 | 2522 | 0 | 2522 | 1024 | 8728 | 1021 | 3 |
| SMTInterpol | 0 | 73 | 483.843133 | 264.063863 | 73 | 0 | 73 | 3473 | 8728 | 8 | 2 |
24 seconds Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Yices2 | 0 | 8014 | 14658.617858 | 15464.446348 | 8014 | 5258 | 2756 | 4 | 4256 | 0 | 0 |
| Z3-alpha | 0 | 7770 | 35895.741329 | 36686.260879 | 7770 | 5031 | 2739 | 4 | 4500 | 0 | 0 |
| cvc5 | 0 | 4635 | 14193.835106 | 14659.565839 | 4635 | 2515 | 2120 | 1 | 7638 | 0 | 0 |
| SMTInterpol | 0 | 74 | 351.362299 | 170.432044 | 74 | 3 | 71 | 12092 | 108 | 0 | 0 |