act hevm fails to prove Pass claim when Payable keyword is missing

[koolexcrypto]

If you run
act hevm
with the following example:
https://github.com/d-xo/act-examples/blob/main/src/simple.sol

You get
Failed to prove set(Pass)

Is there a reason why would we need this in a simple set function?

[d-xo]

If you remove the payable then you also need to update the spec to reflect this.

If you add a block like this:

iff
  CALLVALUE == 0

to the spec after removing the payable from the solidity source, then I think act hevm should show them to be equivalent again.

[koolexcrypto]

@d-xo
Thank you! I wasn't aware of this. I assumed by default the value is zero. but it doesn't seem the case here .
I am gonna try this out and give an update here later

[koolexcrypto]

I confirm that after adding

iff
  CALLVALUE == 0

It works!

Thank you again!