HEVM prove: "Unexpected response from the solver, context: define-fun"

[transmissions11]

When running a simple symbolic test that deposits into a contract which transfers and mints a token, the SMTChecker will error out with this cryptic message:

hevm: 
*** Data.SBV: Unexpected response from the solver, context: define-fun:
***
***    Sent      : (define-fun array_51 () (Array (_ BitVec 256) (_ BitVec 256)) ((as const (Array (_ BitVec 256) (_ BitVec 256))) s32))
***    Expected  : success
***    Received  : (error "Parse Error: <shell>:1.115: expected constant term inside array constant, but found nonconstant term:
***                the term: s32")
***
***    Executable: /nix/store/2jfvasr5572wa0mm44ssakrp4a6mgm9d-cvc4-1.8/bin/cvc4
***    Options   : --lang=smt --incremental --interactive --no-interactive-prompt --model-witness-value --tlimit-per=30000

Here's a reproduction test-case:

https://github.com/Rari-Capital/vaults/blob/65b2de14363a1481ca2e251d308d1100fcfacb8c/src/tests/Vault.t.sol#L30

The issue is demonstrated in CI: https://github.com/Rari-Capital/vaults/runs/2919981668

To play around yourself simply clone the branch and run make.

[MrChico]

This is a known issue, unfortunately, that I once thought I solved with #582, but it has reappeared lately. Its only present with cvc4 in some particular circumstances. As a workaround for now you can use --solver z3 instead of cvc4

[MrChico]

Long term we should investigate further if the situation can be improved in sbv, but also make z3 the default solver again

[transmissions11]

This is a known issue, unfortunately, that I once thought I solved with #582, but it has reappeared lately. Its only present with cvc4 in some particular circumstances. As a workaround for now you can use --solver z3 instead of cvc4

yup z3 works. is cvc4 considered superior or something?

[d-xo]

I think it probably depends on the use case, but at least for hevm we've generally found cvc4 to be faster, especially for cases where calldata is completely abstract (e.g. searching for assertions in all possible executions of all methods on a contract via hevm symbolic).