Bituzla-dandelion Submission for SMT-COMP 2026

[DarkPaper2022]

No description provided.

[github-actions]

Summary of modified submissions

bitwuzla-dandelion-base

• 2 authors
• website: https://bitwuzla.github.io/
• Participations
  • SingleQuery
    • Bitvec
      • all
    • Equality+MachineArith
      • ABV
      • ABVFP
      • ABVFPLRA
      • AUFBV
      • AUFBVFP
      • UFBV
      • UFBVFP
    • FPArith
      • all
    • QF_Bitvec
      • all
    • QF_Equality+Bitvec
      • QF_UFBVDT
    • QF_FPArith
      • QF_UFFPDTNIRA

bitwuzla-dandelion

• 2 authors
• website: https://zenodo.org/records/20422525
• Participations
  • SingleQuery
    • Bitvec
      • all
    • Equality+MachineArith
      • ABV
      • ABVFP
      • ABVFPLRA
      • AUFBV
      • AUFBVFP
      • UFBV
      • UFBVFP
    • FPArith
      • all
    • QF_Bitvec
      • all
    • QF_Equality+Bitvec
      • QF_UFBVDT
    • QF_FPArith
      • QF_UFFPDTNIRA

[martinjonas]

@DarkPaper2022 Thanks for submitting Bitwuzla-dandelion to this year's SMT-COMP!

We have executed your solver on a small number of benchmarks from each logic it should compete in (except for the parallel track). You can find the results here:

• Single Query Track: https://www.fi.muni.cz/~xjonas/smtcomp/tables/bitwuzladandelion.table.html#/table

We have not seen any incorrect results returned by your solver (compared to the expected status of the benchmarks), but there are some runs that end up with an error.

You can check whether all the results we have obtained are expected. If not, please let us know here.

Some notes:

• We have used smaller resource limits than will be used in the final runs.
• The benchmarks are scrambled by the official scrambler with seed 1.
• The column status shows whether your solver decided the benchmark as sat (true) or unsat (false).
• You can click on the value in the status column to see the output of your solver on that benchmark.

If you upload a new version of the solver and want to have another test run, let me know. We still have some time for that.

Happy rest of the competition!
Martin

[wintered]

Dear @DarkPaper2022,

after inspection of your system description, we have found that your solver does not qualify as a derived tool according to SMT-COMP 2026 rules:

A derived tool is defined as any solver that is based on and extends another SMT solver (the base solver) from a different group of authors. In contrast to a wrapper tool, a derived tool solving a benchmark of logic A is allowed to call an SMT solver to solve a problem for logic A. However, it is not allowed to call more than one SMT solver to solve a problem over the input logic.

As the system description indicates, Z3 is used as a preprocessing step to Bitwuzla. In this preprocessing step, Z3 does not necessarily change the logic of the input which would be required to comply with above rule.

Given that, Bitwuzla-dandalion can unfortunately not participate in the specified tracks. We can only run it as a non-competing solver.