The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the UFDT logic in the Single Query Track.
Page generated on 2023-07-06 16:04:54 +0000
Benchmarks: 1550 Time Limit: 1200 seconds Memory Limit: 60 GB
| 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 | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 564 | 83666.822 | 88667.362 | 564 | 143 | 421 | 986 | 986 | 0 |
| 2022-cvc5n | 0 | 545 | 82143.304 | 85046.858 | 545 | 141 | 404 | 1005 | 1005 | 0 |
| iProver | 0 | 288 | 33193.567 | 8577.731 | 288 | 0 | 288 | 1262 | 1261 | 0 |
| iProver Fixedn | 0 | 285 | 30961.733 | 8006.384 | 285 | 0 | 285 | 1265 | 1264 | 0 |
| SMTInterpol | 0 | 101 | 12485.111 | 9556.717 | 101 | 3 | 98 | 1449 | 1418 | 0 |
| Vampire | 79 | 499 | 80697.918 | 20390.107 | 499 | 0 | 499 | 1051 | 972 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 564 | 83666.822 | 88667.362 | 564 | 143 | 421 | 986 | 986 | 0 |
| 2022-cvc5n | 0 | 545 | 82143.304 | 85046.858 | 545 | 141 | 404 | 1005 | 1005 | 0 |
| iProver Fixedn | 0 | 307 | 79324.183 | 20288.965 | 307 | 0 | 307 | 1243 | 1238 | 0 |
| iProver | 0 | 306 | 72745.787 | 18608.192 | 306 | 0 | 306 | 1244 | 1240 | 0 |
| SMTInterpol | 0 | 103 | 16613.531 | 11813.447 | 103 | 3 | 100 | 1447 | 1397 | 0 |
| Vampire | 79 | 571 | 277092.158 | 69755.917 | 571 | 27 | 544 | 979 | 900 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 143 | 65539.428 | 69299.128 | 143 | 143 | 0 | 3 | 1404 | 986 | 0 |
| 2022-cvc5n | 0 | 141 | 63903.261 | 66527.135 | 141 | 141 | 0 | 5 | 1404 | 1005 | 0 |
| Vampire | 0 | 27 | 84520.26 | 21249.82 | 27 | 27 | 0 | 119 | 1404 | 900 | 0 |
| SMTInterpol | 0 | 3 | 2.641 | 1.515 | 3 | 3 | 0 | 143 | 1404 | 1397 | 0 |
| iProver | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 146 | 1404 | 1240 | 0 |
| iProver Fixedn | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 146 | 1404 | 1238 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 421 | 18127.394 | 19368.234 | 421 | 0 | 421 | 181 | 948 | 986 | 0 |
| 2022-cvc5n | 0 | 404 | 18240.042 | 18519.723 | 404 | 0 | 404 | 198 | 948 | 1005 | 0 |
| iProver Fixedn | 0 | 307 | 79324.183 | 20288.965 | 307 | 0 | 307 | 295 | 948 | 1238 | 0 |
| iProver | 0 | 306 | 72745.787 | 18608.192 | 306 | 0 | 306 | 296 | 948 | 1240 | 0 |
| SMTInterpol | 0 | 100 | 16610.89 | 11811.932 | 100 | 0 | 100 | 502 | 948 | 1397 | 0 |
| Vampire | 79 | 544 | 192571.898 | 48506.097 | 544 | 0 | 544 | 58 | 948 | 900 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 346 | 347.459 | 347.516 | 346 | 4 | 342 | 1204 | 1204 | 0 |
| 2022-cvc5n | 0 | 327 | 372.187 | 372.254 | 327 | 5 | 322 | 1223 | 1223 | 0 |
| Vampire | 0 | 311 | 4073.979 | 1064.227 | 311 | 0 | 311 | 1239 | 1239 | 0 |
| iProver Fixedn | 0 | 215 | 3875.182 | 1072.59 | 215 | 0 | 215 | 1335 | 1335 | 0 |
| iProver | 0 | 212 | 3683.971 | 1020.139 | 212 | 0 | 212 | 1338 | 1338 | 0 |
| SMTInterpol | 0 | 61 | 655.089 | 291.139 | 61 | 3 | 58 | 1489 | 1458 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.