The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the Equality+MachineArith division in the Single Query Track.
Page generated on 2023-07-06 16:04:54 +0000
Benchmarks: 4539 Time Limit: 1200 seconds Memory Limit: 60 GB
Logics:| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| cvc5 | cvc5 | cvc5 | cvc5 | cvc5 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 1599 | 140298.055 | 147567.83 | 1599 | 672 | 927 | 2940 | 0 | 1928 | 0 |
| 2022-z3-4.8.17n | 0 | 921 | 32357.285 | 32345.9 | 921 | 602 | 319 | 3617 | 1 | 1488 | 7 |
| Bitwuzla Fixedn | 0 | 747 | 38059.488 | 37974.305 | 747 | 270 | 477 | 2841 | 951 | 360 | 0 |
| Bitwuzla | 0 | 746 | 37675.455 | 37610.761 | 746 | 270 | 476 | 2842 | 951 | 361 | 0 |
| UltimateEliminator+MathSAT | 0 | 21 | 1279.199 | 1115.252 | 21 | 1 | 20 | 3775 | 743 | 394 | 6 |
| UltimateIntBlastingWrapper+SMTInterpol | 7 | 115 | 3643.837 | 2522.806 | 115 | 21 | 94 | 4228 | 196 | 747 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 1599 | 140298.055 | 147567.83 | 1599 | 672 | 927 | 2940 | 0 | 1928 | 0 |
| 2022-z3-4.8.17n | 0 | 921 | 32357.285 | 32345.9 | 921 | 602 | 319 | 3617 | 1 | 1488 | 7 |
| Bitwuzla Fixedn | 0 | 747 | 38059.488 | 37974.305 | 747 | 270 | 477 | 2841 | 951 | 360 | 0 |
| Bitwuzla | 0 | 746 | 37675.455 | 37610.761 | 746 | 270 | 476 | 2842 | 951 | 361 | 0 |
| UltimateEliminator+MathSAT | 0 | 21 | 1279.199 | 1115.252 | 21 | 1 | 20 | 3775 | 743 | 393 | 6 |
| UltimateIntBlastingWrapper+SMTInterpol | 7 | 115 | 3643.837 | 2522.806 | 115 | 21 | 94 | 4228 | 196 | 686 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 672 | 81276.62 | 85531.904 | 672 | 672 | 0 | 474 | 3393 | 1928 | 0 |
| 2022-z3-4.8.17n | 0 | 602 | 10712.944 | 10698.369 | 602 | 602 | 0 | 544 | 3393 | 1488 | 7 |
| Bitwuzla Fixedn | 0 | 270 | 7087.362 | 7054.254 | 270 | 270 | 0 | 679 | 3590 | 360 | 0 |
| Bitwuzla | 0 | 270 | 7825.43 | 7802.245 | 270 | 270 | 0 | 679 | 3590 | 361 | 0 |
| UltimateEliminator+MathSAT | 0 | 1 | 12.14 | 7.103 | 1 | 1 | 0 | 968 | 3570 | 393 | 6 |
| UltimateIntBlastingWrapper+SMTInterpol | 7 | 21 | 1078.287 | 888.47 | 21 | 21 | 0 | 1024 | 3494 | 686 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 927 | 59021.434 | 62035.925 | 927 | 0 | 927 | 210 | 3402 | 1928 | 0 |
| Bitwuzla Fixedn | 0 | 477 | 30972.127 | 30920.051 | 477 | 0 | 477 | 489 | 3573 | 360 | 0 |
| Bitwuzla | 0 | 476 | 29850.024 | 29808.516 | 476 | 0 | 476 | 490 | 3573 | 361 | 0 |
| 2022-z3-4.8.17n | 0 | 319 | 21644.34 | 21647.53 | 319 | 0 | 319 | 818 | 3402 | 1488 | 7 |
| UltimateIntBlastingWrapper+SMTInterpol | 0 | 94 | 2565.55 | 1634.336 | 94 | 0 | 94 | 1007 | 3438 | 686 | 0 |
| UltimateEliminator+MathSAT | 0 | 20 | 1267.06 | 1108.148 | 20 | 0 | 20 | 954 | 3565 | 393 | 6 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 1104 | 1756.11 | 1713.926 | 1104 | 329 | 775 | 3435 | 0 | 3367 | 0 |
| 2022-z3-4.8.17n | 0 | 822 | 871.579 | 855.431 | 822 | 571 | 251 | 3716 | 1 | 1699 | 7 |
| Bitwuzla Fixedn | 0 | 575 | 1777.283 | 1768.399 | 575 | 229 | 346 | 3013 | 951 | 540 | 0 |
| Bitwuzla | 0 | 574 | 1783.559 | 1755.05 | 574 | 228 | 346 | 3014 | 951 | 541 | 0 |
| UltimateEliminator+MathSAT | 0 | 19 | 196.618 | 96.529 | 19 | 1 | 18 | 3777 | 743 | 531 | 6 |
| UltimateIntBlastingWrapper+SMTInterpol | 7 | 108 | 1481.819 | 561.328 | 108 | 20 | 88 | 4235 | 196 | 986 | 0 |
n Non-competing.
Abstained: Total of benchmarks in logics in this division that solver chose to abstain from. For SAT/UNSAT scores, this column also includes benchmarks not known to be SAT/UNSAT.