The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_LRA logic in the Proof Exhibition Track.
Page generated on 2022-08-10 11:19:33 +0000
Benchmarks: 349 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 |
|---|---|---|---|---|---|---|---|
| OpenSMT | 0 | 344 | 16751.743 | 16726.595 | 5 | 5 | 0 |
| smtinterpol | 0 | 313 | 80094.662 | 73839.276 | 36 | 39 | 0 |
| veriT | 0 | 302 | 31361.683 | 31331.437 | 47 | 15 | 0 |
| cvc5-lfsc | 0 | 294 | 97107.057 | 97050.846 | 55 | 55 | 0 |
| cvc5 | 0 | 114 | 275406.265 | 275365.856 | 235 | 222 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|
| OpenSMT | 0 | 344 | 16752.553 | 16726.285 | 5 | 5 | 0 |
| smtinterpol | 0 | 313 | 80525.732 | 73380.491 | 36 | 36 | 0 |
| veriT | 0 | 302 | 31364.823 | 31330.527 | 47 | 15 | 0 |
| cvc5-lfsc | 0 | 294 | 97120.107 | 97048.756 | 55 | 55 | 0 |
| cvc5 | 0 | 114 | 275453.785 | 275354.636 | 235 | 222 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.