QF_Equality_LinearArith (Unsat Core Track)
Competition results for the QF_Equality_LinearArith
division
in the Unsat Core Track.
Results were generated on 2024-07-08
Benchmarks: 588
Time Limit: 1200 seconds
Memory Limit: 20480 GB
Logics:Winners
| winner_seq | winner_par | winner_sat | winner_unsat | winner_24s |
|---|
| SMTInterpol | cvc5 | - | cvc5 | Yices2 |
Sequential Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| SMTInterpol | 0 | 250811 | 8391.676323 | 4518.686916 | 496 | 0 | 496 | 92 | 0 | 92 | 0 |
| cvc5 | 0 | 198295 | 1842.897048 | 1892.19097 | 487 | 0 | 487 | 101 | 0 | 101 | 0 |
| Yices2 | 3 | 902122 | 21691.477483 | 21749.067584 | 516 | 0 | 516 | 47 | 25 | 41 | 0 |
| OpenSMT | 20 | 598346 | 27426.597799 | 27485.787538 | 494 | 0 | 494 | 69 | 25 | 46 | 0 |
Parallel Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| cvc5 | 0 | 1.367556e+06 | 123135.989994 | 123266.427352 | 487 | 0 | 487 | 101 | 0 | 101 | 0 |
| SMTInterpol | 0 | 1.29984e+06 | 167957.988312 | 119089.362152 | 496 | 0 | 496 | 92 | 0 | 92 | 0 |
| Yices2 | 3 | 1.331326e+06 | 70925.280047 | 70999.919028 | 516 | 0 | 516 | 47 | 25 | 41 | 0 |
| OpenSMT | 20 | 1.323714e+06 | 82669.477339 | 82747.207906 | 494 | 0 | 494 | 69 | 25 | 46 | 0 |
UNSAT Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| cvc5 | 0 | 1.367556e+06 | 123135.989994 | 123266.427352 | 487 | 0 | 487 | 101 | 0 | 101 | 0 |
| SMTInterpol | 0 | 1.29984e+06 | 167957.988312 | 119089.362152 | 496 | 0 | 496 | 92 | 0 | 92 | 0 |
| Yices2 | 3 | 1.331326e+06 | 70925.280047 | 70999.919028 | 516 | 0 | 516 | 47 | 25 | 41 | 0 |
| OpenSMT | 20 | 1.323714e+06 | 82669.477339 | 82747.207906 | 494 | 0 | 494 | 69 | 25 | 46 | 0 |
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 | 208645 | 152.940007 | 199.682283 | 463 | 0 | 463 | 3 | 122 | 0 | 0 |
| cvc5 | 0 | 33173 | 195.475598 | 243.414848 | 479 | 0 | 479 | 0 | 109 | 0 | 0 |
| SMTInterpol | 0 | 4487 | 1227.285654 | 543.080958 | 479 | 0 | 479 | 0 | 109 | 0 | 0 |
| OpenSMT | 17 | 3832 | 161.80326 | 207.976569 | 437 | 0 | 437 | 20 | 131 | 0 | 0 |