The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_LinearIntArith division in the Single Query Track.
Page generated on 2022-08-10 11:17:45 +0000
Benchmarks: 7430 Time Limit: 1200 seconds Memory Limit: 60 GB
Logics:| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| OpenSMT | OpenSMT | Z3++ | cvc5 | Yices2 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 7117 | 462337.315 | 400831.811 | 7117 | 4554 | 2563 | 313 | 0 | 304 | 9 |
| OpenSMT | 0 | 6828 | 1096967.146 | 1096616.535 | 6828 | 4331 | 2497 | 595 | 7 | 589 | 0 |
| Z3++ | 0 | 6805 | 1016387.29 | 1019736.742 | 6805 | 4502 | 2303 | 618 | 7 | 589 | 10 |
| cvc5 | 0 | 6793 | 1157778.615 | 1157546.347 | 6793 | 4292 | 2501 | 637 | 0 | 636 | 0 |
| Yices2 | 0 | 6768 | 889765.982 | 889746.783 | 6768 | 4301 | 2467 | 662 | 0 | 662 | 0 |
| MathSATn | 0 | 6705 | 1154937.613 | 1154708.752 | 6705 | 4254 | 2451 | 725 | 0 | 725 | 0 |
| z3-4.8.17n | 0 | 6667 | 1169666.322 | 1169276.368 | 6667 | 4440 | 2227 | 763 | 0 | 737 | 5 |
| smtinterpol | 0 | 6431 | 1573517.317 | 1481591.901 | 6431 | 4003 | 2428 | 999 | 0 | 999 | 0 |
| veriT | 0 | 5004 | 2577129.266 | 2577133.761 | 5004 | 3446 | 1558 | 2426 | 0 | 2014 | 1 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 7194 | 575760.685 | 363616.649 | 7194 | 4598 | 2596 | 236 | 0 | 227 | 9 |
| OpenSMT | 0 | 6828 | 1097021.206 | 1096597.165 | 6828 | 4331 | 2497 | 595 | 7 | 589 | 0 |
| Z3++ | 0 | 6805 | 1016459.75 | 1019712.782 | 6805 | 4502 | 2303 | 618 | 7 | 589 | 10 |
| cvc5 | 0 | 6793 | 1157879.925 | 1157520.067 | 6793 | 4292 | 2501 | 637 | 0 | 636 | 0 |
| Yices2 | 0 | 6768 | 889821.582 | 889725.963 | 6768 | 4301 | 2467 | 662 | 0 | 662 | 0 |
| MathSATn | 0 | 6705 | 1155036.333 | 1154680.682 | 6705 | 4254 | 2451 | 725 | 0 | 725 | 0 |
| z3-4.8.17n | 0 | 6667 | 1169760.142 | 1169246.828 | 6667 | 4440 | 2227 | 763 | 0 | 737 | 5 |
| smtinterpol | 0 | 6444 | 1576295.637 | 1477864.144 | 6444 | 4003 | 2441 | 986 | 0 | 986 | 0 |
| veriT | 0 | 5004 | 2577291.476 | 2577060.781 | 5004 | 3446 | 1558 | 2426 | 0 | 2014 | 1 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 4598 | 269194.796 | 150140.952 | 4598 | 4598 | 0 | 86 | 2746 | 227 | 9 |
| Z3++ | 0 | 4502 | 341428.12 | 342762.789 | 4502 | 4502 | 0 | 181 | 2747 | 589 | 10 |
| z3-4.8.17n | 0 | 4440 | 409731.554 | 409494.481 | 4440 | 4440 | 0 | 244 | 2746 | 737 | 5 |
| OpenSMT | 0 | 4331 | 695202.704 | 695006.309 | 4331 | 4331 | 0 | 352 | 2747 | 589 | 0 |
| Yices2 | 0 | 4301 | 535460.096 | 535420.064 | 4301 | 4301 | 0 | 383 | 2746 | 662 | 0 |
| cvc5 | 0 | 4292 | 678110.675 | 677912.564 | 4292 | 4292 | 0 | 392 | 2746 | 636 | 0 |
| MathSATn | 0 | 4254 | 651270.707 | 651025.417 | 4254 | 4254 | 0 | 430 | 2746 | 725 | 0 |
| smtinterpol | 0 | 4003 | 1013459.724 | 984273.311 | 4003 | 4003 | 0 | 681 | 2746 | 986 | 0 |
| veriT | 0 | 3446 | 1211097.573 | 1210865.74 | 3446 | 3446 | 0 | 1238 | 2746 | 2014 | 1 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 2596 | 196165.889 | 103075.697 | 2596 | 0 | 2596 | 58 | 4776 | 227 | 9 |
| cvc5 | 0 | 2501 | 369369.25 | 369207.503 | 2501 | 0 | 2501 | 153 | 4776 | 636 | 0 |
| OpenSMT | 0 | 2497 | 291418.502 | 291190.856 | 2497 | 0 | 2497 | 151 | 4782 | 589 | 0 |
| Yices2 | 0 | 2467 | 243961.487 | 243905.899 | 2467 | 0 | 2467 | 187 | 4776 | 662 | 0 |
| MathSATn | 0 | 2451 | 393365.626 | 393255.265 | 2451 | 0 | 2451 | 203 | 4776 | 725 | 0 |
| smtinterpol | 0 | 2441 | 452435.913 | 383190.833 | 2441 | 0 | 2441 | 213 | 4776 | 986 | 0 |
| Z3++ | 0 | 2303 | 570369.464 | 571265.179 | 2303 | 0 | 2303 | 345 | 4782 | 589 | 10 |
| z3-4.8.17n | 0 | 2227 | 649628.588 | 649352.347 | 2227 | 0 | 2227 | 427 | 4776 | 737 | 5 |
| veriT | 0 | 1558 | 1255793.903 | 1255795.04 | 1558 | 0 | 1558 | 1096 | 4776 | 2014 | 1 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 6924 | 25294.286 | 16684.161 | 6924 | 4432 | 2492 | 506 | 0 | 497 | 9 |
| Yices2 | 0 | 6428 | 28914.147 | 28902.855 | 6428 | 4047 | 2381 | 1002 | 0 | 1002 | 0 |
| z3-4.8.17n | 0 | 5565 | 54578.403 | 54343.705 | 5565 | 3853 | 1712 | 1865 | 0 | 1839 | 5 |
| Z3++ | 0 | 5503 | 55820.585 | 55732.865 | 5503 | 3830 | 1673 | 1920 | 7 | 1909 | 10 |
| MathSATn | 0 | 5396 | 56638.345 | 56427.38 | 5396 | 3577 | 1819 | 2034 | 0 | 2034 | 0 |
| OpenSMT | 0 | 5167 | 64811.701 | 64664.87 | 5167 | 3260 | 1907 | 2256 | 7 | 2250 | 0 |
| cvc5 | 0 | 4979 | 68314.088 | 68112.142 | 4979 | 3331 | 1648 | 2451 | 0 | 2451 | 0 |
| smtinterpol | 0 | 4804 | 92001.069 | 75540.844 | 4804 | 3138 | 1666 | 2626 | 0 | 2626 | 0 |
| veriT | 0 | 4455 | 68576.834 | 68499.743 | 4455 | 3087 | 1368 | 2975 | 0 | 2644 | 1 |
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.