-
Notifications
You must be signed in to change notification settings - Fork 34
Bitwuzla-MachBV Submission for SMT-COMP 2025 #171
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Conversation
Summary of modified submissionsBitwuzla-0-7-0
Bitwuzla-MachBV
|
#189: UltimateEliminator submission 2025 #188: Z3-Siri Submission 2025 #187: OSTRICH version 2 #186: yicesQS submission to the 2025 SMT comp #185: Bitwuzla 2025 submission. #184: Yices2 Submission SMTCOMP 2025 #183: cvc5 for SMT-COMP 2025 #182: Create iProver #181: Z3-Owl Submission 2025 #179: Z3-alpha SMT-COMP 2025 #178: Z3-Noodler-Mocha Submission for SMT-COMP 2025 #177: `bv_decide` submission 2025 #176: OpenSMT (min-ucore) submission 2025 #175: Z3-Noodler submission 2025 #172: SMTS submission 2025 #171: Bitwuzla-MachBV Submission for SMT-COMP 2025 #170: Z3-Parti-Z3++ Submission for SMT-COMP 2025 #169: STP-Parti-Bitwuzla Submission for SMT-COMP 2025 #168: SMTInterpol submission 2025 #167: OpenSMT submission 2025 #165: Amaya 2025 #164: SMT-RAT submission #163: COLIBRI submission #162: [Submission] colibri2 #156: upload z3-inc-z3++
|
@Andeviking Thanks for submitting Bitwuzla-MachBV 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:
We have not seen any incorrect results returned by your solver (compared to the expected status of the benchmarks). You can check whether all the results we have obtained are expected. If not, please let us know here. Some notes:
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! |
|
@martinjonas Thanks for your work! We have submitted a new version of the solver and would appreciate it if you could test it. Additionally, I noticed that there might be some issues with the workflow: every time I update the json file, an error related to venv appears in the checks.
|
|
Thanks for letting us know, the CI should be fixed now. I will run new test runs of your solver in few hours. |

init