QF_Equality_LinearArith (Model Validation Track)
Competition results for the QF_Equality_LinearArith
division
in the Model Validation Track.
Results were generated on 2024-07-08
Benchmarks: 891
Time Limit: 1200 seconds
Memory Limit: 20480 GB
Logics:Winners
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|
| OpenSMT | OpenSMT | OpenSMT | - | OpenSMT |
Sequential Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| OpenSMT | 0 | 878 | 13242.047971 | 13332.691215 | 878 | 878 | 0 | 13 | 0 | 13 | 0 |
| SMTInterpol | 0 | 861 | 28367.511206 | 13624.388577 | 866 | 866 | 0 | 25 | 0 | 25 | 0 |
| cvc5 | 0 | 858 | 28553.878972 | 28644.460028 | 858 | 858 | 0 | 33 | 0 | 33 | 0 |
| Yices2 | 0 | 825 | 16049.695677 | 16135.73655 | 825 | 825 | 0 | 66 | 0 | 66 | 0 |
Parallel Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| OpenSMT | 0 | 878 | 13242.047971 | 13332.691215 | 878 | 878 | 0 | 13 | 0 | 13 | 0 |
| SMTInterpol | 0 | 866 | 37472.813115 | 17819.282036 | 866 | 866 | 0 | 25 | 0 | 25 | 0 |
| cvc5 | 0 | 858 | 28553.878972 | 28644.460028 | 858 | 858 | 0 | 33 | 0 | 33 | 0 |
| Yices2 | 0 | 825 | 16049.695677 | 16135.73655 | 825 | 825 | 0 | 66 | 0 | 66 | 0 |
SAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| OpenSMT | 0 | 878 | 13242.047971 | 13332.691215 | 878 | 878 | 0 | 13 | 0 | 13 | 0 |
| SMTInterpol | 0 | 866 | 37472.813115 | 17819.282036 | 866 | 866 | 0 | 25 | 0 | 25 | 0 |
| cvc5 | 0 | 858 | 28553.878972 | 28644.460028 | 858 | 858 | 0 | 33 | 0 | 33 | 0 |
| Yices2 | 0 | 825 | 16049.695677 | 16135.73655 | 825 | 825 | 0 | 66 | 0 | 66 | 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 |
|---|
| OpenSMT | 0 | 813 | 1241.618133 | 1323.072423 | 813 | 813 | 0 | 0 | 78 | 0 | 0 |
| SMTInterpol | 0 | 800 | 3687.822101 | 1413.498043 | 800 | 800 | 0 | 0 | 91 | 0 | 0 |
| Yices2 | 0 | 784 | 222.314996 | 300.902947 | 784 | 784 | 0 | 0 | 107 | 0 | 0 |
| cvc5 | 0 | 776 | 407.324159 | 484.957287 | 776 | 776 | 0 | 0 | 115 | 0 | 0 |