QF_NonLinearIntArith (Single Query Track)
Competition results for the QF_NonLinearIntArith
division
in the Single Query Track.
Results were generated on 2024-07-08
Benchmarks: 12276
Time Limit: 1200 seconds
Memory Limit: 20480 GB
Logics: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 | 9756 | 337614.486309 | 338666.988801 | 9756 | 6451 | 3305 | 2520 | 0 | 2454 | 2 |
| Yices2 | 0 | 8556 | 97393.170971 | 98274.336471 | 8556 | 5651 | 2905 | 3720 | 0 | 3707 | 8 |
| cvc5 | 0 | 8421 | 1.739230224178e+06 | 1.740467954913e+06 | 8421 | 5898 | 2523 | 3855 | 0 | 3592 | 259 |
| SMTInterpol | 0 | 79 | 1735.803079 | 960.658836 | 79 | 5 | 74 | 12197 | 0 | 16 | 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 | 9756 | 337614.486309 | 338666.988801 | 9756 | 6451 | 3305 | 2520 | 0 | 2454 | 2 |
| Yices2 | 0 | 8556 | 97393.170971 | 98274.336471 | 8556 | 5651 | 2905 | 3720 | 0 | 3707 | 8 |
| cvc5 | 0 | 8421 | 1.739230224178e+06 | 1.740467954913e+06 | 8421 | 5898 | 2523 | 3855 | 0 | 3592 | 259 |
| SMTInterpol | 0 | 79 | 1735.803079 | 960.658836 | 79 | 5 | 74 | 12197 | 0 | 16 | 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 | 5208 | 590 | 0 |
| cvc5 | 0 | 5898 | 1.640312874576e+06 | 1.641275049034e+06 | 5898 | 5898 | 0 | 1170 | 5208 | 1049 | 121 |
| Yices2 | 0 | 5651 | 66470.875696 | 67054.711756 | 5651 | 5651 | 0 | 1417 | 5208 | 1417 | 0 |
| SMTInterpol | 0 | 5 | 414.124196 | 259.325135 | 5 | 5 | 0 | 7063 | 5208 | 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 | 3305 | 95072.433461 | 95426.926108 | 3305 | 0 | 3305 | 242 | 8729 | 242 | 0 |
| Yices2 | 0 | 2905 | 30922.295275 | 31219.624715 | 2905 | 0 | 2905 | 642 | 8729 | 635 | 7 |
| cvc5 | 0 | 2523 | 98917.349601 | 99192.905879 | 2523 | 0 | 2523 | 1024 | 8729 | 1021 | 3 |
| SMTInterpol | 0 | 74 | 1321.678883 | 701.333701 | 74 | 0 | 74 | 3473 | 8729 | 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 | 4258 | 0 | 0 |
| Z3-alpha | 0 | 7771 | 35901.120352 | 36691.740801 | 7771 | 5031 | 2740 | 4 | 4501 | 0 | 0 |
| cvc5 | 0 | 4635 | 14193.835106 | 14659.565839 | 4635 | 2515 | 2120 | 1 | 7640 | 0 | 0 |
| SMTInterpol | 0 | 74 | 351.362299 | 170.432044 | 74 | 3 | 71 | 12092 | 110 | 0 | 0 |