Concrete vs Symbolic data inputs

[acmLL]

Hi,

I am using a MacBook M1 Pro, 32 GB RAM, Sonoma 14.2.1 macOS. I am verifying this simple symbolic test (in the following code, token is an instance of openzeppelling ERC20Mock.sol contract---import {ERC20Mock} from "@openzeppelin/mocks/token/ERC20Mock.sol";)

function prove_Approve(address msg_sender, address spender, uint256 amount, bool success) public {
    require(msg_sender != address(0) && spender != address(0) && msg_sender != spender && success);
    vm.prank(msg_sender);
    success = token.approve(spender, amount);
    assert(success);
    assert(token.allowance(msg_sender, spender) ==  amount);
}

which always PASS, even if I remove the entire require statement (This is strange). If I use address(0) instead of spender or msg_sender, as well as consider msg_sender == sender as the same variable name when calling the functions, then hevm reports a FAIL. Why is this the case? How should I use hevm in this situation? I'm somewhat unsure about the parameter and require usage due to such outcomes.

Thanks!

[acmLL]

I saw that I have to use try/catch + assert(false) to get what I want. Thanks

[msooseth]

Sorry, I actually did look at this, but it wasn't obvious to me what you were trying to do. Can you maybe write here what the solution was? I wanna understand what the misunderstanding may have been, so when I write the documentation, I can explain this part a bit better. I wanna make sure this thing is more easy to use :) Thank you in advance,

Mate

[acmLL]

I got what I needed with the following code

function prove_Approve(address msg_sender, address spender, uint256 amount) public { require(msg_sender != address(0) && spender != address(0)); vm.prank(msg_sender); try token.approve(spender, amount) returns (bool success) { assert(success); } catch { assert(false); } assert(token.allowance(msg_sender, spender) == amount); }