The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_ABVFPLRA logic in the Single Query Track.
Page generated on 2023-07-06 16:04:54 +0000
Benchmarks: 25 Time Limit: 1200 seconds Memory Limit: 60 GB
Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
---|---|---|---|---|
COLIBRI | COLIBRI | Bitwuzla | COLIBRI | COLIBRI |
Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
---|---|---|---|---|---|---|---|---|---|---|
COLIBRI | 0 | 25 | 42.244 | 42.386 | 25 | 20 | 5 | 0 | 0 | 0 |
Bitwuzla | 0 | 25 | 88.547 | 88.559 | 25 | 20 | 5 | 0 | 0 | 0 |
Bitwuzla Fixedn | 0 | 25 | 88.641 | 88.652 | 25 | 20 | 5 | 0 | 0 | 0 |
cvc5 | 0 | 25 | 368.273 | 365.686 | 25 | 20 | 5 | 0 | 0 | 0 |
2022-Bitwuzlan | 0 | 9 | 2.245 | 2.247 | 9 | 9 | 0 | 16 | 0 | 0 |
Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
---|---|---|---|---|---|---|---|---|---|---|
COLIBRI | 0 | 25 | 42.244 | 42.386 | 25 | 20 | 5 | 0 | 0 | 0 |
Bitwuzla | 0 | 25 | 88.547 | 88.559 | 25 | 20 | 5 | 0 | 0 | 0 |
Bitwuzla Fixedn | 0 | 25 | 88.641 | 88.652 | 25 | 20 | 5 | 0 | 0 | 0 |
cvc5 | 0 | 25 | 368.273 | 365.686 | 25 | 20 | 5 | 0 | 0 | 0 |
2022-Bitwuzlan | 0 | 9 | 2.245 | 2.247 | 9 | 9 | 0 | 16 | 0 | 0 |
Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
---|---|---|---|---|---|---|---|---|---|---|---|
Bitwuzla | 0 | 20 | 19.314 | 19.325 | 20 | 20 | 0 | 0 | 5 | 0 | 0 |
Bitwuzla Fixedn | 0 | 20 | 19.558 | 19.569 | 20 | 20 | 0 | 0 | 5 | 0 | 0 |
COLIBRI | 0 | 20 | 23.556 | 23.639 | 20 | 20 | 0 | 0 | 5 | 0 | 0 |
cvc5 | 0 | 20 | 112.092 | 109.354 | 20 | 20 | 0 | 0 | 5 | 0 | 0 |
2022-Bitwuzlan | 0 | 9 | 2.245 | 2.247 | 9 | 9 | 0 | 11 | 5 | 0 | 0 |
Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
---|---|---|---|---|---|---|---|---|---|---|---|
COLIBRI | 0 | 5 | 18.688 | 18.747 | 5 | 0 | 5 | 0 | 20 | 0 | 0 |
Bitwuzla Fixedn | 0 | 5 | 69.083 | 69.083 | 5 | 0 | 5 | 0 | 20 | 0 | 0 |
Bitwuzla | 0 | 5 | 69.234 | 69.234 | 5 | 0 | 5 | 0 | 20 | 0 | 0 |
cvc5 | 0 | 5 | 256.181 | 256.333 | 5 | 0 | 5 | 0 | 20 | 0 | 0 |
2022-Bitwuzlan | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 5 | 20 | 0 | 0 |
Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
---|---|---|---|---|---|---|---|---|---|---|
COLIBRI | 0 | 25 | 42.244 | 42.386 | 25 | 20 | 5 | 0 | 0 | 0 |
Bitwuzla | 0 | 24 | 27.533 | 27.545 | 24 | 20 | 4 | 1 | 1 | 0 |
Bitwuzla Fixedn | 0 | 24 | 27.794 | 27.807 | 24 | 20 | 4 | 1 | 1 | 0 |
cvc5 | 0 | 22 | 60.727 | 57.987 | 22 | 19 | 3 | 3 | 3 | 0 |
2022-Bitwuzlan | 0 | 9 | 2.245 | 2.247 | 9 | 9 | 0 | 16 | 0 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.