The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the Equality+LinearArith division in the Single Query Track.
Page generated on 2022-08-10 11:17:44 +0000
Benchmarks: 13994 Time Limit: 1200 seconds Memory Limit: 60 GB
Logics:| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| cvc5 | cvc5 | cvc5 | cvc5 | cvc5 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 11328 | 2996312.274 | 3029013.431 | 11328 | 757 | 10571 | 2666 | 0 | 2376 | 0 |
| z3-4.8.17n | 0 | 10834 | 2622991.473 | 2638109.198 | 10834 | 802 | 10032 | 3160 | 0 | 1890 | 15 |
| 2020-CVC4n | 0 | 10801 | 2215291.113 | 2246798.991 | 10801 | 279 | 10522 | 3193 | 0 | 1742 | 0 |
| Vampire | 0 | 9979 | 5528327.193 | 4941676.917 | 9979 | 108 | 9871 | 4015 | 0 | 3952 | 0 |
| veriT | 0 | 4133 | 2298741.141 | 2298896.244 | 4133 | 0 | 4133 | 2082 | 7779 | 1804 | 73 |
| UltimateEliminator+MathSAT | 0 | 62 | 75855.0 | 46690.554 | 62 | 9 | 53 | 13932 | 0 | 3 | 0 |
| smtinterpol | 1 | 8848 | 4781783.502 | 4746402.638 | 8848 | 582 | 8266 | 5146 | 0 | 3864 | 0 |
| smtinterpol-fixedn | 1 | 5614 | 2192968.382 | 2173811.897 | 5614 | 81 | 5533 | 2099 | 6281 | 1752 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 11328 | 3025773.274 | 3028899.181 | 11328 | 757 | 10571 | 2666 | 0 | 2376 | 0 |
| z3-4.8.17n | 0 | 10834 | 2625230.313 | 2638024.628 | 10834 | 802 | 10032 | 3160 | 0 | 1890 | 15 |
| 2020-CVC4n | 0 | 10801 | 2244130.033 | 2246717.261 | 10801 | 279 | 10522 | 3193 | 0 | 1742 | 0 |
| Vampire | 0 | 10236 | 6438928.063 | 4771900.705 | 10236 | 108 | 10128 | 3758 | 0 | 3690 | 0 |
| veriT | 0 | 4133 | 2298973.951 | 2298825.364 | 4133 | 0 | 4133 | 2082 | 7779 | 1804 | 73 |
| UltimateEliminator+MathSAT | 0 | 62 | 75855.0 | 46690.554 | 62 | 9 | 53 | 13932 | 0 | 3 | 0 |
| smtinterpol | 1 | 8854 | 4872680.862 | 4718004.123 | 8854 | 582 | 8272 | 5140 | 0 | 3788 | 0 |
| smtinterpol-fixedn | 1 | 5617 | 2228095.352 | 2159474.466 | 5617 | 81 | 5536 | 2096 | 6281 | 1718 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| z3-4.8.17n | 0 | 802 | 114219.322 | 114217.289 | 802 | 802 | 0 | 96 | 13096 | 1890 | 15 |
| cvc5 | 0 | 757 | 126334.0 | 126929.609 | 757 | 757 | 0 | 141 | 13096 | 2376 | 0 |
| 2020-CVC4n | 0 | 279 | 114910.477 | 115308.191 | 279 | 279 | 0 | 619 | 13096 | 1742 | 0 |
| Vampire | 0 | 108 | 1080290.29 | 948533.139 | 108 | 108 | 0 | 790 | 13096 | 3690 | 0 |
| UltimateEliminator+MathSAT | 0 | 9 | 4332.299 | 2561.314 | 9 | 9 | 0 | 889 | 13096 | 3 | 0 |
| veriT | 0 | 0 | 104406.377 | 104406.402 | 0 | 0 | 0 | 223 | 13771 | 1804 | 73 |
| smtinterpol | 1 | 582 | 81909.522 | 80887.522 | 582 | 582 | 0 | 316 | 13096 | 3788 | 0 |
| smtinterpol-fixedn | 1 | 81 | 121756.745 | 121089.547 | 81 | 81 | 0 | 220 | 13693 | 1718 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 10571 | 308055.4 | 310560.883 | 10571 | 0 | 10571 | 152 | 3271 | 2376 | 0 |
| 2020-CVC4n | 0 | 10522 | 325548.669 | 327726.945 | 10522 | 0 | 10522 | 201 | 3271 | 1742 | 0 |
| Vampire | 0 | 10128 | 2082603.313 | 976189.946 | 10128 | 0 | 10128 | 595 | 3271 | 3690 | 0 |
| z3-4.8.17n | 0 | 10032 | 652388.077 | 657702.379 | 10032 | 0 | 10032 | 691 | 3271 | 1890 | 15 |
| smtinterpol | 0 | 8272 | 2885440.279 | 2806583.955 | 8272 | 0 | 8272 | 2451 | 3271 | 3788 | 0 |
| smtinterpol-fixedn | 0 | 5536 | 1369197.83 | 1325593.588 | 5536 | 0 | 5536 | 1094 | 7364 | 1718 | 0 |
| veriT | 0 | 4133 | 567115.11 | 567069.72 | 4133 | 0 | 4133 | 453 | 9408 | 1804 | 73 |
| UltimateEliminator+MathSAT | 0 | 53 | 58405.306 | 36271.8 | 53 | 0 | 53 | 10670 | 3271 | 3 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| z3-4.8.17n | 0 | 10763 | 66010.111 | 65990.625 | 10763 | 792 | 9971 | 3231 | 0 | 2668 | 15 |
| cvc5 | 0 | 10682 | 79553.966 | 79514.399 | 10682 | 661 | 10021 | 3312 | 0 | 3091 | 0 |
| 2020-CVC4n | 0 | 10196 | 59854.01 | 59813.343 | 10196 | 190 | 10006 | 3798 | 0 | 2368 | 0 |
| Vampire | 0 | 8639 | 161716.514 | 136737.612 | 8639 | 96 | 8543 | 5355 | 0 | 5295 | 0 |
| smtinterpol | 0 | 8525 | 140824.836 | 118899.665 | 8525 | 582 | 7943 | 5469 | 0 | 4307 | 0 |
| smtinterpol-fixedn | 0 | 5380 | 70115.19 | 57927.555 | 5380 | 81 | 5299 | 2333 | 6281 | 2043 | 0 |
| veriT | 0 | 4038 | 50975.04 | 50940.083 | 4038 | 0 | 4038 | 2177 | 7779 | 1938 | 73 |
| UltimateEliminator+MathSAT | 0 | 62 | 69830.815 | 41209.173 | 62 | 9 | 53 | 13932 | 0 | 31 | 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.