The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the UFDT logic in the Single Query Track.
Page generated on 2021-07-18 17:29:07 +0000
Benchmarks: 1552 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| cvc5 | cvc5 | cvc5 | cvc5 | cvc5 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2020-CVC4n | 0 | 531 | 1292956.003 | 1306804.95 | 531 | 132 | 399 | 1021 | 1021 | 0 |
| cvc5 | 0 | 449 | 667497.647 | 1367384.535 | 449 | 72 | 377 | 1103 | 1103 | 0 |
| 2020-Vampiren | 0 | 351 | 1464937.16 | 1442165.199 | 351 | 0 | 351 | 1201 | 1195 | 0 |
| Vampire | 0 | 350 | 1471901.193 | 1449816.068 | 350 | 0 | 350 | 1202 | 1201 | 0 |
| Vampire - fixedn | 0 | 346 | 1471429.523 | 1447972.46 | 346 | 0 | 346 | 1206 | 1199 | 0 |
| iProver - fixed2n | 0 | 268 | 1566743.987 | 1542072.156 | 268 | 0 | 268 | 1284 | 1195 | 83 |
| iProver - fixedn | 0 | 263 | 1569473.41 | 1547240.177 | 263 | 0 | 263 | 1289 | 1180 | 103 |
| iProver | 0 | 259 | 1571495.854 | 1550600.303 | 259 | 0 | 259 | 1293 | 1195 | 91 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2020-CVC4n | 0 | 531 | 1304237.963 | 1306758.11 | 531 | 132 | 399 | 1021 | 1021 | 0 |
| cvc5 | 0 | 449 | 1366163.715 | 1367329.085 | 449 | 72 | 377 | 1103 | 1103 | 0 |
| 2020-Vampiren | 0 | 389 | 1544406.0 | 1425966.763 | 389 | 20 | 369 | 1163 | 1153 | 0 |
| Vampire | 0 | 378 | 1521090.153 | 1434289.007 | 378 | 1 | 377 | 1174 | 1173 | 0 |
| Vampire - fixedn | 0 | 375 | 1514940.013 | 1431091.467 | 375 | 2 | 373 | 1177 | 1168 | 0 |
| iProver - fixed2n | 0 | 282 | 1590552.937 | 1534913.039 | 282 | 0 | 282 | 1270 | 1180 | 83 |
| iProver - fixedn | 0 | 279 | 1594533.96 | 1539221.739 | 279 | 0 | 279 | 1273 | 1164 | 103 |
| iProver | 0 | 277 | 1596045.534 | 1540077.02 | 277 | 0 | 277 | 1275 | 1176 | 91 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2020-CVC4n | 0 | 132 | 62384.733 | 64695.268 | 132 | 132 | 0 | 2 | 1418 | 1021 | 0 |
| cvc5 | 0 | 72 | 106581.715 | 107622.998 | 72 | 72 | 0 | 62 | 1418 | 1103 | 0 |
| 2020-Vampiren | 0 | 20 | 218534.53 | 156827.742 | 20 | 20 | 0 | 114 | 1418 | 1153 | 0 |
| Vampire - fixedn | 0 | 2 | 166612.86 | 160558.017 | 2 | 2 | 0 | 132 | 1418 | 1168 | 0 |
| Vampire | 0 | 1 | 167282.27 | 160659.25 | 1 | 1 | 0 | 133 | 1418 | 1173 | 0 |
| iProver - fixedn | 0 | 0 | 153618.758 | 153607.267 | 0 | 0 | 0 | 134 | 1418 | 1164 | 103 |
| iProver | 0 | 0 | 153620.886 | 153607.754 | 0 | 0 | 0 | 134 | 1418 | 1176 | 91 |
| iProver - fixed2n | 0 | 0 | 153620.777 | 153607.756 | 0 | 0 | 0 | 134 | 1418 | 1180 | 83 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2020-CVC4n | 0 | 399 | 80253.23 | 80462.842 | 399 | 0 | 399 | 51 | 1102 | 1021 | 0 |
| cvc5 | 0 | 377 | 97982.0 | 98106.087 | 377 | 0 | 377 | 73 | 1102 | 1103 | 0 |
| Vampire | 0 | 377 | 185001.523 | 112031.837 | 377 | 0 | 377 | 73 | 1102 | 1173 | 0 |
| Vampire - fixedn | 0 | 373 | 186727.153 | 108933.45 | 373 | 0 | 373 | 77 | 1102 | 1168 | 0 |
| 2020-Vampiren | 0 | 369 | 164271.47 | 107539.021 | 369 | 0 | 369 | 81 | 1102 | 1153 | 0 |
| iProver - fixed2n | 0 | 282 | 275300.38 | 220323.745 | 282 | 0 | 282 | 168 | 1102 | 1180 | 83 |
| iProver - fixedn | 0 | 279 | 279315.202 | 224014.472 | 279 | 0 | 279 | 171 | 1102 | 1164 | 103 |
| iProver | 0 | 277 | 280825.008 | 226192.82 | 277 | 0 | 277 | 173 | 1102 | 1176 | 91 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2020-CVC4n | 0 | 321 | 29873.142 | 29871.066 | 321 | 4 | 317 | 1231 | 1231 | 0 |
| cvc5 | 0 | 318 | 29905.617 | 29905.614 | 318 | 4 | 314 | 1234 | 1234 | 0 |
| 2020-Vampiren | 0 | 280 | 33832.861 | 31304.922 | 280 | 0 | 280 | 1272 | 1267 | 0 |
| Vampire | 0 | 278 | 34256.639 | 31540.318 | 278 | 0 | 278 | 1274 | 1274 | 0 |
| Vampire - fixedn | 0 | 274 | 34236.547 | 31534.941 | 274 | 0 | 274 | 1278 | 1274 | 0 |
| iProver - fixed2n | 0 | 203 | 36583.755 | 33403.865 | 203 | 0 | 203 | 1349 | 1260 | 83 |
| iProver | 0 | 200 | 36462.113 | 33423.097 | 200 | 0 | 200 | 1352 | 1255 | 91 |
| iProver - fixedn | 0 | 198 | 36381.667 | 33438.875 | 198 | 0 | 198 | 1354 | 1245 | 103 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.