The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the AUFLIA division in the Single Query Track.
Page generated on 2020-07-04 11:46:58 +0000
Benchmarks: 1310 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Vampire | Vampire | CVC4 | Vampire | Vampire |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2018-CVC4n | 0 | 1098 | 257281.701 | 262511.043 | 1098 | 111 | 987 | 212 | 199 | 0 | |
| Vampire | 0 | 1097 | 261861.107 | 257390.735 | 1097 | 81 | 1016 | 213 | 213 | 0 | |
| CVC4 | 0 | 1092 | 255795.226 | 261782.87 | 1092 | 107 | 985 | 218 | 201 | 0 | |
| z3n | 0 | 1029 | 321149.757 | 323125.81 | 1029 | 121 | 908 | 281 | 232 | 11 | |
| veriT | 0 | 968 | 352802.973 | 352854.121 | 968 | 0 | 968 | 342 | 216 | 0 | |
| Alt-Ergo | 0 | 954 | 334862.185 | 326384.172 | 954 | 0 | 954 | 356 | 244 | 24 | |
| veriT+viten | 0 | 953 | 274942.543 | 274951.691 | 953 | 0 | 953 | 357 | 212 | 8 | |
| SMTInterpol-fixedn | 0 | 801 | 520164.434 | 518127.059 | 801 | 52 | 749 | 509 | 419 | 0 | |
| SMTInterpol | 0 | 801 | 520208.63 | 518159.744 | 801 | 52 | 749 | 509 | 419 | 0 | |
| UltimateEliminator+MathSAT | 0 | 15 | 74114.268 | 72067.305 | 15 | 6 | 9 | 1295 | 57 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Vampire | 0 | 1099 | 272122.177 | 256380.902 | 1099 | 81 | 1018 | 211 | 211 | 0 | |
| 2018-CVC4n | 0 | 1098 | 262178.991 | 262501.923 | 1098 | 111 | 987 | 212 | 199 | 0 | |
| CVC4 | 0 | 1092 | 261524.776 | 261773.1 | 1092 | 107 | 985 | 218 | 201 | 0 | |
| z3n | 0 | 1029 | 322128.537 | 323115.25 | 1029 | 121 | 908 | 281 | 232 | 11 | |
| veriT | 0 | 968 | 352834.183 | 352845.591 | 968 | 0 | 968 | 342 | 216 | 0 | |
| Alt-Ergo | 0 | 965 | 356181.245 | 319964.846 | 965 | 0 | 965 | 345 | 233 | 24 | |
| veriT+viten | 0 | 953 | 274964.003 | 274942.911 | 953 | 0 | 953 | 357 | 212 | 8 | |
| SMTInterpol-fixedn | 0 | 802 | 520618.064 | 516957.601 | 802 | 52 | 750 | 508 | 416 | 0 | |
| SMTInterpol | 0 | 801 | 520629.81 | 517656.62 | 801 | 52 | 749 | 509 | 418 | 0 | |
| UltimateEliminator+MathSAT | 0 | 15 | 74114.268 | 72067.305 | 15 | 6 | 9 | 1295 | 57 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 121 | 11679.088 | 11680.736 | 121 | 121 | 0 | 1189 | 232 | 11 |
| 2018-CVC4n | 0 | 111 | 27060.282 | 27142.716 | 111 | 111 | 0 | 1199 | 199 | 0 |
| CVC4 | 0 | 107 | 24353.515 | 24404.515 | 107 | 107 | 0 | 1203 | 201 | 0 |
| Vampire | 0 | 81 | 62411.936 | 62408.454 | 81 | 81 | 0 | 1229 | 211 | 0 |
| SMTInterpol | 0 | 52 | 23287.777 | 23103.422 | 52 | 52 | 0 | 1258 | 418 | 0 |
| SMTInterpol-fixedn | 0 | 52 | 23296.832 | 23105.78 | 52 | 52 | 0 | 1258 | 416 | 0 |
| UltimateEliminator+MathSAT | 0 | 6 | 472.515 | 321.543 | 6 | 6 | 0 | 1304 | 57 | 0 |
| veriT+viten | 0 | 0 | 39693.356 | 39685.532 | 0 | 0 | 0 | 1310 | 212 | 8 |
| Alt-Ergo | 0 | 0 | 68822.387 | 64670.443 | 0 | 0 | 0 | 1310 | 233 | 24 |
| veriT | 0 | 0 | 92291.747 | 92298.621 | 0 | 0 | 0 | 1310 | 216 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Vampire | 0 | 1018 | 27309.861 | 18777.919 | 1018 | 0 | 1018 | 292 | 211 | 0 |
| 2018-CVC4n | 0 | 987 | 60666.751 | 60907.184 | 987 | 0 | 987 | 323 | 199 | 0 |
| CVC4 | 0 | 985 | 62717.858 | 62915.001 | 985 | 0 | 985 | 325 | 201 | 0 |
| veriT | 0 | 968 | 99615.147 | 99617.64 | 968 | 0 | 968 | 342 | 216 | 0 |
| Alt-Ergo | 0 | 965 | 120363.46 | 88657.735 | 965 | 0 | 965 | 345 | 233 | 24 |
| veriT+viten | 0 | 953 | 90660.668 | 90647.775 | 953 | 0 | 953 | 357 | 212 | 8 |
| z3n | 0 | 908 | 141316.784 | 142297.346 | 908 | 0 | 908 | 402 | 232 | 11 |
| SMTInterpol-fixedn | 0 | 750 | 342630.863 | 339238.78 | 750 | 0 | 750 | 560 | 416 | 0 |
| SMTInterpol | 0 | 749 | 342663.581 | 339949.118 | 749 | 0 | 749 | 561 | 418 | 0 |
| UltimateEliminator+MathSAT | 0 | 9 | 41683.783 | 40079.132 | 9 | 0 | 9 | 1301 | 57 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Vampire | 0 | 1080 | 6853.416 | 5946.875 | 1080 | 81 | 999 | 230 | 230 | 0 | |
| z3n | 0 | 1011 | 7470.127 | 7470.217 | 1011 | 120 | 891 | 299 | 288 | 11 | |
| 2018-CVC4n | 0 | 977 | 8124.811 | 8124.549 | 977 | 66 | 911 | 333 | 331 | 0 | |
| CVC4 | 0 | 975 | 8002.191 | 8003.17 | 975 | 66 | 909 | 335 | 326 | 0 | |
| veriT+viten | 0 | 946 | 7591.149 | 7569.818 | 946 | 0 | 946 | 364 | 238 | 8 | |
| Alt-Ergo | 0 | 931 | 9664.048 | 7844.258 | 931 | 0 | 931 | 379 | 274 | 24 | |
| veriT | 0 | 880 | 10452.077 | 10451.958 | 880 | 0 | 880 | 430 | 430 | 0 | |
| SMTInterpol | 0 | 762 | 13216.868 | 12121.281 | 762 | 52 | 710 | 548 | 465 | 0 | |
| SMTInterpol-fixedn | 0 | 762 | 13219.219 | 12131.684 | 762 | 52 | 710 | 548 | 465 | 0 | |
| UltimateEliminator+MathSAT | 0 | 15 | 6133.584 | 4617.253 | 15 | 6 | 9 | 1295 | 61 | 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.