Bitwuzla-BV_Parti Submission for SMT-COMP 2026

[zmylinxi99]

No description provided.

[github-actions]

Summary of modified submissions

Bitwuzla-BV_Parti

• 3 authors
• website: https://github.com/zmylinxi99/Bitwuzla-BV_Parti-at-SMT-COMP-2026
• Participations
  • Parallel
    • QF_Bitvec
      • all

[Tomaqa]

Dear authors, thank you for the submission. Please update the system description as requested.

[Tomaqa]

The description cannot be found.

[zmylinxi99]

The description cannot be found.

Thank you for the reminder.

We have updated the relevant repository and URL for the system description. It should now be accessible.

Please let me know if there are still any issues.

[martinjonas]

@zmylinxi99 Thanks for submitting Bitwuzla-BV_Parti to this year's SMT-COMP! 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.

We are currently working on executing your parallel solver on a small number of test benchmarks to confirm that everything is working correctly. I will send you the results as soon as possible.

[martinjonas]

@zmylinxi99 I finally managed to execute Bitwuzla-BV_Parti on our infrastructure. To do that, I needed to do some changes.

First, the command in the JSON submission should probably be ./Bitwuzla-BV_Parti-at-SMT-COMP-2026/solver/run_BV_Parti.py" instead of ./Bitwuzla-BV_Parti-at-SMT-COMP-2026-build/solver/run_BV_Parti.py. Please fix this in your final submission.

Second, I had to

• Compile my own build of openmpi 5.0.10 and add it to PATH and LD_LIBRARY_PATH.
• Remove all --mca options from BV-Parti_launcher.py, as we run the solver without the network access and it was not able to find the network interface.

Please check that you agree with these changes and let me know if they can result in some issues.

After performing these changes, I have executed your solver on a small number of benchmarks from each competitive logic your solver competes in. You can find the results here:

• https://www.fi.muni.cz/~xjonas/smtcomp/tables/bitwuzlabv_parti_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

[zmylinxi99]

@zmylinxi99 I finally managed to execute Bitwuzla-BV_Parti on our infrastructure. To do that, I needed to do some changes.

First, the command in the JSON submission should probably be ./Bitwuzla-BV_Parti-at-SMT-COMP-2026/solver/run_BV_Parti.py" instead of ./Bitwuzla-BV_Parti-at-SMT-COMP-2026-build/solver/run_BV_Parti.py. Please fix this in your final submission.

Second, I had to

• Compile my own build of openmpi 5.0.10 and add it to PATH and LD_LIBRARY_PATH.
• Remove all --mca options from BV-Parti_launcher.py, as we run the solver without the network access and it was not able to find the network interface.

Please check that you agree with these changes and let me know if they can result in some issues.

After performing these changes, I have executed your solver on a small number of benchmarks from each competitive logic your solver competes in. You can find the results here:

• https://www.fi.muni.cz/~xjonas/smtcomp/tables/bitwuzlabv_parti_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

Hi Martin,

Thank you very much for the test run and the detailed notes.

I agree with both changes. The JSON command should use ./Bitwuzla-BV_Parti-at-SMT-COMP-2026/solver/run_BV_Parti.py, and I will fix this in the final submission.

Using OpenMPI 5.0.10 should be fine. Removing the --mca options is also OK, since they were only used for our local network configuration and are not required by the solver logic. This should not affect correctness; at most it may affect MPI launch behavior or performance depending on the environment.

The reported results look expected to me, and I did not notice any issue. I will update the final submission accordingly.

Thanks again for your help!

Mengyu