leanwuzla

Tactic Frontend

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"

SMT-LIB v2 Terminal Frontend

This provides the ability to call bv_decide with QF_BV SMT-LIB v2 problems. You can call it like this:

lake exe leanwuzla [-D name=value] /path/to/file.smt2

Quality and Stability

This tool:

• is a development tool for figuring out differences between what Bitwuzla and bv_decide can do.
• is not meant to be used productively
• does not necessarily produce a sound reduction to SMT-lib