GHC 9.6 v4 try, with CVC5 this time around.

ethereum / hevm

symbolic EVM evaluator

https://hevm.dev

GNU Affero General Public License v3.0

235 stars 48 forks source link

GHC 9.6 v4 try, with CVC5 this time around. #507

Closed msooseth closed 3 months ago

msooseth commented 3 months ago

Description

Test with CVC5 as default for

Checklist

[ ] tested locally
[ ] added automated tests
[ ] updated the docs
[ ] updated the changelog

ggrieco-tob commented 3 months ago

Is CVC5 support coming? I think I tested some time ago and it was broken :thinking:

msooseth commented 3 months ago

Yeah, unfortunately you are right. We get: Array theory solver does not yet support write-chains connecting two different constant arrays for a single test. I disabled that test for the moment. Just to try.

Test was: keccak concrete and sym injectivity

d-xo commented 3 months ago

Awesome to see a green 9.6 finally. I don't love that we have no test coverage for z3 and bitwuzla in ci like this now though.

d-xo commented 3 months ago

closing since https://github.com/ethereum/hevm/pull/499 is merged