Summary of all competition results for the Single Query Track.
Results are given ranked by performance for each scoring scheme (best solver
is given as left-most solver).
| Scoring Scheme | Winner | Ranking | | Sequential Performance | Z3-alpha2 | Z3-alpha2, Z3-alpha2-debug, z3-BooledASS, Z3-GEX, YicesQS, cvc5-cvc5-xyz, cvc5, UltimateEliminator+MathSAT, Amaya, SMTInterpol, SMT-RAT |
| Parallel Performance | Z3-alpha2 | Z3-alpha2, Z3-alpha2-debug, Z3-GEX, z3-BooledASS, YicesQS, cvc5-cvc5-xyz, cvc5, UltimateEliminator+MathSAT, Amaya, SMTInterpol, SMT-RAT |
| SAT Performance | Z3-alpha2 | Z3-alpha2, Z3-alpha2-debug, YicesQS, Z3-GEX, z3-BooledASS, cvc5-cvc5-xyz, cvc5, UltimateEliminator+MathSAT, Amaya, SMTInterpol, SMT-RAT |
| UNSAT Performance | Z3-GEX | Z3-GEX, Z3-alpha2, Z3-alpha2-debug, z3-BooledASS, cvc5-cvc5-xyz, cvc5, YicesQS, UltimateEliminator+MathSAT, Amaya, SMTInterpol, SMT-RAT |
| 24 seconds Performance | Z3-GEX | Z3-GEX, Z3-alpha2, Z3-alpha2-debug, z3-BooledASS, YicesQS, cvc5-cvc5-xyz, cvc5, UltimateEliminator+MathSAT, Amaya, SMTInterpol, SMT-RAT |
| Scoring Scheme | Winner | Ranking | | Sequential Performance | Bitwuzla | Bitwuzla-fixed, Bitwuzla, cvc5, cvc5-cvc5-xyz, YicesQS, bitwuzla-dandelion, z3-BooledASS, UltimateEliminator+MathSAT, SMTInterpol |
| Parallel Performance | Bitwuzla | Bitwuzla-fixed, Bitwuzla, cvc5, cvc5-cvc5-xyz, YicesQS, bitwuzla-dandelion, z3-BooledASS, UltimateEliminator+MathSAT, SMTInterpol |
| SAT Performance | Bitwuzla | Bitwuzla, Bitwuzla-fixed, YicesQS, bitwuzla-dandelion, cvc5, cvc5-cvc5-xyz, z3-BooledASS, UltimateEliminator+MathSAT, SMTInterpol |
| UNSAT Performance | cvc5 | cvc5, cvc5-cvc5-xyz, Bitwuzla-fixed, Bitwuzla, YicesQS, bitwuzla-dandelion, z3-BooledASS, UltimateEliminator+MathSAT, SMTInterpol |
| 24 seconds Performance | Bitwuzla | Bitwuzla-fixed, Bitwuzla, YicesQS, bitwuzla-dandelion, z3-BooledASS, cvc5, cvc5-cvc5-xyz, UltimateEliminator+MathSAT, SMTInterpol |
| Scoring Scheme | Winner | Ranking | | Sequential Performance | cvc5 | cvc5-cvc5-xyz, cvc5, z3-BooledASS, Yices2, SMTInterpol, UltimateEliminator+MathSAT |
| Parallel Performance | cvc5 | cvc5-cvc5-xyz, cvc5, z3-BooledASS, Yices2, SMTInterpol, UltimateEliminator+MathSAT |
| SAT Performance | cvc5 | cvc5-cvc5-xyz, cvc5, z3-BooledASS, Yices2, SMTInterpol, UltimateEliminator+MathSAT |
| UNSAT Performance | cvc5 | cvc5-cvc5-xyz, cvc5, z3-BooledASS, Yices2, SMTInterpol, UltimateEliminator+MathSAT |
| 24 seconds Performance | cvc5 | cvc5-cvc5-xyz, cvc5, z3-BooledASS, Yices2, SMTInterpol, UltimateEliminator+MathSAT |
| Scoring Scheme | Winner | Ranking | | Sequential Performance | cvc5 | cvc5-cvc5-xyz, cvc5, z3-BooledASS, SMTInterpol, UltimateEliminator+MathSAT |
| Parallel Performance | cvc5 | cvc5-cvc5-xyz, cvc5, z3-BooledASS, SMTInterpol, UltimateEliminator+MathSAT |
| SAT Performance | cvc5 | z3-BooledASS, cvc5-cvc5-xyz, cvc5, SMTInterpol, UltimateEliminator+MathSAT |
| UNSAT Performance | cvc5 | cvc5-cvc5-xyz, cvc5, z3-BooledASS, SMTInterpol, UltimateEliminator+MathSAT |
| 24 seconds Performance | cvc5 | cvc5, cvc5-cvc5-xyz, z3-BooledASS, SMTInterpol, UltimateEliminator+MathSAT |
| Scoring Scheme | Winner | Ranking | | Sequential Performance | cvc5 | cvc5-cvc5-xyz, cvc5, SMTInterpol, Bitwuzla-fixed, Bitwuzla, z3-BooledASS, bitwuzla-dandelion, UltimateEliminator+MathSAT |
| Parallel Performance | cvc5 | cvc5-cvc5-xyz, cvc5, SMTInterpol, Bitwuzla-fixed, Bitwuzla, z3-BooledASS, bitwuzla-dandelion, UltimateEliminator+MathSAT |
| SAT Performance | Bitwuzla | Bitwuzla, Bitwuzla-fixed, cvc5-cvc5-xyz, cvc5, z3-BooledASS, bitwuzla-dandelion, UltimateEliminator+MathSAT, SMTInterpol |
| UNSAT Performance | cvc5 | cvc5-cvc5-xyz, cvc5, SMTInterpol, z3-BooledASS, Bitwuzla-fixed, Bitwuzla, bitwuzla-dandelion, UltimateEliminator+MathSAT |
| 24 seconds Performance | cvc5 | cvc5, cvc5-cvc5-xyz, SMTInterpol, Bitwuzla-fixed, Bitwuzla, z3-BooledASS, bitwuzla-dandelion, UltimateEliminator+MathSAT |
| Scoring Scheme | Winner | Ranking | | Sequential Performance | cvc5 | cvc5, cvc5-cvc5-xyz, z3-BooledASS, SMTInterpol, UltimateEliminator+MathSAT |
| Parallel Performance | cvc5 | cvc5, cvc5-cvc5-xyz, z3-BooledASS, SMTInterpol, UltimateEliminator+MathSAT |
| SAT Performance | cvc5 | z3-BooledASS, cvc5, cvc5-cvc5-xyz, UltimateEliminator+MathSAT, SMTInterpol |
| UNSAT Performance | cvc5 | cvc5, cvc5-cvc5-xyz, z3-BooledASS, SMTInterpol, UltimateEliminator+MathSAT |
| 24 seconds Performance | cvc5 | z3-BooledASS, cvc5, cvc5-cvc5-xyz, SMTInterpol, UltimateEliminator+MathSAT |
| Scoring Scheme | Winner | Ranking | | Sequential Performance | Bitwuzla | Bitwuzla, cvc5, cvc5-cvc5-xyz, z3-BooledASS, Bitwuzla-fixed, bitwuzla-dandelion, colibri2, UltimateEliminator+MathSAT |
| Parallel Performance | Bitwuzla | Bitwuzla, cvc5, cvc5-cvc5-xyz, z3-BooledASS, Bitwuzla-fixed, bitwuzla-dandelion, colibri2, UltimateEliminator+MathSAT |
| SAT Performance | Bitwuzla | Bitwuzla, cvc5, cvc5-cvc5-xyz, Bitwuzla-fixed, colibri2, UltimateEliminator+MathSAT, bitwuzla-dandelion, z3-BooledASS |
| UNSAT Performance | Bitwuzla | Bitwuzla, cvc5, cvc5-cvc5-xyz, z3-BooledASS, bitwuzla-dandelion, colibri2, UltimateEliminator+MathSAT, Bitwuzla-fixed |
| 24 seconds Performance | Bitwuzla | Bitwuzla, cvc5, cvc5-cvc5-xyz, Bitwuzla-fixed, z3-BooledASS, bitwuzla-dandelion, colibri2, UltimateEliminator+MathSAT |
| Scoring Scheme | Winner | Ranking | | Sequential Performance | Bitwuzla-MachBV | Bitwuzla-MachBV, Bitwuzla, bitwuzla-dandelion, Bitwuzla-SPFD, bv_decide-nokernel, bv_decide, cvc5-cvc5-xyz, cvc5, NeuroSym, Z3-GEX, Z3-alpha2, Z3-alpha2-debug, SMTInterpol, Roole, z3-BooledASS, Yices2 |
| Parallel Performance | Bitwuzla-MachBV | Bitwuzla-MachBV, Bitwuzla, bitwuzla-dandelion, Bitwuzla-SPFD, bv_decide-nokernel, bv_decide, cvc5-cvc5-xyz, cvc5, NeuroSym, Z3-GEX, Z3-alpha2, Z3-alpha2-debug, SMTInterpol, Roole, z3-BooledASS, Yices2 |
| SAT Performance | Bitwuzla-MachBV | Bitwuzla-MachBV, bitwuzla-dandelion, Bitwuzla, Bitwuzla-SPFD, cvc5-cvc5-xyz, cvc5, bv_decide-nokernel, bv_decide, NeuroSym, Z3-alpha2, Z3-alpha2-debug, Z3-GEX, Roole, SMTInterpol, z3-BooledASS, Yices2 |
| UNSAT Performance | Bitwuzla-MachBV | Bitwuzla-MachBV, Bitwuzla, Yices2, bitwuzla-dandelion, Bitwuzla-SPFD, bv_decide-nokernel, bv_decide, NeuroSym, cvc5-cvc5-xyz, cvc5, Z3-GEX, Z3-alpha2, Z3-alpha2-debug, SMTInterpol, z3-BooledASS, Roole |
| 24 seconds Performance | Bitwuzla | Bitwuzla-MachBV, Bitwuzla, NeuroSym, Bitwuzla-SPFD, cvc5, cvc5-cvc5-xyz, Z3-GEX, bitwuzla-dandelion, Z3-alpha2, Z3-alpha2-debug, bv_decide-nokernel, bv_decide, z3-BooledASS, SMTInterpol, Roole, Yices2 |
| Scoring Scheme | Winner | Ranking | | Sequential Performance | cvc5-cvc5-xyz | cvc5-cvc5-xyz, Z3-Z3++, cvc5, Z3-alpha2, Z3-alpha2-debug, z3-BooledASS, SMTInterpol |
| Parallel Performance | cvc5-cvc5-xyz | cvc5-cvc5-xyz, Z3-Z3++, cvc5, Z3-alpha2, Z3-alpha2-debug, z3-BooledASS, SMTInterpol |
| SAT Performance | cvc5 | cvc5-cvc5-xyz, cvc5, Z3-Z3++, Z3-alpha2, Z3-alpha2-debug, SMTInterpol, z3-BooledASS |
| UNSAT Performance | Z3-Z3++ | Z3-Z3++, Z3-alpha2, Z3-alpha2-debug, z3-BooledASS, cvc5-cvc5-xyz, cvc5, SMTInterpol |
| 24 seconds Performance | SMTInterpol | Z3-Z3++, cvc5-cvc5-xyz, SMTInterpol, Z3-alpha2, Z3-alpha2-debug, z3-BooledASS, cvc5 |
| Scoring Scheme | Winner | Ranking | | Sequential Performance | Yices2 | Yices2, cvc5-cvc5-xyz, OpenSMT, cvc5, z3-BooledASS, OpenSMT-SMTS-seq, SMTInterpol, plat-smt |
| Parallel Performance | Yices2 | Yices2, cvc5-cvc5-xyz, OpenSMT, cvc5, z3-BooledASS, OpenSMT-SMTS-seq, SMTInterpol, plat-smt |
| SAT Performance | Yices2 | Yices2, z3-BooledASS, OpenSMT, cvc5-cvc5-xyz, cvc5, OpenSMT-SMTS-seq, SMTInterpol, plat-smt |
| UNSAT Performance | Yices2 | Yices2, cvc5-cvc5-xyz, OpenSMT, cvc5, z3-BooledASS, OpenSMT-SMTS-seq, SMTInterpol, plat-smt |
| 24 seconds Performance | Yices2 | Yices2, z3-BooledASS, OpenSMT, cvc5-cvc5-xyz, OpenSMT-SMTS-seq, cvc5, SMTInterpol, plat-smt |
| Scoring Scheme | Winner | Ranking | | Sequential Performance | Bitwuzla | bitwuzla-dandelion, Bitwuzla, Yices2, cvc5-cvc5-xyz, cvc5, NeuroSym, SMTInterpol, z3-BooledASS |
| Parallel Performance | Bitwuzla | bitwuzla-dandelion, Bitwuzla, Yices2, cvc5-cvc5-xyz, cvc5, NeuroSym, SMTInterpol, z3-BooledASS |
| SAT Performance | Bitwuzla | Bitwuzla, bitwuzla-dandelion, Yices2, cvc5-cvc5-xyz, cvc5, NeuroSym, SMTInterpol, z3-BooledASS |
| UNSAT Performance | Bitwuzla | bitwuzla-dandelion, Bitwuzla, Yices2, cvc5, cvc5-cvc5-xyz, SMTInterpol, z3-BooledASS, NeuroSym |
| 24 seconds Performance | Bitwuzla | Bitwuzla, bitwuzla-dandelion, Yices2, cvc5, cvc5-cvc5-xyz, NeuroSym, z3-BooledASS, SMTInterpol |
| Scoring Scheme | Winner | Ranking | | Sequential Performance | SMTInterpol | z3-BooledASS, SMTInterpol, cvc5, OpenSMT, Yices2, cvc5-cvc5-xyz, OpenSMT-SMTS-seq |
| Parallel Performance | SMTInterpol | z3-BooledASS, SMTInterpol, cvc5, OpenSMT, Yices2, cvc5-cvc5-xyz, OpenSMT-SMTS-seq |
| SAT Performance | SMTInterpol | SMTInterpol, z3-BooledASS, cvc5, cvc5-cvc5-xyz, OpenSMT-SMTS-seq, OpenSMT, Yices2 |
| UNSAT Performance | OpenSMT | z3-BooledASS, OpenSMT, Yices2, cvc5, SMTInterpol, cvc5-cvc5-xyz, OpenSMT-SMTS-seq |
| 24 seconds Performance | SMTInterpol | z3-BooledASS, SMTInterpol, Yices2, cvc5, OpenSMT, cvc5-cvc5-xyz, OpenSMT-SMTS-seq |
| Scoring Scheme | Winner | Ranking | | Sequential Performance | Yices2 | Z3-alpha2, Z3-alpha2-debug, Yices2, z3-BooledASS, cvc5-cvc5-xyz, cvc5, SMTInterpol, Xolver |
| Parallel Performance | Yices2 | Z3-alpha2, Z3-alpha2-debug, Yices2, z3-BooledASS, cvc5-cvc5-xyz, cvc5, SMTInterpol, Xolver |
| SAT Performance | Yices2 | Yices2, Z3-alpha2, Z3-alpha2-debug, z3-BooledASS, cvc5-cvc5-xyz, cvc5, SMTInterpol, Xolver |
| UNSAT Performance | Z3-alpha2 | Z3-alpha2, Z3-alpha2-debug, z3-BooledASS, cvc5-cvc5-xyz, cvc5, Yices2, SMTInterpol, Xolver |
| 24 seconds Performance | Yices2 | Z3-alpha2, Z3-alpha2-debug, z3-BooledASS, Yices2, cvc5, cvc5-cvc5-xyz, SMTInterpol, Xolver |
| Scoring Scheme | Winner | Ranking | | Sequential Performance | Bitwuzla | Bitwuzla, cvc5, cvc5-cvc5-xyz, colibri2, bitwuzla-dandelion, z3-BooledASS, COLIBRI |
| Parallel Performance | Bitwuzla | Bitwuzla, cvc5, cvc5-cvc5-xyz, colibri2, bitwuzla-dandelion, z3-BooledASS, COLIBRI |
| SAT Performance | Bitwuzla | Bitwuzla, cvc5-cvc5-xyz, cvc5, colibri2, bitwuzla-dandelion, z3-BooledASS, COLIBRI |
| UNSAT Performance | Bitwuzla | Bitwuzla, cvc5, cvc5-cvc5-xyz, COLIBRI, colibri2, bitwuzla-dandelion, z3-BooledASS |
| 24 seconds Performance | Bitwuzla | Bitwuzla, cvc5-cvc5-xyz, cvc5, colibri2, bitwuzla-dandelion, z3-BooledASS, COLIBRI |
| Scoring Scheme | Winner | Ranking | | Sequential Performance | QiuQi | QiuQi, OpenSMT-SMTS-seq, OpenSMT, Yices2, cvc5, Z3-alpha2, Z3-alpha2-debug, Z3-GEX, cvc5-cvc5-xyz, z3-BooledASS, SMTInterpol, NeuroSym |
| Parallel Performance | QiuQi | QiuQi, OpenSMT-SMTS-seq, OpenSMT, Yices2, cvc5, Z3-GEX, Z3-alpha2, Z3-alpha2-debug, cvc5-cvc5-xyz, z3-BooledASS, SMTInterpol, NeuroSym |
| SAT Performance | QiuQi | QiuQi, Z3-GEX, OpenSMT-SMTS-seq, OpenSMT, Z3-alpha2, Z3-alpha2-debug, Yices2, cvc5, cvc5-cvc5-xyz, z3-BooledASS, SMTInterpol, NeuroSym |
| UNSAT Performance | QiuQi | QiuQi, cvc5, Yices2, OpenSMT, OpenSMT-SMTS-seq, Z3-alpha2, Z3-alpha2-debug, Z3-GEX, cvc5-cvc5-xyz, SMTInterpol, z3-BooledASS, NeuroSym |
| 24 seconds Performance | Yices2 | Yices2, Z3-GEX, QiuQi, Z3-alpha2, Z3-alpha2-debug, z3-BooledASS, OpenSMT, OpenSMT-SMTS-seq, cvc5, cvc5-cvc5-xyz, SMTInterpol, NeuroSym |
| Scoring Scheme | Winner | Ranking | | Sequential Performance | Yices2 | Yices2, OpenSMT, OpenSMT-SMTS-seq, cvc5, z3-BooledASS, cvc5-cvc5-xyz, Z3-GEX, SMTInterpol, Samet |
| Parallel Performance | Yices2 | Yices2, OpenSMT, OpenSMT-SMTS-seq, cvc5, Z3-GEX, z3-BooledASS, cvc5-cvc5-xyz, SMTInterpol, Samet |
| SAT Performance | OpenSMT | OpenSMT, OpenSMT-SMTS-seq, Yices2, Z3-GEX, cvc5, z3-BooledASS, cvc5-cvc5-xyz, SMTInterpol, Samet |
| UNSAT Performance | Yices2 | Yices2, cvc5, OpenSMT, z3-BooledASS, Z3-GEX, OpenSMT-SMTS-seq, cvc5-cvc5-xyz, SMTInterpol, Samet |
| 24 seconds Performance | Yices2 | Yices2, OpenSMT-SMTS-seq, OpenSMT, cvc5, Z3-GEX, z3-BooledASS, cvc5-cvc5-xyz, SMTInterpol, Samet |
| Scoring Scheme | Winner | Ranking | | Sequential Performance | Z3-alpha2 | Z3-alpha2, Z3-Z3++, Z3-alpha2-debug, Z3-GEX, Yices2, cvc5, cvc5-cvc5-xyz, Z3-siri, z3-BooledASS, Xolver, SMTInterpol |
| Parallel Performance | Z3-alpha2 | Z3-alpha2, Z3-Z3++, Z3-alpha2-debug, Z3-GEX, Yices2, cvc5, cvc5-cvc5-xyz, Z3-siri, z3-BooledASS, Xolver, SMTInterpol |
| SAT Performance | Z3-Z3++ | Z3-Z3++, Z3-alpha2, Z3-alpha2-debug, Z3-GEX, Yices2, cvc5, cvc5-cvc5-xyz, Xolver, Z3-siri, z3-BooledASS, SMTInterpol |
| UNSAT Performance | Z3-alpha2 | Z3-alpha2, Z3-alpha2-debug, Z3-GEX, Z3-Z3++, Z3-siri, Yices2, cvc5, cvc5-cvc5-xyz, z3-BooledASS, Xolver, SMTInterpol |
| 24 seconds Performance | Z3-alpha2 | Z3-GEX, Z3-alpha2, Z3-alpha2-debug, Yices2, Z3-Z3++, Z3-siri, z3-BooledASS, cvc5, cvc5-cvc5-xyz, Xolver, SMTInterpol |
| Scoring Scheme | Winner | Ranking | | Sequential Performance | Z3-alpha2 | Z3-GEX, Z3-alpha2, Z3-alpha2-debug, Z3-siri, cvc5, cvc5-cvc5-xyz, Yices2, z3-BooledASS, SMT-RAT, Xolver, SMTInterpol |
| Parallel Performance | Z3-GEX | Z3-GEX, Z3-alpha2, Z3-alpha2-debug, Z3-siri, cvc5, cvc5-cvc5-xyz, Yices2, z3-BooledASS, SMT-RAT, Xolver, SMTInterpol |
| SAT Performance | Z3-GEX | Z3-GEX, Z3-alpha2, Z3-alpha2-debug, Z3-siri, z3-BooledASS, Yices2, cvc5, cvc5-cvc5-xyz, SMT-RAT, Xolver, SMTInterpol |
| UNSAT Performance | Z3-GEX | Z3-GEX, Z3-alpha2, Z3-alpha2-debug, Z3-siri, cvc5, cvc5-cvc5-xyz, Yices2, z3-BooledASS, SMT-RAT, Xolver, SMTInterpol |
| 24 seconds Performance | Yices2 | Z3-GEX, Z3-alpha2, Yices2, Z3-alpha2-debug, cvc5, cvc5-cvc5-xyz, Z3-siri, z3-BooledASS, SMT-RAT, Xolver, SMTInterpol |
| Scoring Scheme | Winner | Ranking | | Sequential Performance | Z3-Noodler | Z3-Noodler, OSTRICH, cvc5, cvc5-cvc5-xyz, Z3-GEX, z3-BooledASS |
| Parallel Performance | Z3-Noodler | Z3-Noodler, OSTRICH, cvc5, cvc5-cvc5-xyz, Z3-GEX, z3-BooledASS |
| SAT Performance | Z3-Noodler | Z3-Noodler, OSTRICH, cvc5, cvc5-cvc5-xyz, Z3-GEX, z3-BooledASS |
| UNSAT Performance | Z3-Noodler | Z3-Noodler, OSTRICH, cvc5-cvc5-xyz, cvc5, Z3-GEX, z3-BooledASS |
| 24 seconds Performance | Z3-Noodler | Z3-Noodler, OSTRICH, Z3-GEX, cvc5, cvc5-cvc5-xyz, z3-BooledASS |