The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_IDL division in the Single Query Track.
Page generated on 2020-07-04 11:46:59 +0000
Benchmarks: 834 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Yices2 | Yices2 | Yices2 | CVC4 | Yices2 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 742 | 123877.335 | 123888.42 | 742 | 486 | 256 | 92 | 92 | 0 | |
| Yices2-fixedn | 0 | 742 | 124121.869 | 124117.603 | 742 | 486 | 256 | 92 | 92 | 0 | |
| 2019-Z3n | 0 | 739 | 137184.425 | 137145.953 | 739 | 478 | 261 | 95 | 95 | 0 | |
| 2019-Par4n | 0 | 736 | 140562.936 | 123468.33 | 736 | 481 | 255 | 98 | 98 | 0 | |
| z3n | 0 | 721 | 122201.539 | 122188.973 | 721 | 482 | 239 | 113 | 84 | 0 | |
| CVC4 | 0 | 680 | 235473.129 | 235454.564 | 680 | 423 | 257 | 154 | 154 | 0 | |
| veriT | 0 | 610 | 320196.593 | 320176.879 | 610 | 362 | 248 | 224 | 224 | 0 | |
| MathSAT5n | 0 | 566 | 356443.967 | 356493.482 | 566 | 326 | 240 | 268 | 268 | 0 | |
| SMTInterpol | 0 | 534 | 410519.691 | 405162.97 | 534 | 302 | 232 | 300 | 300 | 0 | |
| SMTInterpol-fixedn | 0 | 534 | 410714.465 | 405313.293 | 534 | 302 | 232 | 300 | 300 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 752 | 162651.156 | 114684.445 | 752 | 490 | 262 | 82 | 82 | 0 | |
| Yices2 | 0 | 742 | 123885.645 | 123885.41 | 742 | 486 | 256 | 92 | 92 | 0 | |
| Yices2-fixedn | 0 | 742 | 124129.899 | 124114.773 | 742 | 486 | 256 | 92 | 92 | 0 | |
| 2019-Z3n | 0 | 739 | 137191.995 | 137143.023 | 739 | 478 | 261 | 95 | 95 | 0 | |
| z3n | 0 | 721 | 122208.739 | 122186.103 | 721 | 482 | 239 | 113 | 84 | 0 | |
| CVC4 | 0 | 680 | 235500.889 | 235447.814 | 680 | 423 | 257 | 154 | 154 | 0 | |
| veriT | 0 | 610 | 320214.923 | 320170.329 | 610 | 362 | 248 | 224 | 224 | 0 | |
| MathSAT5n | 0 | 566 | 356482.137 | 356483.712 | 566 | 326 | 240 | 268 | 268 | 0 | |
| SMTInterpol | 0 | 535 | 410534.011 | 405159.63 | 535 | 303 | 232 | 299 | 299 | 0 | |
| SMTInterpol-fixedn | 0 | 535 | 410724.685 | 405305.573 | 535 | 303 | 232 | 299 | 299 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 490 | 66818.877 | 40240.697 | 490 | 490 | 0 | 344 | 82 | 0 |
| Yices2 | 0 | 486 | 43714.319 | 43713.35 | 486 | 486 | 0 | 348 | 92 | 0 |
| Yices2-fixedn | 0 | 486 | 43784.623 | 43772.185 | 486 | 486 | 0 | 348 | 92 | 0 |
| z3n | 0 | 482 | 48397.606 | 48377.255 | 482 | 482 | 0 | 352 | 84 | 0 |
| 2019-Z3n | 0 | 478 | 59807.796 | 59758.151 | 478 | 478 | 0 | 356 | 95 | 0 |
| CVC4 | 0 | 423 | 150474.754 | 150423.038 | 423 | 423 | 0 | 411 | 154 | 0 |
| veriT | 0 | 362 | 228006.542 | 227961.143 | 362 | 362 | 0 | 472 | 224 | 0 |
| MathSAT5n | 0 | 326 | 257334.842 | 257337.838 | 326 | 326 | 0 | 508 | 268 | 0 |
| SMTInterpol | 0 | 303 | 292797.388 | 289315.969 | 303 | 303 | 0 | 531 | 299 | 0 |
| SMTInterpol-fixedn | 0 | 303 | 292892.027 | 289379.356 | 303 | 303 | 0 | 531 | 299 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 262 | 63432.28 | 42043.747 | 262 | 0 | 262 | 572 | 82 | 0 |
| 2019-Z3n | 0 | 261 | 44984.199 | 44984.872 | 261 | 0 | 261 | 573 | 95 | 0 |
| CVC4 | 0 | 257 | 52626.136 | 52624.776 | 257 | 0 | 257 | 577 | 154 | 0 |
| Yices2 | 0 | 256 | 47771.326 | 47772.061 | 256 | 0 | 256 | 578 | 92 | 0 |
| Yices2-fixedn | 0 | 256 | 47945.276 | 47942.588 | 256 | 0 | 256 | 578 | 92 | 0 |
| veriT | 0 | 248 | 59808.381 | 59809.186 | 248 | 0 | 248 | 586 | 224 | 0 |
| MathSAT5n | 0 | 240 | 66747.295 | 66745.874 | 240 | 0 | 240 | 594 | 268 | 0 |
| z3n | 0 | 239 | 41411.132 | 41408.848 | 239 | 0 | 239 | 595 | 84 | 0 |
| SMTInterpol | 0 | 232 | 85336.624 | 83443.661 | 232 | 0 | 232 | 602 | 299 | 0 |
| SMTInterpol-fixedn | 0 | 232 | 85432.658 | 83526.218 | 232 | 0 | 232 | 602 | 299 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 672 | 7410.35 | 4845.351 | 672 | 438 | 234 | 162 | 162 | 0 | |
| Yices2 | 0 | 670 | 4966.996 | 4965.419 | 670 | 439 | 231 | 164 | 164 | 0 | |
| Yices2-fixedn | 0 | 669 | 4982.731 | 4966.236 | 669 | 438 | 231 | 165 | 165 | 0 | |
| 2019-Z3n | 0 | 623 | 6747.046 | 6695.638 | 623 | 403 | 220 | 211 | 211 | 0 | |
| z3n | 0 | 605 | 6590.321 | 6564.906 | 605 | 405 | 200 | 229 | 200 | 0 | |
| CVC4 | 0 | 447 | 11082.358 | 11070.213 | 447 | 240 | 207 | 387 | 387 | 0 | |
| MathSAT5n | 0 | 443 | 10674.752 | 10672.77 | 443 | 227 | 216 | 391 | 391 | 0 | |
| veriT | 0 | 415 | 11021.181 | 11021.246 | 415 | 195 | 220 | 419 | 419 | 0 | |
| SMTInterpol-fixedn | 0 | 349 | 15198.685 | 13235.643 | 349 | 172 | 177 | 485 | 485 | 0 | |
| SMTInterpol | 0 | 348 | 15192.707 | 13235.96 | 348 | 172 | 176 | 486 | 486 | 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.