QF_Equality_LinearArith (Single Query Track)
Competition results for the QF_Equality_LinearArith
division
in the Single Query Track.
Results were generated on 2024-07-08
Benchmarks: 1936
Time Limit: 1200 seconds
Memory Limit: 20480 GB
Logics:Winners
| winner_seq | winner_par | winner_sat | winner_unsat | winner_24s |
|---|
| SMTInterpol | SMTInterpol | SMTInterpol | OpenSMT | 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 | 1811 | 44096.431385 | 27640.530684 | 1821 | 1047 | 774 | 115 | 0 | 112 | 3 |
| OpenSMT | 0 | 1774 | 30920.891339 | 31105.776144 | 1774 | 981 | 793 | 77 | 85 | 77 | 0 |
| cvc5 | 0 | 1758 | 65604.47768 | 65791.993226 | 1758 | 971 | 787 | 178 | 0 | 178 | 0 |
| Yices2 | 0 | 1748 | 20462.466911 | 20642.447641 | 1748 | 958 | 790 | 103 | 85 | 103 | 0 |
Parallel Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| SMTInterpol | 0 | 1821 | 62502.221999 | 36747.6329 | 1821 | 1047 | 774 | 115 | 0 | 112 | 3 |
| OpenSMT | 0 | 1774 | 30920.891339 | 31105.776144 | 1774 | 981 | 793 | 77 | 85 | 77 | 0 |
| cvc5 | 0 | 1758 | 65604.47768 | 65791.993226 | 1758 | 971 | 787 | 178 | 0 | 178 | 0 |
| Yices2 | 0 | 1748 | 20462.466911 | 20642.447641 | 1748 | 958 | 790 | 103 | 85 | 103 | 0 |
SAT Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| SMTInterpol | 0 | 1047 | 37177.51401 | 22871.391154 | 1047 | 1047 | 0 | 17 | 872 | 16 | 1 |
| OpenSMT | 0 | 981 | 15962.743363 | 16064.732367 | 981 | 981 | 0 | 31 | 924 | 31 | 0 |
| cvc5 | 0 | 971 | 39486.588884 | 39590.311316 | 971 | 971 | 0 | 93 | 872 | 93 | 0 |
| Yices2 | 0 | 958 | 11669.319474 | 11768.392865 | 958 | 958 | 0 | 54 | 924 | 54 | 0 |
UNSAT Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| OpenSMT | 0 | 793 | 14958.147975 | 15041.043776 | 793 | 0 | 793 | 26 | 1117 | 26 | 0 |
| Yices2 | 0 | 790 | 8793.147437 | 8874.054776 | 790 | 0 | 790 | 29 | 1117 | 29 | 0 |
| cvc5 | 0 | 787 | 26117.888795 | 26201.68191 | 787 | 0 | 787 | 49 | 1100 | 49 | 0 |
| SMTInterpol | 0 | 774 | 25324.707988 | 13876.241746 | 774 | 0 | 774 | 62 | 1100 | 62 | 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 | 1694 | 609.40362 | 778.967427 | 1694 | 926 | 768 | 0 | 242 | 0 | 0 |
| SMTInterpol | 0 | 1690 | 9038.137256 | 3604.411136 | 1690 | 961 | 729 | 0 | 246 | 0 | 0 |
| OpenSMT | 0 | 1626 | 2153.907183 | 2317.036068 | 1626 | 892 | 734 | 0 | 310 | 0 | 0 |
| cvc5 | 0 | 1575 | 1405.858137 | 1563.177534 | 1575 | 874 | 701 | 0 | 361 | 0 | 0 |