Z3-Owl Submission 2025

[Zahrinas]

No description provided.

[github-actions]

Summary of modified submissions

Z3-Owl

• 2 authors
• website: https://rainoftime.github.io/html/owl.html
• Participations
  • SingleQuery
    • QF_Bitvec
      • all
    • QF_Equality+Bitvec
      • QF_UFBVDT
    • QF_FPArith
      • QF_BVFP
      • QF_FP

Z3-4.15.2.0

• 1 authors
• website: https://github.com/Z3Prover/z3
• Participations
  • SingleQuery
    • QF_Bitvec
      • all
    • QF_Equality+Bitvec
      • QF_UFBVDT
    • QF_FPArith
      • QF_BVFP
      • QF_FP

[wintered]

@Zahrinas Thank you for submitting your derived tool! Please also submit the corresponding base solver to comply with the rules. Thanks!

[martinjonas]

@Zahrinas Thanks for submitting Z3-Owl to this year's SMT-COMP!

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

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

We have not seen any incorrect results returned by your solver (compared to the expected status of the benchmarks). There are some benchmarks where the output of your tool is not valid according to the rules (and SMT-LIB specification). For example, it outputs

calling pysat
unsat

when it should reply only unsat. These results are categorized as unknown.

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

Some notes:

• We have used less resources 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

[martinjonas]

@Zahrinas Thanks for submitting the solver. As Dominik already wrote here earlier, according to the rules, for each derived solver also the corresponding base solver must be submitted (non-competitively). Look here for an example. Please, also create a submission for the base solver of Z3-Owl as soon as possible. In case you do not submit the base solver by the end of Thursday July 03 AoE, we will have to disqualify Z3-Owl from the competition.

[Zahrinas]

@martinjonas Thanks for your reply. I have added the base solver submission and fixed the output issue mentioned. Please comment further if still there are problems.

[martinjonas]

Perfect, thanks a lot for the quick fix!