The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the UF division in the Single Query Track.
Page generated on 2019-07-23 17:56:09 +0000
Benchmarks: 2816 Time Limit: 2400 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| CVC4 | Vampire | Vampire | Par4 | Vampire |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 1141 | 4406118.838 | 4436448.822 | 1141 | 376 | 765 | 1675 | 1675 | 0 | |
| 2018-CVC4n | 0 | 1130 | 4244586.494 | 4260633.827 | 1130 | 371 | 759 | 1686 | 1686 | 0 | |
| Par4 | 0 | 1128 | 4575063.664 | 4226640.975 | 1128 | 363 | 765 | 1688 | 1420 | 268 | |
| Vampire | 0 | 1120 | 4233800.251 | 4111634.178 | 1120 | 423 | 697 | 1696 | 1696 | 0 | |
| 2018-Vampiren | 0 | 1078 | 4381857.552 | 4224340.257 | 1078 | 427 | 651 | 1738 | 1738 | 0 | |
| veriT | 0 | 665 | 5111250.699 | 5111636.509 | 665 | 0 | 665 | 2151 | 1855 | 158 | |
| Alt-Ergo | 0 | 640 | 5157073.351 | 5117379.075 | 640 | 0 | 640 | 2176 | 2035 | 91 | |
| Z3n | 0 | 455 | 3237148.569 | 3237695.064 | 455 | 41 | 414 | 2361 | 861 | 67 | |
| SMTInterpol | 0 | 16 | 6695278.855 | 6679894.107 | 16 | 4 | 12 | 2800 | 2777 | 0 | |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 0 | 10021.874 | 7369.04 | 0 | 0 | 0 | 2816 | 0 | 0 | |
| UltimateEliminator+SMTInterpol | 0 | 0 | 16950.182 | 13252.991 | 0 | 0 | 0 | 2816 | 3 | 0 | |
| UltimateEliminator+Yices-2.6.1 | 0 | 0 | 17216.907 | 13888.844 | 0 | 0 | 0 | 2816 | 3 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2018-Vampiren | 0 | 1171 | 6257667.952 | 4099803.018 | 1171 | 434 | 737 | 1645 | 1645 | 0 | |
| Vampire | 0 | 1157 | 5071140.731 | 4070434.872 | 1157 | 427 | 730 | 1659 | 1659 | 0 | |
| Par4 | 0 | 1142 | 4585000.064 | 4207563.01 | 1142 | 370 | 772 | 1674 | 1406 | 268 | |
| CVC4 | 0 | 1141 | 4430946.398 | 4436373.452 | 1141 | 376 | 765 | 1675 | 1675 | 0 | |
| 2018-CVC4n | 0 | 1130 | 4257953.294 | 4260560.957 | 1130 | 371 | 759 | 1686 | 1686 | 0 | |
| veriT | 0 | 665 | 5112293.149 | 5111316.269 | 665 | 0 | 665 | 2151 | 1851 | 158 | |
| Alt-Ergo | 0 | 664 | 5371320.651 | 5088014.59 | 664 | 0 | 664 | 2152 | 2011 | 91 | |
| Z3n | 0 | 455 | 3237499.609 | 3237656.524 | 455 | 41 | 414 | 2361 | 861 | 67 | |
| SMTInterpol | 0 | 16 | 6815660.745 | 6664398.447 | 16 | 4 | 12 | 2800 | 2744 | 0 | |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 0 | 10021.874 | 7369.04 | 0 | 0 | 0 | 2816 | 0 | 0 | |
| UltimateEliminator+SMTInterpol | 0 | 0 | 16950.182 | 13252.991 | 0 | 0 | 0 | 2816 | 3 | 0 | |
| UltimateEliminator+Yices-2.6.1 | 0 | 0 | 17216.907 | 13888.844 | 0 | 0 | 0 | 2816 | 3 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2018-Vampiren | 0 | 434 | 157419.768 | 75400.861 | 434 | 434 | 0 | 2382 | 1645 | 0 |
| Vampire | 0 | 427 | 180023.992 | 95517.912 | 427 | 427 | 0 | 2389 | 1659 | 0 |
| CVC4 | 0 | 376 | 558407.519 | 563371.256 | 376 | 376 | 0 | 2440 | 1675 | 0 |
| 2018-CVC4n | 0 | 371 | 393712.229 | 396192.331 | 371 | 371 | 0 | 2445 | 1686 | 0 |
| Par4 | 0 | 370 | 710592.709 | 381552.636 | 370 | 370 | 0 | 2446 | 1406 | 268 |
| Z3n | 0 | 41 | 584817.156 | 584856.326 | 41 | 41 | 0 | 2775 | 861 | 67 |
| SMTInterpol | 0 | 4 | 1093231.24 | 1072619.475 | 4 | 4 | 0 | 2812 | 2744 | 0 |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 0 | 1608.55 | 1077.024 | 0 | 0 | 0 | 2816 | 0 | 0 |
| UltimateEliminator+SMTInterpol | 0 | 0 | 8793.984 | 8182.676 | 0 | 0 | 0 | 2816 | 3 | 0 |
| UltimateEliminator+Yices-2.6.1 | 0 | 0 | 8792.47 | 8277.231 | 0 | 0 | 0 | 2816 | 3 | 0 |
| Alt-Ergo | 0 | 0 | 1037976.002 | 1006996.028 | 0 | 0 | 0 | 2816 | 2011 | 91 |
| veriT | 0 | 0 | 1039068.218 | 1039073.236 | 0 | 0 | 0 | 2816 | 1851 | 158 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 772 | 212007.356 | 163610.373 | 772 | 0 | 772 | 2044 | 1406 | 268 |
| CVC4 | 0 | 765 | 210138.879 | 210602.197 | 765 | 0 | 765 | 2051 | 1675 | 0 |
| 2018-CVC4n | 0 | 759 | 201841.065 | 201968.625 | 759 | 0 | 759 | 2057 | 1686 | 0 |
| 2018-Vampiren | 0 | 737 | 918615.444 | 363787.298 | 737 | 0 | 737 | 2079 | 1645 | 0 |
| Vampire | 0 | 730 | 595102.038 | 313020.29 | 730 | 0 | 730 | 2086 | 1659 | 0 |
| veriT | 0 | 665 | 426531.004 | 426519.5 | 665 | 0 | 665 | 2151 | 1851 | 158 |
| Alt-Ergo | 0 | 664 | 576044.213 | 441301.567 | 664 | 0 | 664 | 2152 | 2011 | 91 |
| Z3n | 0 | 414 | 611765.708 | 611779.48 | 414 | 0 | 414 | 2402 | 861 | 67 |
| SMTInterpol | 0 | 12 | 2003103.087 | 1953209.807 | 12 | 0 | 12 | 2804 | 2744 | 0 |
| UltimateEliminator+SMTInterpol | 0 | 0 | 2881.321 | 1784.656 | 0 | 0 | 0 | 2816 | 3 | 0 |
| UltimateEliminator+Yices-2.6.1 | 0 | 0 | 2976.003 | 1975.203 | 0 | 0 | 0 | 2816 | 3 | 0 |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 0 | 2987.91 | 2670.385 | 0 | 0 | 0 | 2816 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2018-Vampiren | 0 | 847 | 54045.681 | 49072.359 | 847 | 392 | 455 | 1969 | 1969 | 0 | |
| Vampire | 0 | 774 | 58178.322 | 51417.485 | 774 | 263 | 511 | 2042 | 2042 | 0 | |
| Par4 | 0 | 718 | 52111.04 | 51030.731 | 718 | 47 | 671 | 2098 | 1830 | 268 | |
| CVC4 | 0 | 606 | 53596.519 | 53582.489 | 606 | 7 | 599 | 2210 | 2210 | 0 | |
| 2018-CVC4n | 0 | 606 | 53619.463 | 53616.958 | 606 | 7 | 599 | 2210 | 2210 | 0 | |
| veriT | 0 | 603 | 53868.688 | 53853.304 | 603 | 0 | 603 | 2213 | 2033 | 158 | |
| Alt-Ergo | 0 | 563 | 57194.142 | 54238.07 | 563 | 0 | 563 | 2253 | 2122 | 91 | |
| Z3n | 0 | 412 | 58138.267 | 58114.758 | 412 | 38 | 374 | 2404 | 2332 | 67 | |
| SMTInterpol | 0 | 10 | 67264.719 | 67221.542 | 10 | 4 | 6 | 2806 | 2799 | 0 | |
| UltimateEliminator+SMTInterpol | 0 | 0 | 9822.182 | 6124.991 | 0 | 0 | 0 | 2816 | 3 | 0 | |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 0 | 10041.565 | 6703.206 | 0 | 0 | 0 | 2816 | 1 | 0 | |
| UltimateEliminator+Yices-2.6.1 | 0 | 0 | 10088.907 | 6760.844 | 0 | 0 | 0 | 2816 | 3 | 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.