search

ethereum / hevm

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

Fix cvc5 incremental use #453

Closed msooseth closed 6 months ago

msooseth commented 6 months ago

Description

CVC5 needs the flag --incremental for abstraction-refinement to work. Adding this flag.

Error by cvc5:

*** Exception: Internal Error: solver returned: Unable to parse solver output: (error "Cannot make multiple queries unless incremental solving is enabled (try --incremental)") -- CallStack (from HasCallStack):
  internalError, called at src/EVM/SymExec.hs:717:27 in hevm-0.52.0-CCZJOZs40MI9tgkh5WHYEQ:EVM.SymExec
CallStack (from HasCallStack):
  error, called at src/EVM/Types.hs:1344:19 in hevm-0.52.0-CCZJOZs40MI9tgkh5WHYEQ:EVM.Types
  internalError, called at src/EVM/SymExec.hs:717:27 in hevm-0.52.0-CCZJOZs40MI9tgkh5WHYEQ:EVM.SymExec

Checklist