The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_AUFLIA logic in the Incremental Track.
Page generated on 2021-07-18 17:30:28 +0000
Benchmarks: 72 Time Limit: 1200 seconds Memory Limit: 60 GB
| Parallel Performance |
|---|
| cvc5-inc |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|
| 2018-Yices (incremental)n | 0 | 4699864 | 3249.849 | 3040.414 | 0 | 0 | 0 |
| 2020-z3n | 0 | 4641633 | 4739.864 | 4578.663 | 58231 | 1 | 0 |
| z3n | 0 | 4515581 | 6796.418 | 6626.62 | 184283 | 1 | 0 |
| cvc5-inc | 0 | 3891121 | 9029.051 | 8853.417 | 808743 | 2 | 0 |
| SMTInterpol | 0 | 3788321 | 17387.648 | 15874.552 | 911543 | 4 | 0 |
| Yices2 incremental | 0 | 3050626 | 2450.605 | 2289.095 | 1649238 | 0 | 0 |
| MathSAT5n | 0 | 2050467 | 5835.579 | 5707.915 | 2649397 | 1 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.