The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_UFIDL logic in the Unsat Core Track.
Page generated on 2022-08-10 11:18:51 +0000
Benchmarks: 113 Time Limit: 1200 seconds Memory Limit: 60 GB
Sequential Performance | Parallel Performance |
---|---|
Yices2 | Yices2 |
Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Timeout | Memout |
---|---|---|---|---|---|---|
Yices2 | 0 | 802882 | 72820.592 | 72831.464 | 38 | 0 |
MathSATn | 0 | 797716 | 60435.643 | 60456.666 | 35 | 0 |
2021-MathSAT5n | 0 | 778665 | 62043.973 | 62454.552 | 37 | 0 |
z3-4.8.17n | 0 | 445009 | 63224.466 | 63235.937 | 29 | 0 |
smtinterpol | 0 | 185088 | 112516.056 | 108352.193 | 84 | 0 |
cvc5 | 0 | 29766 | 116283.871 | 116304.559 | 94 | 0 |
Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Timeout | Memout |
---|---|---|---|---|---|---|
Yices2 | 0 | 802882 | 72825.892 | 72829.864 | 38 | 0 |
MathSATn | 0 | 797716 | 60449.063 | 60455.076 | 35 | 0 |
2021-MathSAT5n | 0 | 778665 | 62312.443 | 62452.572 | 37 | 0 |
z3-4.8.17n | 0 | 445009 | 63229.336 | 63234.767 | 29 | 0 |
smtinterpol | 0 | 210908 | 113157.206 | 107652.087 | 82 | 0 |
cvc5 | 0 | 29766 | 116300.171 | 116300.589 | 94 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.