ethereum / hevm

symbolic EVM evaluator
https://hevm.dev
GNU Affero General Public License v3.0
225 stars 46 forks source link

add support for bitwuzla #438

Closed d-xo closed 7 months ago

d-xo commented 8 months ago

Description

Adds support for Bitwuzla. This is the same as the old PR, but uses a new bitwuzla version (0.3.0), which has support for timeouts This pr also messes with the smt generation less (only real change is replacing define-const with define-fun).

It currently can't pass the full test suite (currently 9 failures due to issues support for comparison of constant arrays), but I enabled it for a few tests where it doesn't error out to make sure we're exercising it in CI.

Checklist