The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the Arith division in the Single Query Track.
Page generated on 2021-07-18 17:29:05 +0000
Benchmarks: 1511 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 | Vampire | cvc5 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 1451 | 113382.071 | 113360.72 | 1451 | 693 | 758 | 60 | 0 | 57 | 0 |
| 2020-z3n | 0 | 1429 | 142973.746 | 142875.829 | 1429 | 690 | 739 | 82 | 0 | 80 | 0 |
| 2019-Par4n | 0 | 1221 | 123474.489 | 111013.678 | 1221 | 593 | 628 | 82 | 208 | 82 | 0 |
| cvc5 - fixedn | 0 | 1182 | 382761.788 | 420998.731 | 1182 | 533 | 649 | 329 | 0 | 329 | 0 |
| cvc5 | 0 | 1181 | 389074.999 | 421793.153 | 1181 | 530 | 651 | 330 | 0 | 330 | 0 |
| 2020-CVC4n | 0 | 1150 | 374130.728 | 375690.902 | 1150 | 495 | 655 | 361 | 0 | 268 | 0 |
| UltimateEliminator+MathSAT | 0 | 906 | 707662.904 | 699530.1 | 906 | 335 | 571 | 605 | 0 | 551 | 0 |
| Vampire | 0 | 678 | 1001819.028 | 1000920.033 | 678 | 4 | 674 | 833 | 0 | 833 | 0 |
| Vampire - fixedn | 0 | 666 | 1006517.806 | 1003462.412 | 666 | 2 | 664 | 845 | 0 | 835 | 0 |
| Yices2-QS | 0 | 297 | 3875.305 | 3875.717 | 297 | 211 | 86 | 3 | 1211 | 3 | 0 |
| iProver | 0 | 120 | 1671021.539 | 1663449.802 | 120 | 0 | 120 | 1391 | 0 | 1329 | 55 |
| SMTInterpol | 0 | 67 | 74467.085 | 72236.115 | 67 | 5 | 62 | 1127 | 317 | 49 | 0 |
| veriT | 0 | 49 | 16176.927 | 16172.143 | 49 | 0 | 49 | 142 | 1320 | 13 | 0 |
| 2018-Z3n | 0 | 16 | 9.389 | 9.394 | 16 | 12 | 4 | 1 | 1494 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 1451 | 113386.051 | 113358.97 | 1451 | 693 | 758 | 60 | 0 | 57 | 0 |
| 2020-z3n | 0 | 1429 | 142978.936 | 142873.849 | 1429 | 690 | 739 | 82 | 0 | 80 | 0 |
| 2019-Par4n | 0 | 1234 | 133193.279 | 108082.293 | 1234 | 597 | 637 | 69 | 208 | 69 | 0 |
| cvc5 - fixedn | 0 | 1182 | 420947.626 | 420986.551 | 1182 | 533 | 649 | 329 | 0 | 329 | 0 |
| cvc5 | 0 | 1181 | 421791.499 | 421779.133 | 1181 | 530 | 651 | 330 | 0 | 330 | 0 |
| 2020-CVC4n | 0 | 1150 | 374788.068 | 375389.6 | 1150 | 495 | 655 | 361 | 0 | 267 | 0 |
| UltimateEliminator+MathSAT | 0 | 907 | 707672.194 | 699502.8 | 907 | 335 | 572 | 604 | 0 | 550 | 0 |
| Vampire | 0 | 684 | 1019203.368 | 996887.393 | 684 | 4 | 680 | 827 | 0 | 827 | 0 |
| Vampire - fixedn | 0 | 667 | 1013858.736 | 1001783.119 | 667 | 2 | 665 | 844 | 0 | 832 | 0 |
| Yices2-QS | 0 | 297 | 3875.555 | 3875.657 | 297 | 211 | 86 | 3 | 1211 | 3 | 0 |
| iProver | 0 | 123 | 1674638.779 | 1661669.321 | 123 | 0 | 123 | 1388 | 0 | 1326 | 55 |
| SMTInterpol | 0 | 67 | 74467.085 | 72236.115 | 67 | 5 | 62 | 1127 | 317 | 49 | 0 |
| veriT | 0 | 49 | 16178.357 | 16171.673 | 49 | 0 | 49 | 142 | 1320 | 13 | 0 |
| 2018-Z3n | 0 | 16 | 9.389 | 9.394 | 16 | 12 | 4 | 1 | 1494 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 693 | 21613.349 | 21613.928 | 693 | 693 | 0 | 12 | 806 | 57 | 0 |
| 2020-z3n | 0 | 690 | 27952.497 | 27949.521 | 690 | 690 | 0 | 15 | 806 | 80 | 0 |
| 2019-Par4n | 0 | 597 | 32814.648 | 24244.884 | 597 | 597 | 0 | 13 | 901 | 69 | 0 |
| cvc5 - fixedn | 0 | 533 | 221787.553 | 221804.87 | 533 | 533 | 0 | 172 | 806 | 329 | 0 |
| cvc5 | 0 | 530 | 224436.544 | 224480.184 | 530 | 530 | 0 | 175 | 806 | 330 | 0 |
| 2020-CVC4n | 0 | 495 | 172157.635 | 172640.532 | 495 | 495 | 0 | 210 | 806 | 267 | 0 |
| UltimateEliminator+MathSAT | 0 | 335 | 452896.624 | 449813.132 | 335 | 335 | 0 | 370 | 806 | 550 | 0 |
| Yices2-QS | 0 | 211 | 260.932 | 261.035 | 211 | 211 | 0 | 0 | 1300 | 3 | 0 |
| 2018-Z3n | 0 | 12 | 0.826 | 0.83 | 12 | 12 | 0 | 0 | 1499 | 0 | 0 |
| SMTInterpol | 0 | 5 | 60290.026 | 59091.023 | 5 | 5 | 0 | 477 | 1029 | 49 | 0 |
| Vampire | 0 | 4 | 852008.281 | 841191.721 | 4 | 4 | 0 | 701 | 806 | 827 | 0 |
| Vampire - fixedn | 0 | 2 | 847200.54 | 843592.141 | 2 | 2 | 0 | 703 | 806 | 832 | 0 |
| veriT | 0 | 0 | 101.196 | 94.377 | 0 | 0 | 0 | 83 | 1428 | 13 | 0 |
| iProver | 0 | 0 | 843600.974 | 843601.54 | 0 | 0 | 0 | 705 | 806 | 1326 | 55 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 758 | 72572.703 | 72545.043 | 758 | 0 | 758 | 32 | 721 | 57 | 0 |
| 2020-z3n | 0 | 739 | 95826.439 | 95724.328 | 739 | 0 | 739 | 51 | 721 | 80 | 0 |
| Vampire | 0 | 680 | 147995.087 | 136495.672 | 680 | 0 | 680 | 110 | 721 | 827 | 0 |
| Vampire - fixedn | 0 | 665 | 147458.195 | 138990.978 | 665 | 0 | 665 | 125 | 721 | 832 | 0 |
| 2020-CVC4n | 0 | 655 | 183430.433 | 183549.068 | 655 | 0 | 655 | 135 | 721 | 267 | 0 |
| cvc5 | 0 | 651 | 178154.955 | 178098.95 | 651 | 0 | 651 | 139 | 721 | 330 | 0 |
| cvc5 - fixedn | 0 | 649 | 179960.073 | 179981.681 | 649 | 0 | 649 | 141 | 721 | 329 | 0 |
| 2019-Par4n | 0 | 637 | 81178.631 | 64637.409 | 637 | 0 | 637 | 40 | 834 | 69 | 0 |
| UltimateEliminator+MathSAT | 0 | 572 | 235575.571 | 230489.668 | 572 | 0 | 572 | 218 | 721 | 550 | 0 |
| iProver | 0 | 123 | 811837.805 | 798867.781 | 123 | 0 | 123 | 667 | 721 | 1326 | 55 |
| Yices2-QS | 0 | 86 | 2414.623 | 2414.622 | 86 | 0 | 86 | 2 | 1423 | 3 | 0 |
| SMTInterpol | 0 | 62 | 14140.608 | 13130.848 | 62 | 0 | 62 | 635 | 814 | 49 | 0 |
| veriT | 0 | 49 | 16077.161 | 16077.296 | 49 | 0 | 49 | 59 | 1403 | 13 | 0 |
| 2018-Z3n | 0 | 4 | 8.563 | 8.563 | 4 | 0 | 4 | 1 | 1506 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 1316 | 5995.675 | 5994.54 | 1316 | 668 | 648 | 195 | 0 | 195 | 0 |
| 2020-z3n | 0 | 1296 | 6750.841 | 6724.343 | 1296 | 659 | 637 | 215 | 0 | 215 | 0 |
| 2019-Par4n | 0 | 1149 | 5213.052 | 4517.53 | 1149 | 569 | 580 | 154 | 208 | 154 | 0 |
| cvc5 - fixedn | 0 | 1037 | 11941.465 | 11941.161 | 1037 | 436 | 601 | 474 | 0 | 474 | 0 |
| cvc5 | 0 | 1037 | 11955.538 | 11952.657 | 1037 | 436 | 601 | 474 | 0 | 474 | 0 |
| 2020-CVC4n | 0 | 1029 | 12123.532 | 12117.5 | 1029 | 433 | 596 | 482 | 0 | 480 | 0 |
| UltimateEliminator+MathSAT | 0 | 750 | 24731.282 | 20853.337 | 750 | 285 | 465 | 761 | 0 | 707 | 0 |
| Vampire | 0 | 664 | 20903.444 | 20584.886 | 664 | 4 | 660 | 847 | 0 | 847 | 0 |
| Vampire - fixedn | 0 | 651 | 20965.544 | 20656.619 | 651 | 2 | 649 | 860 | 0 | 851 | 0 |
| Yices2-QS | 0 | 296 | 129.412 | 129.432 | 296 | 210 | 86 | 4 | 1211 | 4 | 0 |
| iProver | 0 | 104 | 34771.256 | 33959.846 | 104 | 0 | 104 | 1407 | 0 | 1345 | 55 |
| SMTInterpol | 0 | 67 | 4638.424 | 3258.14 | 67 | 5 | 62 | 1127 | 317 | 92 | 0 |
| veriT | 0 | 49 | 479.917 | 473.186 | 49 | 0 | 49 | 142 | 1320 | 15 | 0 |
| 2018-Z3n | 0 | 16 | 9.389 | 9.394 | 16 | 12 | 4 | 1 | 1494 | 0 | 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.