The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_IDL logic in the Single Query Track.
Page generated on 2021-07-18 17:29:06 +0000
Benchmarks: 1138 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| YicesLS | YicesLS | YicesLS | YicesLS | YicesLS |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 1012 | 219068.067 | 218911.381 | 1012 | 624 | 388 | 126 | 126 | 0 |
| YicesLS | 0 | 1009 | 187459.02 | 187522.635 | 1009 | 625 | 384 | 129 | 63 | 0 |
| 2019-Par4n | 0 | 957 | 268949.214 | 230380.499 | 957 | 598 | 359 | 181 | 181 | 0 |
| Yices2 | 0 | 938 | 266139.525 | 266135.702 | 938 | 597 | 341 | 200 | 200 | 0 |
| cvc5 | 0 | 886 | 377285.784 | 377137.815 | 886 | 508 | 378 | 252 | 252 | 0 |
| cvc5 - fixedn | 0 | 885 | 377802.465 | 377760.238 | 885 | 507 | 378 | 253 | 253 | 0 |
| OpenSMT | 0 | 833 | 427048.645 | 426984.206 | 833 | 503 | 330 | 305 | 305 | 0 |
| OpenSMT - fixedn | 0 | 831 | 427488.222 | 427557.755 | 831 | 502 | 329 | 307 | 307 | 0 |
| veriT | 0 | 777 | 496096.148 | 496061.385 | 777 | 453 | 324 | 361 | 361 | 0 |
| MathSAT5n | 0 | 714 | 557014.538 | 557296.104 | 714 | 396 | 318 | 424 | 424 | 0 |
| SMTInterpol | 0 | 698 | 600641.751 | 591207.468 | 698 | 396 | 302 | 440 | 440 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 1012 | 219082.607 | 218906.451 | 1012 | 624 | 388 | 126 | 126 | 0 |
| YicesLS | 0 | 1009 | 187477.24 | 187520.935 | 1009 | 625 | 384 | 129 | 119 | 0 |
| 2019-Par4n | 0 | 1009 | 338429.864 | 201305.991 | 1009 | 623 | 386 | 129 | 129 | 0 |
| Yices2 | 0 | 938 | 266153.505 | 266130.682 | 938 | 597 | 341 | 200 | 200 | 0 |
| cvc5 | 0 | 886 | 377337.494 | 377126.155 | 886 | 508 | 378 | 252 | 252 | 0 |
| cvc5 - fixedn | 0 | 885 | 377853.335 | 377748.578 | 885 | 507 | 378 | 253 | 253 | 0 |
| OpenSMT | 0 | 833 | 427074.835 | 426975.516 | 833 | 503 | 330 | 305 | 305 | 0 |
| OpenSMT - fixedn | 0 | 831 | 427604.972 | 427547.185 | 831 | 502 | 329 | 307 | 307 | 0 |
| veriT | 0 | 777 | 496124.158 | 496051.585 | 777 | 453 | 324 | 361 | 361 | 0 |
| MathSAT5n | 0 | 714 | 557276.108 | 557277.764 | 714 | 396 | 318 | 424 | 424 | 0 |
| SMTInterpol | 0 | 698 | 600641.751 | 591207.468 | 698 | 396 | 302 | 440 | 440 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| YicesLS | 0 | 625 | 83020.431 | 83061.32 | 625 | 625 | 0 | 52 | 461 | 119 | 0 |
| z3n | 0 | 624 | 93776.92 | 93712.17 | 624 | 624 | 0 | 53 | 461 | 126 | 0 |
| 2019-Par4n | 0 | 623 | 158287.915 | 88503.56 | 623 | 623 | 0 | 54 | 461 | 129 | 0 |
| Yices2 | 0 | 597 | 111234.97 | 111214.333 | 597 | 597 | 0 | 80 | 461 | 200 | 0 |
| cvc5 | 0 | 508 | 257524.373 | 257450.965 | 508 | 508 | 0 | 169 | 461 | 252 | 0 |
| cvc5 - fixedn | 0 | 507 | 257994.164 | 257922.107 | 507 | 507 | 0 | 170 | 461 | 253 | 0 |
| OpenSMT | 0 | 503 | 251627.851 | 251548.899 | 503 | 503 | 0 | 174 | 461 | 305 | 0 |
| OpenSMT - fixedn | 0 | 502 | 251908.123 | 251857.628 | 502 | 502 | 0 | 175 | 461 | 307 | 0 |
| veriT | 0 | 453 | 319049.561 | 318977.394 | 453 | 453 | 0 | 224 | 461 | 361 | 0 |
| MathSAT5n | 0 | 396 | 374614.837 | 374621.254 | 396 | 396 | 0 | 281 | 461 | 424 | 0 |
| SMTInterpol | 0 | 396 | 390846.099 | 385270.979 | 396 | 396 | 0 | 281 | 461 | 440 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 388 | 89305.687 | 89194.281 | 388 | 0 | 388 | 43 | 707 | 126 | 0 |
| 2019-Par4n | 0 | 386 | 144141.948 | 76802.432 | 386 | 0 | 386 | 45 | 707 | 129 | 0 |
| YicesLS | 0 | 384 | 68457.479 | 68459.614 | 384 | 0 | 384 | 47 | 707 | 119 | 0 |
| cvc5 | 0 | 378 | 83813.121 | 83675.19 | 378 | 0 | 378 | 53 | 707 | 252 | 0 |
| cvc5 - fixedn | 0 | 378 | 83859.17 | 83826.471 | 378 | 0 | 378 | 53 | 707 | 253 | 0 |
| Yices2 | 0 | 341 | 118918.534 | 118916.35 | 341 | 0 | 341 | 90 | 707 | 200 | 0 |
| OpenSMT | 0 | 330 | 139446.984 | 139426.617 | 330 | 0 | 330 | 101 | 707 | 305 | 0 |
| OpenSMT - fixedn | 0 | 329 | 139696.849 | 139689.556 | 329 | 0 | 329 | 102 | 707 | 307 | 0 |
| veriT | 0 | 324 | 141074.597 | 141074.191 | 324 | 0 | 324 | 107 | 707 | 361 | 0 |
| MathSAT5n | 0 | 318 | 146661.27 | 146656.51 | 318 | 0 | 318 | 113 | 707 | 424 | 0 |
| SMTInterpol | 0 | 302 | 173795.651 | 169936.489 | 302 | 0 | 302 | 129 | 707 | 440 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| YicesLS | 0 | 833 | 8856.22 | 8889.543 | 833 | 526 | 307 | 305 | 305 | 0 |
| 2019-Par4n | 0 | 828 | 12258.517 | 8752.588 | 828 | 524 | 304 | 310 | 310 | 0 |
| Yices2 | 0 | 826 | 8876.584 | 8852.453 | 826 | 529 | 297 | 312 | 312 | 0 |
| z3n | 0 | 782 | 10654.202 | 10612.604 | 782 | 497 | 285 | 356 | 356 | 0 |
| OpenSMT | 0 | 572 | 15682.058 | 15629.848 | 572 | 304 | 268 | 566 | 566 | 0 |
| OpenSMT - fixedn | 0 | 571 | 15680.673 | 15645.13 | 571 | 303 | 268 | 567 | 567 | 0 |
| cvc5 | 0 | 562 | 16190.876 | 16159.357 | 562 | 285 | 277 | 576 | 576 | 0 |
| cvc5 - fixedn | 0 | 561 | 16241.406 | 16179.732 | 561 | 285 | 276 | 577 | 577 | 0 |
| MathSAT5n | 0 | 544 | 15816.333 | 15810.003 | 544 | 265 | 279 | 594 | 594 | 0 |
| veriT | 0 | 530 | 16026.547 | 16011.326 | 530 | 244 | 286 | 608 | 608 | 0 |
| SMTInterpol | 0 | 436 | 22246.201 | 19207.364 | 436 | 215 | 221 | 702 | 702 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.