The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the Equality division in the Single Query Track.
Page generated on 2023-07-06 16:04:54 +0000
Benchmarks: 4407 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 | Vampire |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 1735 | 298080.055 | 310223.557 | 1735 | 529 | 1206 | 2672 | 0 | 2672 | 0 |
| 2022-cvc5n | 0 | 1721 | 295570.73 | 302864.928 | 1721 | 528 | 1193 | 2686 | 0 | 2686 | 0 |
| iProver Fixedn | 0 | 914 | 83545.516 | 21615.035 | 914 | 47 | 867 | 3493 | 0 | 3492 | 0 |
| iProver | 0 | 869 | 82890.752 | 21436.113 | 869 | 0 | 869 | 3538 | 0 | 3520 | 0 |
| Yices2 | 0 | 343 | 11422.427 | 11419.25 | 343 | 30 | 313 | 2514 | 1550 | 2514 | 0 |
| SMTInterpol | 0 | 318 | 30763.634 | 22963.67 | 318 | 13 | 305 | 4089 | 0 | 4034 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 2857 | 1550 | 0 | 0 |
| Vampire | 79 | 1674 | 146564.083 | 37106.095 | 1674 | 472 | 1202 | 2733 | 0 | 2654 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 1735 | 298080.055 | 310223.557 | 1735 | 529 | 1206 | 2672 | 0 | 2672 | 0 |
| 2022-cvc5n | 0 | 1721 | 295570.73 | 302864.928 | 1721 | 528 | 1193 | 2686 | 0 | 2686 | 0 |
| Yices2 | 0 | 343 | 11422.427 | 11419.25 | 343 | 30 | 313 | 2514 | 1550 | 2514 | 0 |
| SMTInterpol | 0 | 324 | 41536.164 | 29541.37 | 324 | 13 | 311 | 4083 | 0 | 3919 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 2857 | 1550 | 0 | 0 |
| iProver Fixedn | 9 | 1202 | 513330.566 | 130769.213 | 1202 | 221 | 981 | 3205 | 0 | 3170 | 0 |
| iProver | 9 | 982 | 275241.882 | 70205.432 | 982 | 0 | 982 | 3425 | 0 | 3375 | 0 |
| Vampire | 79 | 1808 | 493980.853 | 124471.702 | 1808 | 503 | 1305 | 2599 | 0 | 2520 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 529 | 256016.159 | 265960.496 | 529 | 529 | 0 | 101 | 3777 | 2672 | 0 |
| 2022-cvc5n | 0 | 528 | 254941.423 | 261688.784 | 528 | 528 | 0 | 102 | 3777 | 2686 | 0 |
| Vampire | 0 | 503 | 116726.955 | 29420.585 | 503 | 503 | 0 | 127 | 3777 | 2520 | 0 |
| iProver Fixedn | 0 | 221 | 245570.081 | 62357.353 | 221 | 221 | 0 | 409 | 3777 | 3170 | 0 |
| Yices2 | 0 | 30 | 8.696 | 8.788 | 30 | 30 | 0 | 454 | 3923 | 2514 | 0 |
| SMTInterpol | 0 | 13 | 277.472 | 231.233 | 13 | 13 | 0 | 617 | 3777 | 3919 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 484 | 3923 | 0 | 0 |
| iProver | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 630 | 3777 | 3375 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 1206 | 42063.896 | 44263.06 | 1206 | 0 | 1206 | 291 | 2910 | 2672 | 0 |
| 2022-cvc5n | 0 | 1193 | 40629.307 | 41176.144 | 1193 | 0 | 1193 | 304 | 2910 | 2686 | 0 |
| Yices2 | 0 | 313 | 11413.731 | 11410.462 | 313 | 0 | 313 | 582 | 3512 | 2514 | 0 |
| SMTInterpol | 0 | 311 | 41258.691 | 29310.137 | 311 | 0 | 311 | 1186 | 2910 | 3919 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 895 | 3512 | 0 | 0 |
| iProver | 9 | 982 | 275241.882 | 70205.432 | 982 | 0 | 982 | 515 | 2910 | 3375 | 0 |
| iProver Fixedn | 9 | 981 | 267760.484 | 68411.859 | 981 | 0 | 981 | 516 | 2910 | 3170 | 0 |
| Vampire | 79 | 1305 | 377253.898 | 95051.117 | 1305 | 0 | 1305 | 192 | 2910 | 2520 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Vampire | 0 | 1237 | 10508.568 | 2797.046 | 1237 | 355 | 882 | 3170 | 0 | 3170 | 0 |
| cvc5 | 0 | 1014 | 988.946 | 983.41 | 1014 | 16 | 998 | 3393 | 0 | 3393 | 0 |
| 2022-cvc5n | 0 | 993 | 921.333 | 917.718 | 993 | 19 | 974 | 3414 | 0 | 3414 | 0 |
| iProver Fixedn | 0 | 712 | 10696.795 | 2945.328 | 712 | 34 | 678 | 3695 | 0 | 3695 | 0 |
| iProver | 0 | 671 | 9901.61 | 2761.873 | 671 | 0 | 671 | 3736 | 0 | 3722 | 0 |
| Yices2 | 0 | 290 | 534.986 | 530.378 | 290 | 30 | 260 | 2567 | 1550 | 2567 | 0 |
| SMTInterpol | 0 | 202 | 2069.977 | 937.497 | 202 | 11 | 191 | 4205 | 0 | 4159 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 2857 | 1550 | 90 | 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.