The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the AUFLIA logic in the Single Query Track.
Page generated on 2021-07-18 17:29:05 +0000
Benchmarks: 1638 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Vampire | Vampire | cvc5 | Vampire | Vampire |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2020-CVC4n | 0 | 1354 | 323098.765 | 331543.471 | 1354 | 137 | 1217 | 284 | 255 | 0 |
| Vampire | 0 | 1353 | 352366.428 | 344905.492 | 1353 | 100 | 1253 | 285 | 285 | 0 |
| Vampire - fixedn | 0 | 1341 | 347553.311 | 342652.154 | 1341 | 98 | 1243 | 297 | 283 | 0 |
| 2020-Vampiren | 0 | 1333 | 349111.74 | 341383.973 | 1333 | 100 | 1233 | 305 | 282 | 0 |
| cvc5 | 0 | 1332 | 188647.483 | 353990.804 | 1332 | 127 | 1205 | 306 | 281 | 0 |
| cvc5 - fixedn | 0 | 1327 | 179959.968 | 357364.644 | 1327 | 129 | 1198 | 311 | 285 | 0 |
| z3n | 0 | 1298 | 378668.041 | 379115.955 | 1298 | 176 | 1122 | 340 | 282 | 3 |
| 2020-z3n | 0 | 1294 | 385487.123 | 387008.63 | 1294 | 174 | 1120 | 344 | 277 | 11 |
| 2018-CVC4n | 0 | 1221 | 330661.564 | 338212.771 | 1221 | 98 | 1123 | 417 | 256 | 0 |
| veriT | 0 | 1212 | 312278.164 | 312325.992 | 1212 | 0 | 1212 | 426 | 254 | 0 |
| SMTInterpol | 0 | 1115 | 524887.234 | 520707.106 | 1115 | 91 | 1024 | 523 | 409 | 0 |
| UltimateEliminator+MathSAT | 0 | 47 | 58093.298 | 49172.281 | 47 | 14 | 33 | 1591 | 24 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Vampire | 0 | 1360 | 374996.308 | 340735.704 | 1360 | 100 | 1260 | 278 | 278 | 0 |
| 2020-CVC4n | 0 | 1354 | 330880.675 | 331530.871 | 1354 | 137 | 1217 | 284 | 255 | 0 |
| Vampire - fixedn | 0 | 1347 | 362566.601 | 338580.406 | 1347 | 98 | 1249 | 291 | 276 | 0 |
| 2020-Vampiren | 0 | 1336 | 360759.34 | 339842.731 | 1336 | 100 | 1236 | 302 | 278 | 0 |
| cvc5 | 0 | 1332 | 353609.935 | 353975.684 | 1332 | 127 | 1205 | 306 | 281 | 0 |
| cvc5 - fixedn | 0 | 1327 | 356956.087 | 357348.964 | 1327 | 129 | 1198 | 311 | 285 | 0 |
| z3n | 0 | 1298 | 378747.441 | 379104.075 | 1298 | 176 | 1122 | 340 | 282 | 3 |
| 2020-z3n | 0 | 1294 | 386406.903 | 386996.07 | 1294 | 174 | 1120 | 344 | 277 | 11 |
| 2018-CVC4n | 0 | 1221 | 337733.004 | 338202.201 | 1221 | 98 | 1123 | 417 | 256 | 0 |
| veriT | 0 | 1212 | 312318.044 | 312314.692 | 1212 | 0 | 1212 | 426 | 254 | 0 |
| SMTInterpol | 0 | 1115 | 541595.304 | 508228.067 | 1115 | 91 | 1024 | 523 | 387 | 0 |
| UltimateEliminator+MathSAT | 0 | 47 | 58093.298 | 49172.281 | 47 | 14 | 33 | 1591 | 24 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 176 | 6825.128 | 6825.64 | 176 | 176 | 0 | 6 | 1456 | 282 | 3 |
| 2020-z3n | 0 | 174 | 7373.024 | 7373.867 | 174 | 174 | 0 | 8 | 1456 | 277 | 11 |
| 2020-CVC4n | 0 | 137 | 29136.939 | 29273.584 | 137 | 137 | 0 | 45 | 1456 | 255 | 0 |
| cvc5 - fixedn | 0 | 129 | 41033.505 | 41176.271 | 129 | 129 | 0 | 53 | 1456 | 285 | 0 |
| cvc5 | 0 | 127 | 43824.136 | 43904.588 | 127 | 127 | 0 | 55 | 1456 | 281 | 0 |
| 2020-Vampiren | 0 | 100 | 102018.052 | 98406.471 | 100 | 100 | 0 | 82 | 1456 | 278 | 0 |
| Vampire | 0 | 100 | 105617.149 | 98407.645 | 100 | 100 | 0 | 82 | 1456 | 278 | 0 |
| 2018-CVC4n | 0 | 98 | 34620.153 | 34732.116 | 98 | 98 | 0 | 84 | 1456 | 256 | 0 |
| Vampire - fixedn | 0 | 98 | 98415.528 | 98410.712 | 98 | 98 | 0 | 84 | 1456 | 276 | 0 |
| SMTInterpol | 0 | 91 | 22104.504 | 21914.974 | 91 | 91 | 0 | 91 | 1456 | 387 | 0 |
| UltimateEliminator+MathSAT | 0 | 14 | 2020.868 | 1336.997 | 14 | 14 | 0 | 168 | 1456 | 24 | 0 |
| veriT | 0 | 0 | 46446.431 | 46446.204 | 0 | 0 | 0 | 182 | 1456 | 254 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Vampire | 0 | 1260 | 52178.439 | 32348.189 | 1260 | 0 | 1260 | 21 | 357 | 278 | 0 |
| Vampire - fixedn | 0 | 1249 | 50550.873 | 30177.354 | 1249 | 0 | 1249 | 32 | 357 | 276 | 0 |
| 2020-Vampiren | 0 | 1236 | 48741.288 | 31436.26 | 1236 | 0 | 1236 | 45 | 357 | 278 | 0 |
| 2020-CVC4n | 0 | 1217 | 91743.736 | 92257.287 | 1217 | 0 | 1217 | 64 | 357 | 255 | 0 |
| veriT | 0 | 1212 | 87540.976 | 87537.73 | 1212 | 0 | 1212 | 69 | 357 | 254 | 0 |
| cvc5 | 0 | 1205 | 99785.799 | 100071.096 | 1205 | 0 | 1205 | 76 | 357 | 281 | 0 |
| cvc5 - fixedn | 0 | 1198 | 105922.582 | 106172.693 | 1198 | 0 | 1198 | 83 | 357 | 285 | 0 |
| 2018-CVC4n | 0 | 1123 | 93741.926 | 94098.642 | 1123 | 0 | 1123 | 158 | 357 | 256 | 0 |
| z3n | 0 | 1122 | 175110.897 | 175464.882 | 1122 | 0 | 1122 | 159 | 357 | 282 | 3 |
| 2020-z3n | 0 | 1120 | 178549.042 | 178888.757 | 1120 | 0 | 1120 | 161 | 357 | 277 | 11 |
| SMTInterpol | 0 | 1024 | 338848.6 | 312088.125 | 1024 | 0 | 1024 | 257 | 357 | 387 | 0 |
| UltimateEliminator+MathSAT | 0 | 33 | 41746.151 | 35780.684 | 33 | 0 | 33 | 1248 | 357 | 24 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Vampire | 0 | 1332 | 9167.048 | 7947.383 | 1332 | 100 | 1232 | 306 | 306 | 0 |
| Vampire - fixedn | 0 | 1321 | 9104.081 | 7891.704 | 1321 | 98 | 1223 | 317 | 304 | 0 |
| 2020-Vampiren | 0 | 1309 | 8901.921 | 7860.267 | 1309 | 100 | 1209 | 329 | 306 | 0 |
| z3n | 0 | 1269 | 9218.407 | 9218.658 | 1269 | 175 | 1094 | 369 | 366 | 3 |
| 2020-z3n | 0 | 1264 | 9339.269 | 9339.479 | 1264 | 174 | 1090 | 374 | 362 | 11 |
| cvc5 | 0 | 1220 | 9823.091 | 9825.086 | 1220 | 100 | 1120 | 418 | 399 | 0 |
| cvc5 - fixedn | 0 | 1220 | 9833.684 | 9826.439 | 1220 | 100 | 1120 | 418 | 399 | 0 |
| 2018-CVC4n | 0 | 1219 | 10202.843 | 10198.246 | 1219 | 97 | 1122 | 419 | 411 | 0 |
| 2020-CVC4n | 0 | 1215 | 9933.797 | 9935.429 | 1215 | 99 | 1116 | 423 | 404 | 0 |
| veriT | 0 | 1198 | 7561.403 | 7557.218 | 1198 | 0 | 1198 | 440 | 279 | 0 |
| SMTInterpol | 0 | 1038 | 15378.825 | 13550.304 | 1038 | 91 | 947 | 600 | 498 | 0 |
| UltimateEliminator+MathSAT | 0 | 47 | 12640.806 | 7743.004 | 47 | 14 | 33 | 1591 | 85 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.