I added Bitwuzla support to my GCC translation validator, smtgcc. The performance improvement over Z3 and cvc5 is impressive!
https://github.com/kristerw/smtgcc

@kristerw Boolector (the predecessor) is really damn good for verifying that RISC-V soft-cores behave as expected. Unfortunately, I've found it difficult to build Bitwuzla on Windoze, so I've stuck w/ Boolector.

(Also I can't remember if it's faster or slower than Boolector on the RISC-V stuff. But hey, that's SMT solvers for you.)

@kristerw Boolector (the predecessor) is really damn good for verifying that RISC-V soft-cores behave as expected. Unfortunately, I've found it difficult to build Bitwuzla on Windoze, so I've stuck w/ Boolector.

(Also I can't remember if it's faster or slower than Boolector on the RISC-V stuff. But hey, that's SMT solvers for you.)

@kristerw Boolector (the predecessor) is really damn good for verifying that RISC-V soft-cores behave as expected. Unfortunately, I've found it difficult to build Bitwuzla on Windoze, so I've stuck w/ Boolector.

(Also I can't remember if it's faster or slower than Boolector on the RISC-V stuff. But hey, that's SMT solvers for you.)

@kristerw Boolector (the predecessor) is really damn good for verifying that RISC-V soft-cores behave as expected. Unfortunately, I've found it difficult to build Bitwuzla on Windoze, so I've stuck w/ Boolector.

(Also I can't remember if it's faster or slower than Boolector on the RISC-V stuff. But hey, that's SMT solvers for you.)