The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the UFLIA division in the Single Query Track.
Page generated on 2019-07-23 17:56:09 +0000
Benchmarks: 2848 Time Limit: 2400 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Par4 | Par4 | Par4 | Par4 | Par4 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 1674 | 2872857.6 | 2836528.739 | 1674 | 8 | 1666 | 1174 | 1063 | 111 | |
| CVC4 | 0 | 1644 | 2876609.874 | 2944307.644 | 1644 | 5 | 1639 | 1204 | 1189 | 0 | |
| 2018-CVC4n | 0 | 1637 | 2908980.824 | 2926313.181 | 1637 | 5 | 1632 | 1211 | 1196 | 0 | |
| veriT | 0 | 1545 | 3112585.538 | 3112960.053 | 1545 | 0 | 1545 | 1303 | 1164 | 69 | |
| Vampire | 0 | 1423 | 3572991.47 | 3458795.006 | 1423 | 0 | 1423 | 1425 | 1425 | 0 | |
| Z3n | 0 | 1405 | 2058425.405 | 2064145.676 | 1405 | 6 | 1399 | 1443 | 595 | 20 | |
| Alt-Ergo | 0 | 1356 | 3633265.225 | 3559959.68 | 1356 | 0 | 1356 | 1492 | 1395 | 77 | |
| SMTInterpol | 0 | 47 | 6638832.092 | 6623072.118 | 47 | 5 | 42 | 2801 | 2750 | 0 | |
| UltimateEliminator+Yices-2.6.1 | 0 | 0 | 19808.146 | 23625.717 | 0 | 0 | 0 | 2848 | 7 | 0 | |
| UltimateEliminator+SMTInterpol | 0 | 0 | 21898.476 | 18623.415 | 0 | 0 | 0 | 2848 | 5 | 0 | |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 0 | 22286.482 | 19950.492 | 0 | 0 | 0 | 2848 | 5 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 1681 | 2890786.76 | 2831381.873 | 1681 | 8 | 1673 | 1167 | 1056 | 111 | |
| CVC4 | 0 | 1644 | 2942508.164 | 2944250.794 | 1644 | 5 | 1639 | 1204 | 1189 | 0 | |
| 2018-CVC4n | 0 | 1637 | 2925682.654 | 2926262.851 | 1637 | 5 | 1632 | 1211 | 1196 | 0 | |
| veriT | 0 | 1545 | 3112958.678 | 3112913.573 | 1545 | 0 | 1545 | 1303 | 1164 | 69 | |
| Vampire | 0 | 1479 | 4198978.49 | 3391947.714 | 1479 | 0 | 1479 | 1369 | 1369 | 0 | |
| Z3n | 0 | 1405 | 2058727.995 | 2064116.896 | 1405 | 6 | 1399 | 1443 | 595 | 20 | |
| Alt-Ergo | 0 | 1401 | 3831462.325 | 3500680.893 | 1401 | 0 | 1401 | 1447 | 1349 | 77 | |
| SMTInterpol | 0 | 47 | 6689951.452 | 6607955.483 | 47 | 5 | 42 | 2801 | 2730 | 0 | |
| UltimateEliminator+SMTInterpol | 0 | 0 | 21898.476 | 18623.415 | 0 | 0 | 0 | 2848 | 5 | 0 | |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 0 | 22286.482 | 19950.492 | 0 | 0 | 0 | 2848 | 5 | 0 | |
| UltimateEliminator+Yices-2.6.1 | 0 | 0 | 33196.806 | 23565.467 | 0 | 0 | 0 | 2848 | 6 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 8 | 11739.589 | 8727.378 | 8 | 8 | 0 | 2840 | 1056 | 111 |
| Z3n | 0 | 6 | 10057.916 | 10058.169 | 6 | 6 | 0 | 2842 | 595 | 20 |
| SMTInterpol | 0 | 5 | 10783.749 | 9273.208 | 5 | 5 | 0 | 2843 | 2730 | 0 |
| 2018-CVC4n | 0 | 5 | 12330.535 | 12386.645 | 5 | 5 | 0 | 2843 | 1196 | 0 |
| CVC4 | 0 | 5 | 14733.746 | 14910.887 | 5 | 5 | 0 | 2843 | 1189 | 0 |
| UltimateEliminator+SMTInterpol | 0 | 0 | 37.028 | 23.953 | 0 | 0 | 0 | 2848 | 5 | 0 |
| UltimateEliminator+Yices-2.6.1 | 0 | 0 | 36.489 | 25.129 | 0 | 0 | 0 | 2848 | 6 | 0 |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 0 | 37.127 | 26.845 | 0 | 0 | 0 | 2848 | 5 | 0 |
| Alt-Ergo | 0 | 0 | 21601.167 | 14297.389 | 0 | 0 | 0 | 2848 | 1349 | 77 |
| veriT | 0 | 0 | 16740.238 | 16740.594 | 0 | 0 | 0 | 2848 | 1164 | 69 |
| Vampire | 0 | 0 | 26400.0 | 26400.0 | 0 | 0 | 0 | 2848 | 1369 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 1673 | 193447.17 | 137054.495 | 1673 | 0 | 1673 | 1175 | 1056 | 111 |
| CVC4 | 0 | 1639 | 260187.921 | 261677.735 | 1639 | 0 | 1639 | 1209 | 1189 | 0 |
| 2018-CVC4n | 0 | 1632 | 251097.445 | 251578.196 | 1632 | 0 | 1632 | 1216 | 1196 | 0 |
| veriT | 0 | 1545 | 450641.826 | 450588.982 | 1545 | 0 | 1545 | 1303 | 1164 | 69 |
| Vampire | 0 | 1479 | 1040560.28 | 680849.824 | 1479 | 0 | 1479 | 1369 | 1369 | 0 |
| Alt-Ergo | 0 | 1401 | 1068457.35 | 833883.821 | 1401 | 0 | 1401 | 1447 | 1349 | 77 |
| Z3n | 0 | 1399 | 441021.895 | 441972.65 | 1399 | 0 | 1399 | 1449 | 595 | 20 |
| SMTInterpol | 0 | 42 | 4008936.378 | 3978280.922 | 42 | 0 | 42 | 2806 | 2730 | 0 |
| UltimateEliminator+SMTInterpol | 0 | 0 | 17990.102 | 16145.497 | 0 | 0 | 0 | 2848 | 5 | 0 |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 0 | 18236.732 | 17182.761 | 0 | 0 | 0 | 2848 | 5 | 0 |
| UltimateEliminator+Yices-2.6.1 | 0 | 0 | 26770.475 | 18451.849 | 0 | 0 | 0 | 2848 | 6 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 1583 | 32669.431 | 31293.423 | 1583 | 5 | 1578 | 1265 | 1154 | 111 | |
| 2018-CVC4n | 0 | 1450 | 35308.26 | 35303.124 | 1450 | 1 | 1449 | 1398 | 1397 | 0 | |
| CVC4 | 0 | 1448 | 35318.65 | 35311.629 | 1448 | 1 | 1447 | 1400 | 1399 | 0 | |
| veriT | 0 | 1445 | 35350.032 | 35341.118 | 1445 | 0 | 1445 | 1403 | 1315 | 69 | |
| Z3n | 0 | 1375 | 35888.239 | 35891.025 | 1375 | 6 | 1369 | 1473 | 1444 | 20 | |
| Alt-Ergo | 0 | 1222 | 49515.905 | 41610.236 | 1222 | 0 | 1222 | 1626 | 1536 | 77 | |
| Vampire | 0 | 1144 | 55770.176 | 44806.626 | 1144 | 0 | 1144 | 1704 | 1704 | 0 | |
| SMTInterpol | 0 | 43 | 66883.566 | 66792.645 | 43 | 5 | 38 | 2805 | 2780 | 0 | |
| UltimateEliminator+SMTInterpol | 0 | 0 | 10038.748 | 6376.413 | 0 | 0 | 0 | 2848 | 6 | 0 | |
| UltimateEliminator+Yices-2.6.1 | 0 | 0 | 10359.006 | 6992.747 | 0 | 0 | 0 | 2848 | 7 | 0 | |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 0 | 10488.142 | 7136.666 | 0 | 0 | 0 | 2848 | 9 | 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.