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 2021-07-18 17:29:05 +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 | COLIBRI | COLIBRI | COLIBRI |
Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
---|---|---|---|---|---|---|---|---|---|---|
COLIBRI - fixedn | 0 | 25 | 33.717 | 33.802 | 25 | 20 | 5 | 0 | 0 | 0 |
COLIBRI | 0 | 25 | 34.015 | 34.036 | 25 | 20 | 5 | 0 | 0 | 0 |
cvc5 | 0 | 25 | 461.359 | 460.504 | 25 | 20 | 5 | 0 | 0 | 0 |
2020-CVC4n | 0 | 25 | 1297.533 | 1296.769 | 25 | 20 | 5 | 0 | 0 | 0 |
MathSAT5n | 0 | 13 | 1220.011 | 1220.404 | 13 | 13 | 0 | 12 | 1 | 0 |
2020-MathSAT5n | 0 | 13 | 1221.498 | 1221.823 | 13 | 13 | 0 | 12 | 1 | 0 |
Bitwuzla | 0 | 9 | 2.454 | 2.657 | 9 | 9 | 0 | 16 | 0 | 0 |
2020-COLIBRIn | 3 | 17 | 2702.078 | 2702.535 | 17 | 17 | 0 | 8 | 2 | 0 |
Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
---|---|---|---|---|---|---|---|---|---|---|
COLIBRI - fixedn | 0 | 25 | 33.717 | 33.802 | 25 | 20 | 5 | 0 | 0 | 0 |
COLIBRI | 0 | 25 | 34.015 | 34.036 | 25 | 20 | 5 | 0 | 0 | 0 |
cvc5 | 0 | 25 | 461.359 | 460.504 | 25 | 20 | 5 | 0 | 0 | 0 |
2020-CVC4n | 0 | 25 | 1297.533 | 1296.769 | 25 | 20 | 5 | 0 | 0 | 0 |
MathSAT5n | 0 | 13 | 1220.341 | 1220.344 | 13 | 13 | 0 | 12 | 1 | 0 |
2020-MathSAT5n | 0 | 13 | 1221.798 | 1221.803 | 13 | 13 | 0 | 12 | 1 | 0 |
Bitwuzla | 0 | 9 | 2.454 | 2.657 | 9 | 9 | 0 | 16 | 0 | 0 |
2020-COLIBRIn | 3 | 17 | 2702.208 | 2702.415 | 17 | 17 | 0 | 8 | 2 | 0 |
Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
---|---|---|---|---|---|---|---|---|---|---|---|
COLIBRI - fixedn | 0 | 20 | 17.948 | 18.013 | 20 | 20 | 0 | 0 | 5 | 0 | 0 |
COLIBRI | 0 | 20 | 18.05 | 18.064 | 20 | 20 | 0 | 0 | 5 | 0 | 0 |
cvc5 | 0 | 20 | 101.231 | 100.281 | 20 | 20 | 0 | 0 | 5 | 0 | 0 |
2020-CVC4n | 0 | 20 | 506.701 | 506.87 | 20 | 20 | 0 | 0 | 5 | 0 | 0 |
MathSAT5n | 0 | 13 | 1220.206 | 1220.209 | 13 | 13 | 0 | 7 | 5 | 1 | 0 |
2020-MathSAT5n | 0 | 13 | 1221.653 | 1221.658 | 13 | 13 | 0 | 7 | 5 | 1 | 0 |
Bitwuzla | 0 | 9 | 2.43 | 2.565 | 9 | 9 | 0 | 11 | 5 | 0 | 0 |
2020-COLIBRIn | 3 | 17 | 1489.022 | 1489.101 | 17 | 17 | 0 | 3 | 5 | 2 | 0 |
Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
---|---|---|---|---|---|---|---|---|---|---|---|
COLIBRI - fixedn | 0 | 5 | 15.769 | 15.789 | 5 | 0 | 5 | 0 | 20 | 0 | 0 |
COLIBRI | 0 | 5 | 15.964 | 15.972 | 5 | 0 | 5 | 0 | 20 | 0 | 0 |
cvc5 | 0 | 5 | 360.127 | 360.223 | 5 | 0 | 5 | 0 | 20 | 0 | 0 |
2020-CVC4n | 0 | 5 | 790.832 | 789.9 | 5 | 0 | 5 | 0 | 20 | 0 | 0 |
Bitwuzla | 0 | 0 | 0.025 | 0.092 | 0 | 0 | 0 | 5 | 20 | 0 | 0 |
MathSAT5n | 0 | 0 | 0.135 | 0.136 | 0 | 0 | 0 | 5 | 20 | 1 | 0 |
2020-MathSAT5n | 0 | 0 | 0.145 | 0.145 | 0 | 0 | 0 | 5 | 20 | 1 | 0 |
2020-COLIBRIn | 0 | 0 | 1213.186 | 1213.314 | 0 | 0 | 0 | 5 | 20 | 2 | 0 |
Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
---|---|---|---|---|---|---|---|---|---|---|
COLIBRI - fixedn | 0 | 25 | 33.717 | 33.802 | 25 | 20 | 5 | 0 | 0 | 0 |
COLIBRI | 0 | 25 | 34.015 | 34.036 | 25 | 20 | 5 | 0 | 0 | 0 |
cvc5 | 0 | 22 | 127.363 | 126.402 | 22 | 19 | 3 | 3 | 3 | 0 |
2020-CVC4n | 0 | 21 | 146.393 | 145.38 | 21 | 18 | 3 | 4 | 4 | 0 |
MathSAT5n | 0 | 13 | 44.341 | 44.344 | 13 | 13 | 0 | 12 | 1 | 0 |
2020-MathSAT5n | 0 | 13 | 45.798 | 45.803 | 13 | 13 | 0 | 12 | 1 | 0 |
Bitwuzla | 0 | 9 | 2.454 | 2.657 | 9 | 9 | 0 | 16 | 0 | 0 |
2020-COLIBRIn | 3 | 15 | 159.376 | 159.567 | 15 | 15 | 0 | 10 | 4 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.