The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the UFLIA logic in the Single Query Track.
Page generated on 2022-08-10 11:17:45 +0000
Benchmarks: 2848 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| cvc5 | cvc5 | smtinterpol | cvc5 | veriT |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 1635 | 1463622.503 | 1479120.24 | 1635 | 1 | 1634 | 1213 | 1195 | 0 |
| 2020-CVC4n | 0 | 1615 | 1483336.789 | 1501651.32 | 1615 | 1 | 1614 | 1233 | 1214 | 0 |
| veriT | 0 | 1545 | 1547880.27 | 1547969.303 | 1545 | 0 | 1545 | 1303 | 1258 | 1 |
| Vampire | 0 | 1494 | 1693796.488 | 1629767.055 | 1494 | 0 | 1494 | 1354 | 1340 | 0 |
| z3-4.8.17n | 0 | 1398 | 1335620.494 | 1345546.228 | 1398 | 6 | 1392 | 1450 | 893 | 8 |
| smtinterpol | 0 | 413 | 2870460.888 | 2865303.645 | 413 | 2 | 411 | 2435 | 2366 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 19859.732 | 13625.639 | 0 | 0 | 0 | 2848 | 3 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 1635 | 1478725.813 | 1479064.74 | 1635 | 1 | 1634 | 1213 | 1195 | 0 |
| 2020-CVC4n | 0 | 1615 | 1501062.569 | 1501593.72 | 1615 | 1 | 1614 | 1233 | 1214 | 0 |
| Vampire | 0 | 1555 | 1978463.748 | 1587577.652 | 1555 | 0 | 1555 | 1293 | 1274 | 0 |
| veriT | 0 | 1545 | 1548044.64 | 1547919.973 | 1545 | 0 | 1545 | 1303 | 1258 | 1 |
| z3-4.8.17n | 0 | 1398 | 1337670.974 | 1345506.198 | 1398 | 6 | 1392 | 1450 | 893 | 8 |
| smtinterpol | 0 | 417 | 2927840.048 | 2853986.609 | 417 | 2 | 415 | 2431 | 2326 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 19859.732 | 13625.639 | 0 | 0 | 0 | 2848 | 3 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| z3-4.8.17n | 0 | 6 | 1200.918 | 1200.908 | 6 | 6 | 0 | 1 | 2841 | 893 | 8 |
| smtinterpol | 0 | 2 | 2407.751 | 2403.552 | 2 | 2 | 0 | 5 | 2841 | 2326 | 0 |
| 2020-CVC4n | 0 | 1 | 4641.486 | 4646.827 | 1 | 1 | 0 | 6 | 2841 | 1214 | 0 |
| cvc5 | 0 | 1 | 5837.303 | 5837.827 | 1 | 1 | 0 | 6 | 2841 | 1195 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 38.389 | 20.219 | 0 | 0 | 0 | 7 | 2841 | 3 | 0 |
| veriT | 0 | 0 | 4311.019 | 4311.081 | 0 | 0 | 0 | 7 | 2841 | 1258 | 1 |
| Vampire | 0 | 0 | 8400.0 | 8400.0 | 0 | 0 | 0 | 7 | 2841 | 1274 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 1634 | 125240.336 | 125575.311 | 1634 | 0 | 1634 | 70 | 1144 | 1195 | 0 |
| 2020-CVC4n | 0 | 1614 | 147421.005 | 147935.079 | 1614 | 0 | 1614 | 90 | 1144 | 1214 | 0 |
| Vampire | 0 | 1555 | 400453.208 | 214957.912 | 1555 | 0 | 1555 | 149 | 1144 | 1274 | 0 |
| veriT | 0 | 1545 | 211165.773 | 211144.515 | 1545 | 0 | 1545 | 159 | 1144 | 1258 | 1 |
| z3-4.8.17n | 0 | 1392 | 294749.959 | 296211.962 | 1392 | 0 | 1392 | 312 | 1144 | 893 | 8 |
| smtinterpol | 0 | 415 | 1588181.216 | 1566349.801 | 415 | 0 | 415 | 1289 | 1144 | 2326 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 13803.771 | 9964.676 | 0 | 0 | 0 | 1704 | 1144 | 3 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| veriT | 0 | 1462 | 34425.501 | 34405.956 | 1462 | 0 | 1462 | 1386 | 1365 | 1 |
| cvc5 | 0 | 1440 | 36578.627 | 36530.823 | 1440 | 0 | 1440 | 1408 | 1397 | 0 |
| 2020-CVC4n | 0 | 1427 | 35707.916 | 35666.746 | 1427 | 0 | 1427 | 1421 | 1410 | 0 |
| z3-4.8.17n | 0 | 1369 | 35935.62 | 35931.208 | 1369 | 6 | 1363 | 1479 | 1471 | 8 |
| Vampire | 0 | 1293 | 48646.259 | 40092.416 | 1293 | 0 | 1293 | 1555 | 1541 | 0 |
| smtinterpol | 0 | 330 | 61867.61 | 60033.795 | 330 | 2 | 328 | 2518 | 2449 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 15001.694 | 8880.805 | 0 | 0 | 0 | 2848 | 18 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.