test: add balance reverting case

tests/expected/all.json

@@ -806,6 +806,14 @@
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
+            },
+            {
+                "name": "check_RevertBalance(bool,uint256)",
+                "exitcode": 0,
+                "num_models": 0,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
             }
         ],
         "test/Send.t.sol:SendTest": [
@@ -1081,4 +1089,4 @@
             }
         ]
     }
-}
+}

tests/test/Revert.t.sol

@@ -3,6 +3,8 @@ pragma solidity >=0.8.0 <0.9.0;
 
 // from https://github.com/a16z/halmos/issues/109
 
+import "forge-std/Test.sol";
+
 contract C {
     uint256 public num;
 
@@ -15,9 +17,13 @@ contract C {
         revert("blah");
         num = x;
     }
+
+    function deposit(bool paused) public payable {
+        if (paused) revert("paused");
+    }
 }
 
-contract CTest {
+contract CTest is Test {
     C c;
 
     function setUp() public {
@@ -37,4 +43,21 @@ contract CTest {
         assert(!result);
         assert(c.num() != x);
     }
+
+    function check_RevertBalance(bool paused, uint256 amount) public {
+        vm.deal(address(this), amount);
+        vm.deal(address(c), 0);
+
+        (bool result,) = address(c).call{value: amount}(abi.encodeWithSignature("deposit(bool)", paused));
+
+        if (result) {
+            assert(!paused);
+            assert(address(this).balance == 0);
+            assert(address(c).balance == amount);
+        } else {
+            assert(paused);
+            assert(address(this).balance == amount);
+            assert(address(c).balance == 0);
+        }
+    }
 }