The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_LIA logic in the Proof Exhibition Track.
Page generated on 2022-08-10 11:19:33 +0000
Benchmarks: 2377 Time Limit: 1200 seconds Memory Limit: 60 GB
This track is experimental. Solvers are only ranked by performance, but no winner is selected.
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|
| smtinterpol | 0 | 2240 | 397331.778 | 335847.351 | 137 | 145 | 0 |
| OpenSMT | 0 | 2023 | 229537.564 | 229128.362 | 354 | 68 | 0 |
| veriT | 0 | 1435 | 1048658.86 | 1048554.946 | 942 | 815 | 1 |
| cvc5-lfsc | 0 | 1275 | 1348873.712 | 1349211.254 | 1102 | 1094 | 0 |
| cvc5 | 0 | 854 | 1807708.42 | 1807983.923 | 1523 | 1490 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|
| smtinterpol | 0 | 2240 | 415744.148 | 332486.128 | 137 | 126 | 0 |
| OpenSMT | 0 | 2023 | 229554.504 | 229126.082 | 354 | 68 | 0 |
| veriT | 0 | 1435 | 1048726.57 | 1048524.166 | 942 | 815 | 1 |
| cvc5-lfsc | 0 | 1275 | 1349252.462 | 1349151.784 | 1102 | 1094 | 0 |
| cvc5 | 0 | 854 | 1808152.89 | 1807901.383 | 1523 | 1489 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.