z3-parallel submission

[ilanashapiro]

This PR adds z3-parallel as a competing solver in SMT-COMP 2026 Parallel Track. We have implemented a new parallel algorithm within Z3 over the past year that this submission uses

[Tomaqa]

OK!

[martinjonas]

@ilanashapiro Thanks for submitting z3-parallel to this year's SMT-COMP, it is great to see the real Z3 competing in SMT-COMP again! One important information: we decided to extend the deadline for solvers competing in Parallel track to Sunday, June 21 (AoE). Feel free to update your solver until then.

There are two minor issues your submission:

• The command "command": ["smtcomp2026/bin/z3", "smt.threads=125"] should probably be "command": ["z3_smtcomp2026/smtcomp2026/bin/z3", "smt.threads=125"]
• Please rename z3-parallel to z3-parallel.json. This way the submission will be recognized by the CI and it will trigger an automatic check.

I fixed the issues locally and executed your solver on a small number of benchmarks from each competitive logic it competes in. You can find the results here:

• https://www.fi.muni.cz/~xjonas/smtcomp/tables/z3parallel_parallel.table.html#/table

We have not seen any incorrect results returned by your solver (compared to the expected status of the benchmarks) and everything seems to be looking fine.

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

[github-actions]

Summary of modified submissions

z3-parallel

• 2 authors
• website: https://z3prover.github.io/
• Participations
  • Parallel
    • QF_Equality
      • all
    • QF_Equality+LinearArith
      • QF_UFDTLIA
      • QF_UFDTLIRA
    • QF_LinearIntArith
      • QF_LIRA
    • QF_LinearRealArith
      • all
    • QF_NonLinearIntArith
      • QF_NIA
    • QF_NonLinearRealArith
      • all

[ilanashapiro]

note: I need to redo the Zenodo record, sorry for the delay!

[ilanashapiro]

Hi @martinjonas , thank you so much for your comments! I believe I have addressed the two issues you mentioned. Please let me know if there is anything else I should do!
Best,
Ilana

[martinjonas]

Thanks a lot for the quick update. Everything looks good now. I will run another test run and let you know if there are any issues.