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 2022-08-10 11:17:45 +0000
Benchmarks: 1204 Time Limit: 1200 seconds Memory Limit: 60 GB
Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
---|---|---|---|---|
Z3++ | Z3++ | Z3++ | Z3++ | Yices2 |
Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
---|---|---|---|---|---|---|---|---|---|---|
Z3++ | 0 | 1049 | 248709.844 | 248685.407 | 1049 | 656 | 393 | 155 | 155 | 0 |
z3-4.8.17n | 0 | 1000 | 282237.079 | 282212.194 | 1000 | 638 | 362 | 204 | 183 | 0 |
2019-Par4n | 0 | 980 | 322061.046 | 282368.236 | 980 | 619 | 361 | 224 | 224 | 0 |
Yices2 | 0 | 968 | 314738.395 | 314707.26 | 968 | 625 | 343 | 236 | 236 | 0 |
cvc5 | 0 | 904 | 441256.929 | 441148.777 | 904 | 527 | 377 | 300 | 300 | 0 |
OpenSMT | 0 | 884 | 444917.541 | 444861.438 | 884 | 561 | 323 | 320 | 320 | 0 |
veriT | 0 | 781 | 562839.517 | 562849.668 | 781 | 461 | 320 | 423 | 423 | 0 |
MathSATn | 0 | 742 | 599214.086 | 599224.487 | 742 | 421 | 321 | 462 | 462 | 0 |
smtinterpol | 0 | 693 | 689810.345 | 675508.638 | 693 | 422 | 271 | 511 | 511 | 0 |
Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
---|---|---|---|---|---|---|---|---|---|---|
Z3++ | 0 | 1049 | 248725.234 | 248679.737 | 1049 | 656 | 393 | 155 | 155 | 0 |
2019-Par4n | 0 | 1039 | 417767.476 | 253638.196 | 1039 | 649 | 390 | 165 | 165 | 0 |
z3-4.8.17n | 0 | 1000 | 282260.559 | 282205.514 | 1000 | 638 | 362 | 204 | 183 | 0 |
Yices2 | 0 | 968 | 314757.895 | 314699.5 | 968 | 625 | 343 | 236 | 236 | 0 |
cvc5 | 0 | 904 | 441319.109 | 441134.397 | 904 | 527 | 377 | 300 | 300 | 0 |
OpenSMT | 0 | 884 | 444942.761 | 444851.008 | 884 | 561 | 323 | 320 | 320 | 0 |
veriT | 0 | 781 | 562876.237 | 562836.248 | 781 | 461 | 320 | 423 | 423 | 0 |
MathSATn | 0 | 742 | 599280.276 | 599206.987 | 742 | 421 | 321 | 462 | 462 | 0 |
smtinterpol | 0 | 701 | 690908.345 | 673145.867 | 701 | 422 | 279 | 503 | 503 | 0 |
Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
---|---|---|---|---|---|---|---|---|---|---|---|
Z3++ | 0 | 656 | 107725.386 | 107679.737 | 656 | 656 | 0 | 54 | 494 | 155 | 0 |
2019-Par4n | 0 | 649 | 181658.764 | 100679.547 | 649 | 649 | 0 | 61 | 494 | 165 | 0 |
z3-4.8.17n | 0 | 638 | 120621.346 | 120622.643 | 638 | 638 | 0 | 72 | 494 | 183 | 0 |
Yices2 | 0 | 625 | 121762.697 | 121753.644 | 625 | 625 | 0 | 85 | 494 | 236 | 0 |
OpenSMT | 0 | 561 | 226566.6 | 226527.583 | 561 | 561 | 0 | 149 | 494 | 320 | 0 |
cvc5 | 0 | 527 | 274893.28 | 274772.299 | 527 | 527 | 0 | 183 | 494 | 300 | 0 |
veriT | 0 | 461 | 346010.251 | 345972.622 | 461 | 461 | 0 | 249 | 494 | 423 | 0 |
smtinterpol | 0 | 422 | 397409.442 | 391532.283 | 422 | 422 | 0 | 288 | 494 | 503 | 0 |
MathSATn | 0 | 421 | 379024.804 | 378955.238 | 421 | 421 | 0 | 289 | 494 | 462 | 0 |
Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
---|---|---|---|---|---|---|---|---|---|---|---|
Z3++ | 0 | 393 | 65399.848 | 65400.0 | 393 | 0 | 393 | 38 | 773 | 155 | 0 |
2019-Par4n | 0 | 390 | 160508.712 | 77358.649 | 390 | 0 | 390 | 41 | 773 | 165 | 0 |
cvc5 | 0 | 377 | 90825.829 | 90762.098 | 377 | 0 | 377 | 54 | 773 | 300 | 0 |
z3-4.8.17n | 0 | 362 | 86039.213 | 85982.87 | 362 | 0 | 362 | 69 | 773 | 183 | 0 |
Yices2 | 0 | 343 | 117395.198 | 117345.856 | 343 | 0 | 343 | 88 | 773 | 236 | 0 |
OpenSMT | 0 | 323 | 142776.161 | 142723.425 | 323 | 0 | 323 | 108 | 773 | 320 | 0 |
MathSATn | 0 | 321 | 144655.472 | 144651.749 | 321 | 0 | 321 | 110 | 773 | 462 | 0 |
veriT | 0 | 320 | 141265.985 | 141263.626 | 320 | 0 | 320 | 111 | 773 | 423 | 0 |
smtinterpol | 0 | 279 | 217898.903 | 206013.583 | 279 | 0 | 279 | 152 | 773 | 503 | 0 |
Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
---|---|---|---|---|---|---|---|---|---|---|
2019-Par4n | 0 | 864 | 13108.557 | 9509.514 | 864 | 559 | 305 | 340 | 340 | 0 |
Yices2 | 0 | 849 | 9737.725 | 9725.129 | 849 | 551 | 298 | 355 | 355 | 0 |
Z3++ | 0 | 792 | 12052.363 | 12035.852 | 792 | 505 | 287 | 412 | 412 | 0 |
z3-4.8.17n | 0 | 779 | 11761.172 | 11727.728 | 779 | 504 | 275 | 425 | 404 | 0 |
OpenSMT | 0 | 605 | 16739.435 | 16702.467 | 605 | 333 | 272 | 599 | 599 | 0 |
MathSATn | 0 | 567 | 17086.096 | 17045.308 | 567 | 291 | 276 | 637 | 637 | 0 |
cvc5 | 0 | 557 | 18275.397 | 18182.336 | 557 | 298 | 259 | 647 | 647 | 0 |
veriT | 0 | 541 | 17447.15 | 17438.712 | 541 | 261 | 280 | 663 | 663 | 0 |
smtinterpol | 0 | 412 | 23872.153 | 21112.615 | 412 | 222 | 190 | 792 | 792 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.