The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_UF division in the Single Query Track.
Page generated on 2020-07-04 11:46:59 +0000
Benchmarks: 2800 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Yices2 | Yices2 | Yices2 | Yices2 | Yices2 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 2800 | 374.008 | 383.564 | 2800 | 1130 | 1670 | 0 | 0 | 0 | |
| Yices2-fixedn | 0 | 2800 | 374.281 | 388.793 | 2800 | 1130 | 1670 | 0 | 0 | 0 | |
| 2019-Yices 2.6.2n | 0 | 2800 | 376.185 | 386.994 | 2800 | 1130 | 1670 | 0 | 0 | 0 | |
| 2019-Par4n | 0 | 2800 | 496.93 | 376.245 | 2800 | 1130 | 1670 | 0 | 0 | 0 | |
| veriT | 0 | 2800 | 791.191 | 790.47 | 2800 | 1130 | 1670 | 0 | 0 | 0 | |
| z3n | 0 | 2799 | 5949.848 | 5913.735 | 2799 | 1130 | 1669 | 1 | 1 | 0 | |
| OpenSMT | 0 | 2798 | 9544.475 | 9488.887 | 2798 | 1130 | 1668 | 2 | 2 | 0 | |
| CVC4 | 0 | 2797 | 11686.981 | 11675.984 | 2797 | 1130 | 1667 | 3 | 3 | 0 | |
| SMTInterpol | 0 | 2765 | 59323.135 | 53413.445 | 2765 | 1130 | 1635 | 35 | 35 | 0 | |
| SMTInterpol-fixedn | 0 | 2765 | 59331.033 | 53428.112 | 2765 | 1130 | 1635 | 35 | 35 | 0 | |
| MathSAT5n | 0 | 2745 | 45284.991 | 45280.054 | 2745 | 1113 | 1632 | 55 | 34 | 0 | |
| Alt-Ergo | 0 | 1164 | 1222753.458 | 957418.664 | 1164 | 0 | 1164 | 1636 | 654 | 19 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 2800 | 496.93 | 376.245 | 2800 | 1130 | 1670 | 0 | 0 | 0 | |
| Yices2 | 0 | 2800 | 374.008 | 383.564 | 2800 | 1130 | 1670 | 0 | 0 | 0 | |
| 2019-Yices 2.6.2n | 0 | 2800 | 376.185 | 386.994 | 2800 | 1130 | 1670 | 0 | 0 | 0 | |
| Yices2-fixedn | 0 | 2800 | 374.281 | 388.793 | 2800 | 1130 | 1670 | 0 | 0 | 0 | |
| veriT | 0 | 2800 | 791.191 | 790.47 | 2800 | 1130 | 1670 | 0 | 0 | 0 | |
| z3n | 0 | 2799 | 5949.848 | 5913.735 | 2799 | 1130 | 1669 | 1 | 1 | 0 | |
| OpenSMT | 0 | 2798 | 9544.665 | 9488.857 | 2798 | 1130 | 1668 | 2 | 2 | 0 | |
| CVC4 | 0 | 2797 | 11687.231 | 11675.934 | 2797 | 1130 | 1667 | 3 | 3 | 0 | |
| SMTInterpol | 0 | 2765 | 59323.135 | 53413.445 | 2765 | 1130 | 1635 | 35 | 35 | 0 | |
| SMTInterpol-fixedn | 0 | 2765 | 59331.033 | 53428.112 | 2765 | 1130 | 1635 | 35 | 35 | 0 | |
| MathSAT5n | 0 | 2745 | 45289.771 | 45278.494 | 2745 | 1113 | 1632 | 55 | 34 | 0 | |
| Alt-Ergo | 0 | 1415 | 1594315.558 | 791512.757 | 1415 | 0 | 1415 | 1385 | 352 | 19 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 1130 | 47.447 | 51.941 | 1130 | 1130 | 0 | 1670 | 0 | 0 |
| 2019-Par4n | 0 | 1130 | 21.092 | 53.343 | 1130 | 1130 | 0 | 1670 | 0 | 0 |
| 2019-Yices 2.6.2n | 0 | 1130 | 48.682 | 53.867 | 1130 | 1130 | 0 | 1670 | 0 | 0 |
| Yices2-fixedn | 0 | 1130 | 47.507 | 54.452 | 1130 | 1130 | 0 | 1670 | 0 | 0 |
| veriT | 0 | 1130 | 107.604 | 106.694 | 1130 | 1130 | 0 | 1670 | 0 | 0 |
| z3n | 0 | 1130 | 199.771 | 199.9 | 1130 | 1130 | 0 | 1670 | 1 | 0 |
| OpenSMT | 0 | 1130 | 429.615 | 428.869 | 1130 | 1130 | 0 | 1670 | 2 | 0 |
| CVC4 | 0 | 1130 | 1004.907 | 1003.098 | 1130 | 1130 | 0 | 1670 | 3 | 0 |
| SMTInterpol | 0 | 1130 | 2659.411 | 1084.878 | 1130 | 1130 | 0 | 1670 | 35 | 0 |
| SMTInterpol-fixedn | 0 | 1130 | 2632.145 | 1085.452 | 1130 | 1130 | 0 | 1670 | 35 | 0 |
| MathSAT5n | 0 | 1113 | 131.999 | 132.117 | 1113 | 1113 | 0 | 1687 | 34 | 0 |
| Alt-Ergo | 0 | 0 | 426891.637 | 270549.507 | 0 | 0 | 0 | 2800 | 352 | 19 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 1670 | 475.838 | 322.902 | 1670 | 0 | 1670 | 1130 | 0 | 0 |
| Yices2 | 0 | 1670 | 326.562 | 331.624 | 1670 | 0 | 1670 | 1130 | 0 | 0 |
| 2019-Yices 2.6.2n | 0 | 1670 | 327.503 | 333.127 | 1670 | 0 | 1670 | 1130 | 0 | 0 |
| Yices2-fixedn | 0 | 1670 | 326.773 | 334.341 | 1670 | 0 | 1670 | 1130 | 0 | 0 |
| veriT | 0 | 1670 | 683.587 | 683.776 | 1670 | 0 | 1670 | 1130 | 0 | 0 |
| z3n | 0 | 1669 | 5750.077 | 5713.835 | 1669 | 0 | 1669 | 1131 | 1 | 0 |
| OpenSMT | 0 | 1668 | 9115.05 | 9059.988 | 1668 | 0 | 1668 | 1132 | 2 | 0 |
| CVC4 | 0 | 1667 | 10682.324 | 10672.836 | 1667 | 0 | 1667 | 1133 | 3 | 0 |
| SMTInterpol | 0 | 1635 | 56663.725 | 52328.567 | 1635 | 0 | 1635 | 1165 | 35 | 0 |
| SMTInterpol-fixedn | 0 | 1635 | 56698.888 | 52342.66 | 1635 | 0 | 1635 | 1165 | 35 | 0 |
| MathSAT5n | 0 | 1632 | 45157.772 | 45146.377 | 1632 | 0 | 1632 | 1168 | 34 | 0 |
| Alt-Ergo | 0 | 1415 | 1167423.921 | 520963.25 | 1415 | 0 | 1415 | 1385 | 352 | 19 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 2798 | 188.71 | 246.037 | 2798 | 1130 | 1668 | 2 | 2 | 0 | |
| Yices2 | 0 | 2798 | 247.793 | 257.345 | 2798 | 1130 | 1668 | 2 | 2 | 0 | |
| 2019-Yices 2.6.2n | 0 | 2798 | 248.427 | 259.218 | 2798 | 1130 | 1668 | 2 | 2 | 0 | |
| Yices2-fixedn | 0 | 2798 | 247.625 | 262.126 | 2798 | 1130 | 1668 | 2 | 2 | 0 | |
| veriT | 0 | 2798 | 351.712 | 350.944 | 2798 | 1130 | 1668 | 2 | 2 | 0 | |
| z3n | 0 | 2769 | 1986.953 | 1975.666 | 2769 | 1128 | 1641 | 31 | 31 | 0 | |
| OpenSMT | 0 | 2766 | 2770.973 | 2760.091 | 2766 | 1127 | 1639 | 34 | 34 | 0 | |
| CVC4 | 0 | 2760 | 2974.161 | 2961.799 | 2760 | 1127 | 1633 | 40 | 40 | 0 | |
| SMTInterpol | 0 | 2719 | 11269.114 | 5793.57 | 2719 | 1129 | 1590 | 81 | 81 | 0 | |
| SMTInterpol-fixedn | 0 | 2719 | 11282.511 | 5796.493 | 2719 | 1129 | 1590 | 81 | 81 | 0 | |
| MathSAT5n | 0 | 2715 | 2419.792 | 2408.116 | 2715 | 1113 | 1602 | 85 | 64 | 0 | |
| Alt-Ergo | 0 | 777 | 72671.753 | 51200.421 | 777 | 0 | 777 | 2023 | 1770 | 19 |
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.