This provides the ability to call Bitwuzla with problems generated by the bv_decide tactic
frontend. You can call it like this:
bv_bitwuzla "/path/to/bitwuzla"
To point the tool towards the solver and if you want to see what bitwuzla is doing:
set_option diagnostics true
Alternatively to compare bv_decide and bv_bitwuzla directly run:
bv_compare "/path/to/bitwuzla"
This tool:
- is a development tool for figuring out differences between what Bitwuzla and
bv_decidecan do. - is not meant to be used productively
- does not necessarily produce a sound reduction to SMT-lib