vm.createFork() not supported

[fyang1024]

Describe the bug halmos threw an error when the setUp() function invokes vm operations.

The error on the console was

Traceback (most recent call last): File "/Users/.../Library/Python/3.9/bin/halmos", line 8, in sys.exit(main()) File "/Users/.../Library/Python/3.9/lib/python/site-packages/halmos/main.py", line 474, in main setup_ex = setup(hexcode, abi, srcmap, srcs, args, setup_sig, options) File "/Users/.../Library/Python/3.9/lib/python/site-packages/halmos/main.py", line 132, in setup if (setup_opcode != 'STOP' and setup_opcode != 'RETURN') or setup_ex.failed: raise ValueError('setUp() failed') ValueError: setUp() failed

To Reproduce

1. Create a simple test in a foundry project as below

// SPDX-License-Identifier: AGPL-3.0-only
pragma solidity ^0.8.13;

import "forge-std/Test.sol";

contract MyTest is Test {

    function setUp() public {
       vm.createFork(vm.envString("RPC_URL_MAINNET"));
    }

    function testFailX() pure public {
        revert();
    }
}

2. run forge test

3. run halmos

Environment:

• OS: macOS
• Python version: 3.9.6
• Halmos and other dependency versions:
  • halmos 0.0.4
  • crytic-compile 0.3.0
  • z3-solver 4.12.1.0

Additional context

If we comment out the vm call like this:

   function setUp() public {
       // vm.createFork(vm.envString("RPC_URL_MAINNET"));
    }

halmos can do the verification, but it produces opposite result for testFail... tests. When foundry reports a PASS, halmos reports a FAILURE, and vice versa.