HEVM prove: `Data.SBV: Unexpected response from the solver, context: push:`

[mds1]

Overview

I'm seeing failures with the simple prove test defined here. You can use this branch to reproduce the issue.

Some other info:

• I've tried both solvers and posted the test command and outputs from each below.
• The RPC URL I'm using is a forked mainnet node from Alchemy. I have not yet tested against a non-fork, since it'd require a decent amount of changes, and I typically dev/test against a forked mainnet anyway
• Searching for this error in this repo's issues and I found one reference to this here: Dynamic buffers via SMT lists #500 (comment)
• According to dapp --version, I'm using dapp 0.32.2, hevm 0.46.0, and solc 0.6.7+commit.b8d736ae.Darwin.appleclang

z3 solver

Run using dapp test --verbose --rpc ${ETH_RPC_URL} --solver z3. Fails relatively quickly with the below error

hevm: 
*** Data.SBV: Unexpected response from the solver, context: push:
***
***    Sent      : (push 1)
***    Expected  : success
***    Received  : (error "line 57181 column 7: push canceled")
***
***    Executable: /nix/store/d7xd3hqgwqz7z7q54kyiac1swhyf5372-z3-4.8.10/bin/z3
***    Options   : -nw -in -smt2

cvc4 solver

Run using dapp test --verbose --rpc ${ETH_RPC_URL} --solver cvc4. After waiting for about an hour or two I finally quit the process, so have no error output to show here

[mds1]

Another reproduction case: try verifying that the EVM (L1) and OVM (L2) versions of the Uniswap V3 SwapRouter are equivalent:

# Define URL for Optimistic Ethereum Node
OE_RPC_URL=https://urlToOptimisticEthereumNode

# Check equivalence
hevm equivalence --code-a $(seth code 0xE592427A0AEce92De3Edee1F18E0157C05861564) --code-b $(seth code 0xE592427A0AEce92De3Edee1F18E0157C05861564 --rpc-url=$OE_RPC_URL)

This hangs for a while, and after about an hour it finally fails with

hevm:
*** Data.SBV: Unexpected response from the solver, context: push:
***
***    Sent      : (push 1)
***    Expected  : success
***    Received  : (error "line 28733 column 7: canceled")
***
***    Executable: /nix/store/d7xd3hqgwqz7z7q54kyiac1swhyf5372-z3-4.8.10/bin/z3
***    Options   : -nw -in -smt2

[mds1]

It seems likely that the hevm equivalence failure in the previous comment is due to the fact that the contract at that address contains a while (true) loop that throws off the solver. (h/t @d-xo for pointing this out). So probably safe to ignore that one