SMT generation was wrong in more ways than one. Fixing.

ethereum / hevm

symbolic EVM evaluator

https://hevm.dev

GNU Affero General Public License v3.0

223 stars 45 forks source link

Closed msooseth closed 5 months ago

msooseth commented 5 months ago

concat is a 2-ary, not an n-ary function in SMTLIB2. This fixes this error

declare-const does not exist in QF_AUFBV, replacing with declare-fun ()

Closes #456

msooseth commented 5 months ago

@CodiumAI-Agent /review