The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the UFLIA logic in the Proof Exhibition Track.
Page generated on 2022-08-10 11:19:33 +0000
Benchmarks: 3917 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 |
|---|---|---|---|---|---|---|---|
| veriT | 0 | 3742 | 207559.055 | 207492.462 | 175 | 151 | 1 |
| cvc5-lfsc | 0 | 3737 | 234027.544 | 233997.812 | 180 | 180 | 0 |
| smtinterpol | 0 | 2485 | 1754387.784 | 1745989.826 | 1432 | 1423 | 0 |
| cvc5 | 0 | 2310 | 1792410.246 | 1791078.472 | 1607 | 1396 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|
| veriT | 0 | 3742 | 207587.795 | 207485.142 | 175 | 151 | 1 |
| cvc5-lfsc | 0 | 3737 | 234101.204 | 233987.272 | 180 | 180 | 0 |
| smtinterpol | 0 | 2485 | 1895801.374 | 1716530.887 | 1432 | 1338 | 0 |
| cvc5 | 0 | 2310 | 1792624.026 | 1791013.272 | 1607 | 1396 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.