The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_Equality+LinearArith division in the Single Query Track.
Page generated on 2023-07-06 16:04:54 +0000
Benchmarks: 1922 Time Limit: 1200 seconds Memory Limit: 60 GB
Logics:| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| SMTInterpol | SMTInterpol | SMTInterpol | OpenSMT | Yices2 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| SMTInterpol | 0 | 1809 | 52677.755 | 40237.027 | 1809 | 1058 | 751 | 113 | 0 | 113 | 0 |
| OpenSMT | 0 | 1772 | 40949.939 | 40862.798 | 1772 | 993 | 779 | 65 | 85 | 65 | 0 |
| 2022-z3-4.8.17n | 0 | 1749 | 28616.218 | 28611.835 | 1749 | 976 | 773 | 97 | 76 | 97 | 0 |
| cvc5 | 0 | 1740 | 61435.265 | 61281.341 | 1740 | 976 | 764 | 182 | 0 | 182 | 0 |
| Yices2 | 0 | 1735 | 27167.152 | 27168.868 | 1735 | 960 | 775 | 102 | 85 | 102 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| SMTInterpol | 0 | 1816 | 62150.875 | 46637.515 | 1816 | 1059 | 757 | 106 | 0 | 106 | 0 |
| OpenSMT | 0 | 1772 | 40949.939 | 40862.798 | 1772 | 993 | 779 | 65 | 85 | 65 | 0 |
| 2022-z3-4.8.17n | 0 | 1749 | 28616.218 | 28611.835 | 1749 | 976 | 773 | 97 | 76 | 97 | 0 |
| cvc5 | 0 | 1740 | 61435.265 | 61281.341 | 1740 | 976 | 764 | 182 | 0 | 182 | 0 |
| Yices2 | 0 | 1735 | 27167.152 | 27168.868 | 1735 | 960 | 775 | 102 | 85 | 102 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| SMTInterpol | 0 | 1059 | 35517.413 | 29611.161 | 1059 | 1059 | 0 | 14 | 849 | 106 | 0 |
| OpenSMT | 0 | 993 | 21039.394 | 20957.39 | 993 | 993 | 0 | 28 | 901 | 65 | 0 |
| 2022-z3-4.8.17n | 0 | 976 | 13533.699 | 13533.035 | 976 | 976 | 0 | 50 | 896 | 97 | 0 |
| cvc5 | 0 | 976 | 34579.559 | 34490.907 | 976 | 976 | 0 | 97 | 849 | 182 | 0 |
| Yices2 | 0 | 960 | 14966.937 | 14969.038 | 960 | 960 | 0 | 61 | 901 | 102 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| OpenSMT | 0 | 779 | 19910.545 | 19905.407 | 779 | 0 | 779 | 26 | 1117 | 65 | 0 |
| Yices2 | 0 | 775 | 12200.215 | 12199.83 | 775 | 0 | 775 | 30 | 1117 | 102 | 0 |
| 2022-z3-4.8.17n | 0 | 773 | 15082.519 | 15078.8 | 773 | 0 | 773 | 36 | 1113 | 97 | 0 |
| cvc5 | 0 | 764 | 26855.706 | 26790.434 | 764 | 0 | 764 | 56 | 1102 | 182 | 0 |
| SMTInterpol | 0 | 757 | 26633.462 | 17026.354 | 757 | 0 | 757 | 63 | 1102 | 106 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 1675 | 423.367 | 422.249 | 1675 | 927 | 748 | 162 | 85 | 162 | 0 |
| 2022-z3-4.8.17n | 0 | 1665 | 820.771 | 813.288 | 1665 | 933 | 732 | 181 | 76 | 181 | 0 |
| SMTInterpol | 0 | 1656 | 8365.368 | 3285.951 | 1656 | 953 | 703 | 266 | 0 | 266 | 0 |
| OpenSMT | 0 | 1609 | 2306.367 | 2268.718 | 1609 | 905 | 704 | 228 | 85 | 228 | 0 |
| cvc5 | 0 | 1561 | 1208.12 | 1196.479 | 1561 | 889 | 672 | 361 | 0 | 361 | 0 |
n Non-competing.
Abstained: Total of benchmarks in logics in this division that solver chose to abstain from. For SAT/UNSAT scores, this column also includes benchmarks not known to be SAT/UNSAT.