From 7d496d38c6f13a0a4bf81d277771bc234b6ec0d4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andrei=20V=C4=83caru?=
 <16517508+anvacaru@users.noreply.github.com>
Date: Thu, 23 Jan 2025 15:41:36 +0200
Subject: [PATCH] Implement kevm.forgetBranch cheatcode (#899)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* draft FOUNDRYSemantics

* forgetBranch

* add mlEqualsTrue

* minor corrections

* add simplification step

* formatting

* add back not equal

* rename FOUNDRYSemantics to KontrolSemantics

* checking for negation as well

* correcting indentation

* expanding functionality

* heuristic simplifications

* further refinement

* refactoring _exec_forget_custom_step

* add show test

* fix test

* update expected output

---------

Co-authored-by: Petar Maksimovic <petar.maksimovic@runtimeverification.com>
Co-authored-by: Palina <polina.tolmach@gmail.com>
Co-authored-by: Petar Maksimović <PetarMax@users.noreply.github.com>
---
 src/kontrol/foundry.py                        |  143 +-
 src/kontrol/kdist/cheatcodes.md               |   21 +
 src/kontrol/kdist/foundry.md                  |    4 +
 .../test-data/end-to-end-prove-all            |   29 +-
 .../test-data/end-to-end-prove-show           |    1 +
 .../test-data/end-to-end-prove-skip           |   34 +-
 ...chTest.test_forgetBranch(uint256).expected | 1338 +++++++++++++++++
 .../test-data/src/ForgetBranch.t.sol          |   21 +
 8 files changed, 1555 insertions(+), 36 deletions(-)
 create mode 100644 src/tests/integration/test-data/show/ForgetBranchTest.test_forgetBranch(uint256).expected
 create mode 100644 src/tests/integration/test-data/src/ForgetBranch.t.sol

diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py
index cbd6f7c4e..0a5dfbd08 100644
--- a/src/kontrol/foundry.py
+++ b/src/kontrol/foundry.py
@@ -26,6 +26,7 @@
     collect,
     extract_lhs,
     flatten_label,
+    free_vars,
     minimize_term,
     set_cell,
     top_down,
@@ -34,9 +35,10 @@
 from pyk.kcfg import KCFG
 from pyk.kcfg.kcfg import Step
 from pyk.kcfg.minimize import KCFGMinimizer
+from pyk.kdist import kdist
 from pyk.prelude.bytes import bytesToken
 from pyk.prelude.collections import map_empty
-from pyk.prelude.k import DOTS
+from pyk.prelude.k import DOTS, GENERATED_TOP_CELL
 from pyk.prelude.kbool import notBool
 from pyk.prelude.kint import INT, intToken
 from pyk.prelude.ml import mlEqualsFalse, mlEqualsTrue
@@ -103,7 +105,7 @@ def cut_point_rules(
         break_on_basic_blocks: bool,
         break_on_load_program: bool,
     ) -> list[str]:
-        return ['FOUNDRY-CHEAT-CODES.rename'] + KEVMSemantics.cut_point_rules(
+        return ['FOUNDRY-CHEAT-CODES.rename', 'FOUNDRY-ACCOUNTS.forget'] + KEVMSemantics.cut_point_rules(
             break_on_jumpi,
             break_on_jump,
             break_on_calls,
@@ -153,14 +155,145 @@ def _exec_rename_custom_step(self, cterm: CTerm) -> KCFGExtendResult | None:
         _LOGGER.info(f'Renaming {target_var.name} to {name}')
         return Step(CTerm(new_cterm.config, constraints), 1, (), ['foundry_rename'], cut=True)
 
-    def custom_step(self, cterm: CTerm, _cterm_symbolic: CTermSymbolic) -> KCFGExtendResult | None:
+    def _check_forget_pattern(self, cterm: CTerm) -> bool:
+        """Given a CTerm, check if the rule 'FOUNDRY-ACCOUNTS.forget' is at the top of the K_CELL.
+        This method checks if the 'FOUNDRY-ACCOUNTS.forget' rule is at the top of the `K_CELL` in the given `cterm`.
+        If the rule matches, the resulting substitution is cached in `_cached_subst` for later use in `custom_step`
+        :param cterm: The CTerm representing the current state of the proof node.
+        :return: `True` if the pattern matches and a custom step can be made; `False` otherwise.
+        """
+        abstract_pattern = KSequence(
+            [
+                KApply('cheatcode_forget', [KVariable('###TERM1'), KVariable('###OPERATOR'), KVariable('###TERM2')]),
+                KVariable('###CONTINUATION'),
+            ]
+        )
+        self._cached_subst = abstract_pattern.match(cterm.cell('K_CELL'))
+        return self._cached_subst is not None
+
+    def _exec_forget_custom_step(self, cterm: CTerm, cterm_symbolic: CTermSymbolic) -> KCFGExtendResult | None:
+        """Remove the constraint at the top of K_CELL of a given CTerm from its path constraints,
+           as part of the 'FOUNDRY-ACCOUNTS.forget' cut-rule.
+        :param cterm: CTerm representing a proof node
+        :param cterm_symbolic: CTermSymbolic instance
+        :return: A Step of depth 1 carrying a new configuration in which the constraint is consumed from the top
+                 of the K cell and is removed from the initial path constraints if it existed, together with
+                 information that the `cheatcode_forget` rule has been applied.
+        """
+
+        def _find_constraints_to_keep(cterm: CTerm, constraint_vars: frozenset[str]) -> set[KInner]:
+            range_patterns: list[KInner] = [
+                mlEqualsTrue(KApply('_<Int_', KVariable('###VARL', INT), KVariable('###VARR', INT))),
+                mlEqualsTrue(KApply('_<=Int_', KVariable('###VARL', INT), KVariable('###VARR', INT))),
+                mlEqualsTrue(notBool(KApply('_==Int_', KVariable('###VARL', INT), KVariable('###VARR', INT)))),
+            ]
+            constraints_to_keep: set[KInner] = set()
+            for constraint in cterm.constraints:
+                for pattern in range_patterns:
+                    subst_rcp = pattern.match(constraint)
+                    if subst_rcp is not None and (
+                        (
+                            type(subst_rcp['###VARL']) is KVariable
+                            and subst_rcp['###VARL'].name in constraint_vars
+                            and type(subst_rcp['###VARR']) is KToken
+                        )
+                        or (
+                            type(subst_rcp['###VARR']) is KVariable
+                            and subst_rcp['###VARR'].name in constraint_vars
+                            and type(subst_rcp['###VARL']) is KToken
+                        )
+                    ):
+                        constraints_to_keep.add(constraint)
+                        break
+            return constraints_to_keep
+
+        def _filter_constraints_by_simplification(
+            cterm_symbolic: CTermSymbolic,
+            initial_cterm: CTerm,
+            constraints_to_remove: list[KInner],
+            constraints_to_keep: set[KInner],
+            constraints: set[KInner],
+            empty_config: CTerm,
+        ) -> set[KInner]:
+            for constraint_variant in constraints_to_remove:
+                simplification_cterm = initial_cterm.add_constraint(constraint_variant)
+                result_cterm, _ = cterm_symbolic.simplify(simplification_cterm)
+                # Extract constraints that appear after simplification but are not in the 'to keep' set
+                result_constraints = set(result_cterm.constraints).difference(constraints_to_keep)
+
+                if len(result_constraints) == 1:
+                    target_constraint = single(result_constraints)
+                    if target_constraint in constraints:
+                        _LOGGER.info(f'forgetBranch: removing constraint: {target_constraint}')
+                        constraints.remove(target_constraint)
+                        break
+                    else:
+                        _LOGGER.info(f'forgetBranch: constraint: {target_constraint} not found in current constraints')
+                else:
+                    # If no constraints or multiple constraints appear, log this scenario.
+                    if len(result_constraints) == 0:
+                        _LOGGER.info(f'forgetBranch: constraint {constraint_variant} entailed by remaining constraints')
+                        result_cterm, _ = cterm_symbolic.simplify(CTerm(empty_config.config, [constraint_variant]))
+                        if len(result_cterm.constraints) == 1:
+                            to_remove = single(result_cterm.constraints)
+                            if to_remove in constraints:
+                                _LOGGER.info(f'forgetBranch: removing constraint: {to_remove}')
+                                constraints.remove(to_remove)
+                    else:
+                        _LOGGER.info(
+                            f'forgetBranch: more than one constraint found after simplification and removal:\n{result_constraints}'
+                        )
+            return constraints
+
+        _operators = ['_==Int_', '_=/=Int_', '_<=Int_', '_<Int_', '_>=Int_', '_>Int_']
+        subst = self._cached_subst
+        assert subst is not None
+        # Extract the terms and operator from the substitution
+        fst_term = subst['###TERM1']
+        snd_term = subst['###TERM2']
+        operator = subst['###OPERATOR']
+        assert isinstance(operator, KToken)
+        # Construct the positive and negative constraints
+        pos_constraint = mlEqualsTrue(KApply(_operators[int(operator.token)], fst_term, snd_term))
+        neg_constraint = mlEqualsTrue(notBool(KApply(_operators[int(operator.token)], fst_term, snd_term)))
+        # To be able to better simplify, we maintain range constraints on the variables present in the constraint
+        constraint_vars: frozenset[str] = free_vars(fst_term).union(free_vars(snd_term))
+        constraints_to_keep: set[KInner] = _find_constraints_to_keep(cterm, constraint_vars)
+
+        # Set up initial configuration for constraint simplification, and simplify it to get all
+        # of the kept constraints in the form in which they will appear after constraint simplification
+        kevm = KEVM(kdist.get('kontrol.foundry'))
+        empty_config: CTerm = CTerm.from_kast(kevm.definition.empty_config(GENERATED_TOP_CELL))
+        initial_cterm, _ = cterm_symbolic.simplify(CTerm(empty_config.config, constraints_to_keep))
+        constraints_to_keep = set(initial_cterm.constraints)
+
+        # Simplify in the presence of constraints to keep, then remove the constraints to keep to
+        # reveal simplified constraint, then remove if present in original constraints
+        new_constraints: set[KInner] = _filter_constraints_by_simplification(
+            cterm_symbolic=cterm_symbolic,
+            initial_cterm=initial_cterm,
+            constraints_to_remove=[pos_constraint, neg_constraint],
+            constraints_to_keep=constraints_to_keep,
+            constraints=set(cterm.constraints),
+            empty_config=empty_config,
+        )
+
+        # Update the K_CELL with the continuation
+        new_cterm = CTerm.from_kast(set_cell(cterm.kast, 'K_CELL', KSequence(subst['###CONTINUATION'])))
+        return Step(CTerm(new_cterm.config, new_constraints), 1, (), ['cheatcode_forget'], cut=True)
+
+    def custom_step(self, cterm: CTerm, cterm_symbolic: CTermSymbolic) -> KCFGExtendResult | None:
         if self._check_rename_pattern(cterm):
             return self._exec_rename_custom_step(cterm)
+        elif self._check_forget_pattern(cterm):
+            return self._exec_forget_custom_step(cterm, cterm_symbolic)
         else:
-            return super().custom_step(cterm, _cterm_symbolic)
+            return super().custom_step(cterm, cterm_symbolic)
 
     def can_make_custom_step(self, cterm: CTerm) -> bool:
-        return self._check_rename_pattern(cterm) or super().can_make_custom_step(cterm)
+        return any(
+            [self._check_rename_pattern(cterm), self._check_forget_pattern(cterm), super().can_make_custom_step(cterm)]
+        )
 
 
 class FoundryKEVM(KEVM):
diff --git a/src/kontrol/kdist/cheatcodes.md b/src/kontrol/kdist/cheatcodes.md
index c7c4ffcc9..15da6c2a9 100644
--- a/src/kontrol/kdist/cheatcodes.md
+++ b/src/kontrol/kdist/cheatcodes.md
@@ -1142,6 +1142,26 @@ Mock functions
       [priority(30)]
 ```
 
+
+Abstraction functions
+---------------------
+
+#### `forgetBranch` - removes a given path constraint.
+
+```
+    function forgetBranch(uint256 op1, ComparisonOperator op, uint256 op2) external;
+```
+
+```k
+    rule [cheatcode.call.abstract]:
+         <k> #cheatcode_call SELECTOR ARGS
+          => #forget ( #asWord(#range(ARGS,0,32)), #asWord(#range(ARGS,32,32)), #asWord(#range(ARGS,64,32)))
+          ...
+         </k>
+      requires SELECTOR ==Int selector ( "forgetBranch(uint256,uint8,uint256)" )
+
+```
+
 Utils
 -----
 
@@ -1751,6 +1771,7 @@ Selectors for **implemented** cheat code functions.
     rule ( selector ( "mockCall(address,bytes,bytes)" )            => 3110212580 )
     rule ( selector ( "mockFunction(address,address,bytes)" )      => 2918731041 )
     rule ( selector ( "copyStorage(address,address)" )             => 540912653  )
+    rule ( selector ( "forgetBranch(uint256,uint8,uint256)" )      => 1720990067 )
 ```
 
 Selectors for **unimplemented** cheat code functions.
diff --git a/src/kontrol/kdist/foundry.md b/src/kontrol/kdist/foundry.md
index 2ac8861a7..871f0dd18 100644
--- a/src/kontrol/kdist/foundry.md
+++ b/src/kontrol/kdist/foundry.md
@@ -78,6 +78,10 @@ Then, we define helpers in K which can:
              <storage> STORAGE => STORAGE [ #loc(FoundryCheat . Failed) <- 1 ] </storage>
              ...
            </account>
+
+    syntax KItem ::= #forget ( Int , Int , Int ) [symbol(cheatcode_forget)]
+ // -----------------------------------------------------------------------
+    rule [forget]: <k> #forget(_C1,_OP,_C2) => .K ... </k>
 ```
 
 #### Structure of execution
diff --git a/src/tests/integration/test-data/end-to-end-prove-all b/src/tests/integration/test-data/end-to-end-prove-all
index 6a2bc826c..749effdd8 100644
--- a/src/tests/integration/test-data/end-to-end-prove-all
+++ b/src/tests/integration/test-data/end-to-end-prove-all
@@ -1,14 +1,25 @@
 CounterTest.test_Increment()
+ForgetBranchTest.test_forgetBranch(uint256)
 RandomVarTest.test_custom_names()
-RandomVarTest.test_randomBool()
 RandomVarTest.test_randomAddress()
-RandomVarTest.test_randomUint()
-RandomVarTest.test_randomUint_192()
-RandomVarTest.test_randomUint_Range(uint256,uint256)
+RandomVarTest.test_randomBool()
 RandomVarTest.test_randomBytes_length(uint256)
 RandomVarTest.test_randomBytes4_length()
 RandomVarTest.test_randomBytes8_length()
+RandomVarTest.test_randomUint_192()
+RandomVarTest.test_randomUint_Range(uint256,uint256)
+RandomVarTest.test_randomUint()
 TransientStorageTest.testTransientStoreLoad(uint256,uint256)
+UnitTest.test_assert_eq_address_darray(address[])
+UnitTest.test_assert_eq_bool_darray(bool[])
+UnitTest.test_assert_eq_bytes32_darray(bytes32[])
+UnitTest.test_assert_eq_int256_darray(int256[])
+UnitTest.test_assert_eq_uint256_darray(uint256[])
+UnitTest.test_assertApproxEqAbs_int_same_sign(uint256,uint256,uint256)
+UnitTest.test_assertApproxEqAbs_uint(uint256,uint256,uint256)
+UnitTest.test_assertApproxEqRel_int_same_sign_unit()
+UnitTest.test_assertApproxEqRel_int_zero_cases_unit()
+UnitTest.test_assertApproxEqRel_uint_unit()
 UnitTest.test_assertEq_address_err()
 UnitTest.test_assertEq_bool_err()
 UnitTest.test_assertEq_bytes32_err()
@@ -39,13 +50,3 @@ UnitTest.test_assertNotEq(bytes32,bytes32)
 UnitTest.test_assertNotEq(int256,int256)
 UnitTest.test_assertTrue_err()
 UnitTest.test_assertTrue(bool)
-UnitTest.test_assertApproxEqAbs_uint(uint256,uint256,uint256)
-UnitTest.test_assertApproxEqAbs_int_same_sign(uint256,uint256,uint256)
-UnitTest.test_assertApproxEqRel_uint_unit()
-UnitTest.test_assertApproxEqRel_int_same_sign_unit()
-UnitTest.test_assertApproxEqRel_int_zero_cases_unit()
-UnitTest.test_assert_eq_bytes32_darray(bytes32[])
-UnitTest.test_assert_eq_bool_darray(bool[])
-UnitTest.test_assert_eq_int256_darray(int256[])
-UnitTest.test_assert_eq_uint256_darray(uint256[])
-UnitTest.test_assert_eq_address_darray(address[])
diff --git a/src/tests/integration/test-data/end-to-end-prove-show b/src/tests/integration/test-data/end-to-end-prove-show
index 028eb6cd8..067333b96 100644
--- a/src/tests/integration/test-data/end-to-end-prove-show
+++ b/src/tests/integration/test-data/end-to-end-prove-show
@@ -1 +1,2 @@
+ForgetBranchTest.test_forgetBranch(uint256)
 RandomVarTest.test_custom_names()
diff --git a/src/tests/integration/test-data/end-to-end-prove-skip b/src/tests/integration/test-data/end-to-end-prove-skip
index 903580e0c..2668de8ef 100644
--- a/src/tests/integration/test-data/end-to-end-prove-skip
+++ b/src/tests/integration/test-data/end-to-end-prove-skip
@@ -1,3 +1,19 @@
+UnitTest.test_assert_eq_address_darray_err()
+UnitTest.test_assert_eq_bool_darray_err()
+UnitTest.test_assert_eq_bytes32_darray_err()
+UnitTest.test_assert_eq_int256_darray_err()
+UnitTest.test_assert_eq_uint256_darray_err()
+UnitTest.test_assertApproxEqAbs_int_opp_sign_err()
+UnitTest.test_assertApproxEqAbs_int_opp_sign(uint256,uint256,uint256)
+UnitTest.test_assertApproxEqAbs_int_same_sign_err()
+UnitTest.test_assertApproxEqAbs_int_zero_cases_err()
+UnitTest.test_assertApproxEqAbs_int_zero_cases(uint256,uint256)
+UnitTest.test_assertApproxEqAbs_uint_err()
+UnitTest.test_assertApproxEqRel_int_opp_sign_err()
+UnitTest.test_assertApproxEqRel_int_opp_sign_unit()
+UnitTest.test_assertApproxEqRel_int_same_sign_err()
+UnitTest.test_assertApproxEqRel_int_zero_cases_err()
+UnitTest.test_assertApproxEqRel_uint_err()
 UnitTest.test_assertEq_address_err()
 UnitTest.test_assertEq_bool_err()
 UnitTest.test_assertEq_bytes32_err()
@@ -13,20 +29,4 @@ UnitTest.test_assertNotEq_bool_err()
 UnitTest.test_assertNotEq_bytes32_err()
 UnitTest.test_assertNotEq_err()
 UnitTest.test_assertNotEq_int256_err()
-UnitTest.test_assertTrue_err()
-UnitTest.test_assertApproxEqAbs_uint_err()
-UnitTest.test_assertApproxEqAbs_int_same_sign_err()
-UnitTest.test_assertApproxEqAbs_int_opp_sign(uint256,uint256,uint256)
-UnitTest.test_assertApproxEqAbs_int_opp_sign_err()
-UnitTest.test_assertApproxEqAbs_int_zero_cases(uint256,uint256)
-UnitTest.test_assertApproxEqAbs_int_zero_cases_err()
-UnitTest.test_assertApproxEqRel_uint_err()
-UnitTest.test_assertApproxEqRel_int_same_sign_err()
-UnitTest.test_assertApproxEqRel_int_opp_sign_unit()
-UnitTest.test_assertApproxEqRel_int_opp_sign_err()
-UnitTest.test_assertApproxEqRel_int_zero_cases_err()
-UnitTest.test_assert_eq_bytes32_darray_err()
-UnitTest.test_assert_eq_bool_darray_err()
-UnitTest.test_assert_eq_int256_darray_err()
-UnitTest.test_assert_eq_address_darray_err()
-UnitTest.test_assert_eq_uint256_darray_err()
\ No newline at end of file
+UnitTest.test_assertTrue_err()
\ No newline at end of file
diff --git a/src/tests/integration/test-data/show/ForgetBranchTest.test_forgetBranch(uint256).expected b/src/tests/integration/test-data/show/ForgetBranchTest.test_forgetBranch(uint256).expected
new file mode 100644
index 000000000..aec40fd4a
--- /dev/null
+++ b/src/tests/integration/test-data/show/ForgetBranchTest.test_forgetBranch(uint256).expected
@@ -0,0 +1,1338 @@
+
+┌─ 1 (root, init)
+│   k: #execute ~> CONTINUATION:K
+│   pc: 0
+│   callDepth: 0
+│   statusCode: STATUSCODE:StatusCode
+│   src: test/ForgetBranch.t.sol:8:21
+│   method: test%ForgetBranchTest.test_forgetBranch(uint256)
+│
+│  (755 steps)
+├─ 3
+│   k: #forget ( KV0_x:Int , 5 , 200 ) ~> #cheatcode_return 128 0 ~> #pc [ CALL ] ~> #e ...
+│   pc: 1294
+│   callDepth: 0
+│   statusCode: STATUSCODE:StatusCode
+│   src: test/ForgetBranch.t.sol:14:14
+│   method: test%ForgetBranchTest.test_forgetBranch(uint256)
+│
+│  (1 step)
+├─ 4
+│   k: #cheatcode_return 128 0 ~> #pc [ CALL ] ~> #execute ~> CONTINUATION:K
+│   pc: 1294
+│   callDepth: 0
+│   statusCode: STATUSCODE:StatusCode
+│   src: test/ForgetBranch.t.sol:14:14
+│   method: test%ForgetBranchTest.test_forgetBranch(uint256)
+│
+│  (72 steps)
+├─ 5 (split)
+│   k: JUMPI 1326 bool2Word ( KV0_x:Int <=Int 200 ) ~> #pc [ JUMPI ] ~> #execute ~> CON ...
+│   pc: 1322
+│   callDepth: 0
+│   statusCode: STATUSCODE:StatusCode
+│   src: test/ForgetBranch.t.sol:15:19
+│   method: test%ForgetBranchTest.test_forgetBranch(uint256)
+┃
+┃ (branch)
+┣━━┓ subst: .Subst
+┃  ┃ constraint:
+┃  ┃     KV0_x:Int <=Int 200
+┃  │
+┃  ├─ 6
+┃  │   k: JUMPI 1326 bool2Word ( KV0_x:Int <=Int 200 ) ~> #pc [ JUMPI ] ~> #execute ~> CON ...
+┃  │   pc: 1322
+┃  │   callDepth: 0
+┃  │   statusCode: STATUSCODE:StatusCode
+┃  │   src: test/ForgetBranch.t.sol:15:19
+┃  │   method: test%ForgetBranchTest.test_forgetBranch(uint256)
+┃  │
+┃  │  (49 steps)
+┃  ├─ 8 (terminal)
+┃  │   k: #halt ~> CONTINUATION:K
+┃  │   pc: 320
+┃  │   callDepth: 0
+┃  │   statusCode: EVMC_SUCCESS
+┃  │   src: test/ForgetBranch.t.sol:10:20
+┃  │   method: test%ForgetBranchTest.test_forgetBranch(uint256)
+┃  │
+┃  ┊  constraint: true
+┃  ┊  subst: ...
+┃  └─ 2 (leaf, target, terminal)
+┃      k: #halt ~> CONTINUATION:K
+┃      pc: PC_CELL_5d410f2a:Int
+┃      callDepth: CALLDEPTH_CELL_5d410f2a:Int
+┃      statusCode: STATUSCODE_FINAL:StatusCode
+┃
+┗━━┓ subst: .Subst
+   ┃ constraint:
+   ┃     200 <Int KV0_x:Int
+   │
+   ├─ 7
+   │   k: JUMPI 1326 bool2Word ( KV0_x:Int <=Int 200 ) ~> #pc [ JUMPI ] ~> #execute ~> CON ...
+   │   pc: 1322
+   │   callDepth: 0
+   │   statusCode: STATUSCODE:StatusCode
+   │   src: test/ForgetBranch.t.sol:15:19
+   │   method: test%ForgetBranchTest.test_forgetBranch(uint256)
+   │
+   │  (40 steps)
+   ├─ 9 (terminal)
+   │   k: #halt ~> CONTINUATION:K
+   │   pc: 320
+   │   callDepth: 0
+   │   statusCode: EVMC_SUCCESS
+   │   src: test/ForgetBranch.t.sol:10:20
+   │   method: test%ForgetBranchTest.test_forgetBranch(uint256)
+   │
+   ┊  constraint: true
+   ┊  subst: ...
+   └─ 2 (leaf, target, terminal)
+       k: #halt ~> CONTINUATION:K
+       pc: PC_CELL_5d410f2a:Int
+       callDepth: CALLDEPTH_CELL_5d410f2a:Int
+       statusCode: STATUSCODE_FINAL:StatusCode
+
+
+
+
+module SUMMARY-TEST%FORGETBRANCHTEST.TEST-FORGETBRANCH(UINT256):0
+    
+    
+    rule [BASIC-BLOCK-1-TO-3]: <foundry>
+           <kevm>
+             <k>
+               ( .K => #forget ( KV0_x:Int , 5 , 200 )
+               ~> #cheatcode_return 128 0
+               ~> #pc [ CALL ] )
+               ~> #execute
+               ~> _CONTINUATION
+             </k>
+             <mode>
+               NORMAL
+             </mode>
+             <schedule>
+               CANCUN
+             </schedule>
+             <useGas>
+               false
+             </useGas>
+             <ethereum>
+               <evm>
+                 <output>
+                   b""
+                 </output>
+                 <callStack>
+                   .List
+                 </callStack>
+                 <interimStates>
+                   .List
+                 </interimStates>
+                 <touchedAccounts>
+                   .Set
+                 </touchedAccounts>
+                 <callState>
+                   <id>
+                     728815563385977040452943777879061427756277306518
+                   </id>
+                   <caller>
+                     CALLER_ID:Int
+                   </caller>
+                   <callData>
+                     b"P#a\xd8" +Bytes #buf ( 32 , KV0_x:Int )
+                   </callData>
+                   <callValue>
+                     0
+                   </callValue>
+                   <wordStack>
+                     ( .WordStack => ( 228 : ( selector ( "forgetBranch(uint256,uint8,uint256)" ) : ( 645326474426547203313410069153905908525362434349 : ( 0 : ( KV0_x:Int : ( 319 : ( selector ( "test_forgetBranch(uint256)" ) : .WordStack ) ) ) ) ) ) ) )
+                   </wordStack>
+                   <localMem>
+                     ( b"" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00f\x949s" +Bytes #buf ( 32 , KV0_x:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x05\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xc8" )
+                   </localMem>
+                   <memoryUsed>
+                     0
+                   </memoryUsed>
+                   <callGas>
+                     0
+                   </callGas>
+                   <static>
+                     false
+                   </static>
+                   <callDepth>
+                     0
+                   </callDepth>
+                   ...
+                 </callState>
+                 <substate>
+                   <log>
+                     .List
+                   </log>
+                   <refund>
+                     0
+                   </refund>
+                   <accessedAccounts>
+                     ( .Set => SetItem ( 645326474426547203313410069153905908525362434349 ) )
+                   </accessedAccounts>
+                   <accessedStorage>
+                     .Map
+                   </accessedStorage>
+                   <createdAccounts>
+                     .Set
+                   </createdAccounts>
+                   ...
+                 </substate>
+                 <origin>
+                   ORIGIN_ID:Int
+                 </origin>
+                 <block>
+                   <number>
+                     NUMBER_CELL:Int
+                   </number>
+                   <timestamp>
+                     TIMESTAMP_CELL:Int
+                   </timestamp>
+                   ...
+                 </block>
+                 ...
+               </evm>
+               <network>
+                 <chainID>
+                   1
+                 </chainID>
+                 <accounts>
+                   ( <account>
+                     <acctID>
+                       645326474426547203313410069153905908525362434349
+                     </acctID>
+                     <balance>
+                       0
+                     </balance>
+                     <storage>
+                       .Map
+                     </storage>
+                     <origStorage>
+                       .Map
+                     </origStorage>
+                     <transientStorage>
+                       .Map
+                     </transientStorage>
+                     <nonce>
+                       0
+                     </nonce>
+                     ...
+                   </account>
+                   <account>
+                     <acctID>
+                       728815563385977040452943777879061427756277306518
+                     </acctID>
+                     <balance>
+                       0
+                     </balance>
+                     <storage>
+                       .Map
+                     </storage>
+                     <origStorage>
+                       .Map
+                     </origStorage>
+                     <transientStorage>
+                       .Map
+                     </transientStorage>
+                     <nonce>
+                       1
+                     </nonce>
+                     ...
+                   </account> )
+                 </accounts>
+                 ...
+               </network>
+             </ethereum>
+             ...
+           </kevm>
+           <stackChecks>
+             false
+           </stackChecks>
+           <cheatcodes>
+             <prank>
+               <active>
+                 false
+               </active>
+               <singleCall>
+                 false
+               </singleCall>
+               ...
+             </prank>
+             <expectedRevert>
+               <isRevertExpected>
+                 false
+               </isRevertExpected>
+               ...
+             </expectedRevert>
+             <expectedOpcode>
+               <isOpcodeExpected>
+                 false
+               </isOpcodeExpected>
+               ...
+             </expectedOpcode>
+             <expectEmit>
+               <recordEvent>
+                 false
+               </recordEvent>
+               <isEventExpected>
+                 false
+               </isEventExpected>
+               ...
+             </expectEmit>
+             <whitelist>
+               <isCallWhitelistActive>
+                 false
+               </isCallWhitelistActive>
+               <isStorageWhitelistActive>
+                 false
+               </isStorageWhitelistActive>
+               <addressList>
+                 .List
+               </addressList>
+               <storageSlotList>
+                 .List
+               </storageSlotList>
+             </whitelist>
+             <mockCalls>
+               .MockCallCellMap
+             </mockCalls>
+             <mockFunctions>
+               .MockFunctionCellMap
+             </mockFunctions>
+           </cheatcodes>
+           <KEVMTracing>
+             <activeTracing>
+               false
+             </activeTracing>
+             <traceStorage>
+               false
+             </traceStorage>
+             <traceWordStack>
+               false
+             </traceWordStack>
+             <traceMemory>
+               false
+             </traceMemory>
+             <recordedTrace>
+               false
+             </recordedTrace>
+             <traceData>
+               .List
+             </traceData>
+           </KEVMTracing>
+         </foundry>
+      requires ( 0 <=Int KV0_x:Int
+       andBool ( 0 <=Int CALLER_ID:Int
+       andBool ( 0 <=Int ORIGIN_ID:Int
+       andBool ( pow24 <Int NUMBER_CELL:Int
+       andBool ( NUMBER_CELL:Int <Int pow32
+       andBool ( 1073741824 <Int TIMESTAMP_CELL:Int
+       andBool ( TIMESTAMP_CELL:Int <Int 34359738368
+       andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349
+       andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349
+       andBool ( _C_FORGETBRANCHTEST_ID =/=Int 645326474426547203313410069153905908525362434349
+       andBool ( CALLER_ID:Int <Int pow160
+       andBool ( ORIGIN_ID:Int <Int pow160
+       andBool ( KV0_x:Int <Int pow256
+       andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
+       andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
+               )))))))))))))))
+       ensures 200 <Int KV0_x:Int
+      [priority(20), label(BASIC-BLOCK-1-TO-3)]
+    
+    rule [BASIC-BLOCK-3-TO-4]: <foundry>
+           <kevm>
+             <k>
+               ( #forget ( KV0_x:Int , 5 , 200 ) ~> .K => .K )
+               ~> #cheatcode_return 128 0
+               ~> #pc [ CALL ]
+               ~> #execute
+               ~> _CONTINUATION
+             </k>
+             <mode>
+               NORMAL
+             </mode>
+             <schedule>
+               CANCUN
+             </schedule>
+             <useGas>
+               false
+             </useGas>
+             <ethereum>
+               <evm>
+                 <output>
+                   b""
+                 </output>
+                 <callStack>
+                   .List
+                 </callStack>
+                 <interimStates>
+                   .List
+                 </interimStates>
+                 <touchedAccounts>
+                   .Set
+                 </touchedAccounts>
+                 <callState>
+                   <id>
+                     728815563385977040452943777879061427756277306518
+                   </id>
+                   <caller>
+                     CALLER_ID:Int
+                   </caller>
+                   <callData>
+                     b"P#a\xd8" +Bytes #buf ( 32 , KV0_x:Int )
+                   </callData>
+                   <callValue>
+                     0
+                   </callValue>
+                   <wordStack>
+                     ( 228 : ( selector ( "forgetBranch(uint256,uint8,uint256)" ) : ( 645326474426547203313410069153905908525362434349 : ( 0 : ( KV0_x:Int : ( 319 : ( selector ( "test_forgetBranch(uint256)" ) : .WordStack ) ) ) ) ) ) )
+                   </wordStack>
+                   <localMem>
+                     b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00f\x949s" +Bytes #buf ( 32 , KV0_x:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x05\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xc8"
+                   </localMem>
+                   <memoryUsed>
+                     0
+                   </memoryUsed>
+                   <callGas>
+                     0
+                   </callGas>
+                   <static>
+                     false
+                   </static>
+                   <callDepth>
+                     0
+                   </callDepth>
+                   ...
+                 </callState>
+                 <substate>
+                   <log>
+                     .List
+                   </log>
+                   <refund>
+                     0
+                   </refund>
+                   <accessedAccounts>
+                     SetItem ( 645326474426547203313410069153905908525362434349 )
+                   </accessedAccounts>
+                   <accessedStorage>
+                     .Map
+                   </accessedStorage>
+                   <createdAccounts>
+                     .Set
+                   </createdAccounts>
+                   ...
+                 </substate>
+                 <origin>
+                   ORIGIN_ID:Int
+                 </origin>
+                 <block>
+                   <number>
+                     NUMBER_CELL:Int
+                   </number>
+                   <timestamp>
+                     TIMESTAMP_CELL:Int
+                   </timestamp>
+                   ...
+                 </block>
+                 ...
+               </evm>
+               <network>
+                 <chainID>
+                   1
+                 </chainID>
+                 <accounts>
+                   ( <account>
+                     <acctID>
+                       645326474426547203313410069153905908525362434349
+                     </acctID>
+                     <balance>
+                       0
+                     </balance>
+                     <storage>
+                       .Map
+                     </storage>
+                     <origStorage>
+                       .Map
+                     </origStorage>
+                     <transientStorage>
+                       .Map
+                     </transientStorage>
+                     <nonce>
+                       0
+                     </nonce>
+                     ...
+                   </account>
+                   <account>
+                     <acctID>
+                       728815563385977040452943777879061427756277306518
+                     </acctID>
+                     <balance>
+                       0
+                     </balance>
+                     <storage>
+                       .Map
+                     </storage>
+                     <origStorage>
+                       .Map
+                     </origStorage>
+                     <transientStorage>
+                       .Map
+                     </transientStorage>
+                     <nonce>
+                       1
+                     </nonce>
+                     ...
+                   </account> )
+                 </accounts>
+                 ...
+               </network>
+             </ethereum>
+             ...
+           </kevm>
+           <stackChecks>
+             false
+           </stackChecks>
+           <cheatcodes>
+             <prank>
+               <active>
+                 false
+               </active>
+               <singleCall>
+                 false
+               </singleCall>
+               ...
+             </prank>
+             <expectedRevert>
+               <isRevertExpected>
+                 false
+               </isRevertExpected>
+               ...
+             </expectedRevert>
+             <expectedOpcode>
+               <isOpcodeExpected>
+                 false
+               </isOpcodeExpected>
+               ...
+             </expectedOpcode>
+             <expectEmit>
+               <recordEvent>
+                 false
+               </recordEvent>
+               <isEventExpected>
+                 false
+               </isEventExpected>
+               ...
+             </expectEmit>
+             <whitelist>
+               <isCallWhitelistActive>
+                 false
+               </isCallWhitelistActive>
+               <isStorageWhitelistActive>
+                 false
+               </isStorageWhitelistActive>
+               <addressList>
+                 .List
+               </addressList>
+               <storageSlotList>
+                 .List
+               </storageSlotList>
+             </whitelist>
+             <mockCalls>
+               .MockCallCellMap
+             </mockCalls>
+             <mockFunctions>
+               .MockFunctionCellMap
+             </mockFunctions>
+           </cheatcodes>
+           <KEVMTracing>
+             <activeTracing>
+               false
+             </activeTracing>
+             <traceStorage>
+               false
+             </traceStorage>
+             <traceWordStack>
+               false
+             </traceWordStack>
+             <traceMemory>
+               false
+             </traceMemory>
+             <recordedTrace>
+               false
+             </recordedTrace>
+             <traceData>
+               .List
+             </traceData>
+           </KEVMTracing>
+         </foundry>
+      requires ( 0 <=Int KV0_x:Int
+       andBool ( 200 <Int KV0_x:Int
+       andBool ( 0 <=Int CALLER_ID:Int
+       andBool ( 0 <=Int ORIGIN_ID:Int
+       andBool ( pow24 <Int NUMBER_CELL:Int
+       andBool ( NUMBER_CELL:Int <Int pow32
+       andBool ( 1073741824 <Int TIMESTAMP_CELL:Int
+       andBool ( TIMESTAMP_CELL:Int <Int 34359738368
+       andBool ( CALLER_ID:Int <Int pow160
+       andBool ( ORIGIN_ID:Int <Int pow160
+       andBool ( KV0_x:Int <Int pow256
+       andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349
+       andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349
+       andBool ( _C_FORGETBRANCHTEST_ID =/=Int 645326474426547203313410069153905908525362434349
+       andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
+       andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
+               ))))))))))))))))
+      [priority(20), label(BASIC-BLOCK-3-TO-4)]
+    
+    rule [BASIC-BLOCK-4-TO-5]: <foundry>
+           <kevm>
+             <k>
+               ( #cheatcode_return 128 0
+               ~> #pc [ CALL ] => JUMPI 1326 bool2Word ( KV0_x:Int <=Int 200 )
+               ~> #pc [ JUMPI ] )
+               ~> #execute
+               ~> _CONTINUATION
+             </k>
+             <mode>
+               NORMAL
+             </mode>
+             <schedule>
+               CANCUN
+             </schedule>
+             <useGas>
+               false
+             </useGas>
+             <ethereum>
+               <evm>
+                 <output>
+                   b""
+                 </output>
+                 <callStack>
+                   .List
+                 </callStack>
+                 <interimStates>
+                   .List
+                 </interimStates>
+                 <touchedAccounts>
+                   .Set
+                 </touchedAccounts>
+                 <callState>
+                   <id>
+                     728815563385977040452943777879061427756277306518
+                   </id>
+                   <caller>
+                     CALLER_ID:Int
+                   </caller>
+                   <callData>
+                     b"P#a\xd8" +Bytes #buf ( 32 , KV0_x:Int )
+                   </callData>
+                   <callValue>
+                     0
+                   </callValue>
+                   <wordStack>
+                     ( ( 228 => 0 ) : ( ( selector ( "forgetBranch(uint256,uint8,uint256)" ) => KV0_x:Int ) : ( ( 645326474426547203313410069153905908525362434349 => 319 ) : ( ( 0 => selector ( "test_forgetBranch(uint256)" ) ) : ( ( KV0_x:Int : ( 319 : ( selector ( "test_forgetBranch(uint256)" ) : .WordStack ) ) ) => .WordStack ) ) ) ) )
+                   </wordStack>
+                   <localMem>
+                     b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00f\x949s" +Bytes #buf ( 32 , KV0_x:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x05\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xc8"
+                   </localMem>
+                   <memoryUsed>
+                     0
+                   </memoryUsed>
+                   <callGas>
+                     0
+                   </callGas>
+                   <static>
+                     false
+                   </static>
+                   <callDepth>
+                     0
+                   </callDepth>
+                   ...
+                 </callState>
+                 <substate>
+                   <log>
+                     .List
+                   </log>
+                   <refund>
+                     0
+                   </refund>
+                   <accessedAccounts>
+                     SetItem ( 645326474426547203313410069153905908525362434349 )
+                   </accessedAccounts>
+                   <accessedStorage>
+                     .Map
+                   </accessedStorage>
+                   <createdAccounts>
+                     .Set
+                   </createdAccounts>
+                   ...
+                 </substate>
+                 <origin>
+                   ORIGIN_ID:Int
+                 </origin>
+                 <block>
+                   <number>
+                     NUMBER_CELL:Int
+                   </number>
+                   <timestamp>
+                     TIMESTAMP_CELL:Int
+                   </timestamp>
+                   ...
+                 </block>
+                 ...
+               </evm>
+               <network>
+                 <chainID>
+                   1
+                 </chainID>
+                 <accounts>
+                   ( <account>
+                     <acctID>
+                       645326474426547203313410069153905908525362434349
+                     </acctID>
+                     <balance>
+                       0
+                     </balance>
+                     <storage>
+                       .Map
+                     </storage>
+                     <origStorage>
+                       .Map
+                     </origStorage>
+                     <transientStorage>
+                       .Map
+                     </transientStorage>
+                     <nonce>
+                       0
+                     </nonce>
+                     ...
+                   </account>
+                   <account>
+                     <acctID>
+                       728815563385977040452943777879061427756277306518
+                     </acctID>
+                     <balance>
+                       0
+                     </balance>
+                     <storage>
+                       .Map
+                     </storage>
+                     <origStorage>
+                       .Map
+                     </origStorage>
+                     <transientStorage>
+                       .Map
+                     </transientStorage>
+                     <nonce>
+                       1
+                     </nonce>
+                     ...
+                   </account> )
+                 </accounts>
+                 ...
+               </network>
+             </ethereum>
+             ...
+           </kevm>
+           <stackChecks>
+             false
+           </stackChecks>
+           <cheatcodes>
+             <prank>
+               <active>
+                 false
+               </active>
+               <singleCall>
+                 false
+               </singleCall>
+               ...
+             </prank>
+             <expectedRevert>
+               <isRevertExpected>
+                 false
+               </isRevertExpected>
+               ...
+             </expectedRevert>
+             <expectedOpcode>
+               <isOpcodeExpected>
+                 false
+               </isOpcodeExpected>
+               ...
+             </expectedOpcode>
+             <expectEmit>
+               <recordEvent>
+                 false
+               </recordEvent>
+               <isEventExpected>
+                 false
+               </isEventExpected>
+               ...
+             </expectEmit>
+             <whitelist>
+               <isCallWhitelistActive>
+                 false
+               </isCallWhitelistActive>
+               <isStorageWhitelistActive>
+                 false
+               </isStorageWhitelistActive>
+               <addressList>
+                 .List
+               </addressList>
+               <storageSlotList>
+                 .List
+               </storageSlotList>
+             </whitelist>
+             <mockCalls>
+               .MockCallCellMap
+             </mockCalls>
+             <mockFunctions>
+               .MockFunctionCellMap
+             </mockFunctions>
+           </cheatcodes>
+           <KEVMTracing>
+             <activeTracing>
+               false
+             </activeTracing>
+             <traceStorage>
+               false
+             </traceStorage>
+             <traceWordStack>
+               false
+             </traceWordStack>
+             <traceMemory>
+               false
+             </traceMemory>
+             <recordedTrace>
+               false
+             </recordedTrace>
+             <traceData>
+               .List
+             </traceData>
+           </KEVMTracing>
+         </foundry>
+      requires ( 0 <=Int KV0_x:Int
+       andBool ( 0 <=Int CALLER_ID:Int
+       andBool ( 0 <=Int ORIGIN_ID:Int
+       andBool ( pow24 <Int NUMBER_CELL:Int
+       andBool ( NUMBER_CELL:Int <Int pow32
+       andBool ( 1073741824 <Int TIMESTAMP_CELL:Int
+       andBool ( TIMESTAMP_CELL:Int <Int 34359738368
+       andBool ( CALLER_ID:Int <Int pow160
+       andBool ( ORIGIN_ID:Int <Int pow160
+       andBool ( KV0_x:Int <Int pow256
+       andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349
+       andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349
+       andBool ( _C_FORGETBRANCHTEST_ID =/=Int 645326474426547203313410069153905908525362434349
+       andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
+       andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
+               )))))))))))))))
+      [priority(20), label(BASIC-BLOCK-4-TO-5)]
+    
+    rule [BASIC-BLOCK-6-TO-8]: <foundry>
+           <kevm>
+             <k>
+               ( JUMPI 1326 bool2Word ( KV0_x:Int <=Int 200 )
+               ~> #pc [ JUMPI ]
+               ~> #execute => #halt ~> .K )
+               ~> _CONTINUATION
+             </k>
+             <mode>
+               NORMAL
+             </mode>
+             <schedule>
+               CANCUN
+             </schedule>
+             <useGas>
+               false
+             </useGas>
+             <ethereum>
+               <evm>
+                 <output>
+                   b""
+                 </output>
+                 <statusCode>
+                   ( _STATUSCODE => EVMC_SUCCESS )
+                 </statusCode>
+                 <callStack>
+                   .List
+                 </callStack>
+                 <interimStates>
+                   .List
+                 </interimStates>
+                 <touchedAccounts>
+                   .Set
+                 </touchedAccounts>
+                 <callState>
+                   <id>
+                     728815563385977040452943777879061427756277306518
+                   </id>
+                   <caller>
+                     CALLER_ID:Int
+                   </caller>
+                   <callData>
+                     b"P#a\xd8" +Bytes #buf ( 32 , KV0_x:Int )
+                   </callData>
+                   <callValue>
+                     0
+                   </callValue>
+                   <wordStack>
+                     ( ( 0 => selector ( "test_forgetBranch(uint256)" ) ) : ( ( KV0_x:Int : ( 319 : ( selector ( "test_forgetBranch(uint256)" ) : .WordStack ) ) ) => .WordStack ) )
+                   </wordStack>
+                   <localMem>
+                     b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00f\x949s" +Bytes #buf ( 32 , KV0_x:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x05\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xc8"
+                   </localMem>
+                   <memoryUsed>
+                     0
+                   </memoryUsed>
+                   <callGas>
+                     0
+                   </callGas>
+                   <static>
+                     false
+                   </static>
+                   <callDepth>
+                     0
+                   </callDepth>
+                   ...
+                 </callState>
+                 <substate>
+                   <log>
+                     .List
+                   </log>
+                   <refund>
+                     0
+                   </refund>
+                   <accessedAccounts>
+                     SetItem ( 645326474426547203313410069153905908525362434349 )
+                   </accessedAccounts>
+                   <accessedStorage>
+                     .Map
+                   </accessedStorage>
+                   <createdAccounts>
+                     .Set
+                   </createdAccounts>
+                   ...
+                 </substate>
+                 <origin>
+                   ORIGIN_ID:Int
+                 </origin>
+                 <block>
+                   <number>
+                     NUMBER_CELL:Int
+                   </number>
+                   <timestamp>
+                     TIMESTAMP_CELL:Int
+                   </timestamp>
+                   ...
+                 </block>
+                 ...
+               </evm>
+               <network>
+                 <chainID>
+                   1
+                 </chainID>
+                 <accounts>
+                   ( <account>
+                     <acctID>
+                       645326474426547203313410069153905908525362434349
+                     </acctID>
+                     <balance>
+                       0
+                     </balance>
+                     <storage>
+                       .Map
+                     </storage>
+                     <origStorage>
+                       .Map
+                     </origStorage>
+                     <transientStorage>
+                       .Map
+                     </transientStorage>
+                     <nonce>
+                       0
+                     </nonce>
+                     ...
+                   </account>
+                   <account>
+                     <acctID>
+                       728815563385977040452943777879061427756277306518
+                     </acctID>
+                     <balance>
+                       0
+                     </balance>
+                     <storage>
+                       .Map
+                     </storage>
+                     <origStorage>
+                       .Map
+                     </origStorage>
+                     <transientStorage>
+                       .Map
+                     </transientStorage>
+                     <nonce>
+                       1
+                     </nonce>
+                     ...
+                   </account> )
+                 </accounts>
+                 ...
+               </network>
+             </ethereum>
+             ...
+           </kevm>
+           <stackChecks>
+             false
+           </stackChecks>
+           <cheatcodes>
+             <prank>
+               <active>
+                 false
+               </active>
+               <singleCall>
+                 false
+               </singleCall>
+               ...
+             </prank>
+             <expectedRevert>
+               <isRevertExpected>
+                 false
+               </isRevertExpected>
+               ...
+             </expectedRevert>
+             <expectedOpcode>
+               <isOpcodeExpected>
+                 false
+               </isOpcodeExpected>
+               ...
+             </expectedOpcode>
+             <expectEmit>
+               <recordEvent>
+                 false
+               </recordEvent>
+               <isEventExpected>
+                 false
+               </isEventExpected>
+               ...
+             </expectEmit>
+             <whitelist>
+               <isCallWhitelistActive>
+                 false
+               </isCallWhitelistActive>
+               <isStorageWhitelistActive>
+                 false
+               </isStorageWhitelistActive>
+               <addressList>
+                 .List
+               </addressList>
+               <storageSlotList>
+                 .List
+               </storageSlotList>
+             </whitelist>
+             <mockCalls>
+               .MockCallCellMap
+             </mockCalls>
+             <mockFunctions>
+               .MockFunctionCellMap
+             </mockFunctions>
+           </cheatcodes>
+           <KEVMTracing>
+             <activeTracing>
+               false
+             </activeTracing>
+             <traceStorage>
+               false
+             </traceStorage>
+             <traceWordStack>
+               false
+             </traceWordStack>
+             <traceMemory>
+               false
+             </traceMemory>
+             <recordedTrace>
+               false
+             </recordedTrace>
+             <traceData>
+               .List
+             </traceData>
+           </KEVMTracing>
+         </foundry>
+      requires ( 0 <=Int KV0_x:Int
+       andBool ( KV0_x:Int <=Int 200
+       andBool ( 0 <=Int CALLER_ID:Int
+       andBool ( 0 <=Int ORIGIN_ID:Int
+       andBool ( pow24 <Int NUMBER_CELL:Int
+       andBool ( NUMBER_CELL:Int <Int pow32
+       andBool ( 1073741824 <Int TIMESTAMP_CELL:Int
+       andBool ( TIMESTAMP_CELL:Int <Int 34359738368
+       andBool ( CALLER_ID:Int <Int pow160
+       andBool ( ORIGIN_ID:Int <Int pow160
+       andBool ( KV0_x:Int <Int pow256
+       andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349
+       andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349
+       andBool ( _C_FORGETBRANCHTEST_ID =/=Int 645326474426547203313410069153905908525362434349
+       andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
+       andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
+               ))))))))))))))))
+      [priority(20), label(BASIC-BLOCK-6-TO-8)]
+    
+    rule [BASIC-BLOCK-7-TO-9]: <foundry>
+           <kevm>
+             <k>
+               ( JUMPI 1326 bool2Word ( KV0_x:Int <=Int 200 )
+               ~> #pc [ JUMPI ]
+               ~> #execute => #halt ~> .K )
+               ~> _CONTINUATION
+             </k>
+             <mode>
+               NORMAL
+             </mode>
+             <schedule>
+               CANCUN
+             </schedule>
+             <useGas>
+               false
+             </useGas>
+             <ethereum>
+               <evm>
+                 <output>
+                   b""
+                 </output>
+                 <statusCode>
+                   ( _STATUSCODE => EVMC_SUCCESS )
+                 </statusCode>
+                 <callStack>
+                   .List
+                 </callStack>
+                 <interimStates>
+                   .List
+                 </interimStates>
+                 <touchedAccounts>
+                   .Set
+                 </touchedAccounts>
+                 <callState>
+                   <id>
+                     728815563385977040452943777879061427756277306518
+                   </id>
+                   <caller>
+                     CALLER_ID:Int
+                   </caller>
+                   <callData>
+                     b"P#a\xd8" +Bytes #buf ( 32 , KV0_x:Int )
+                   </callData>
+                   <callValue>
+                     0
+                   </callValue>
+                   <wordStack>
+                     ( ( 0 => selector ( "test_forgetBranch(uint256)" ) ) : ( ( KV0_x:Int : ( 319 : ( selector ( "test_forgetBranch(uint256)" ) : .WordStack ) ) ) => .WordStack ) )
+                   </wordStack>
+                   <localMem>
+                     b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00f\x949s" +Bytes #buf ( 32 , KV0_x:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x05\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xc8"
+                   </localMem>
+                   <memoryUsed>
+                     0
+                   </memoryUsed>
+                   <callGas>
+                     0
+                   </callGas>
+                   <static>
+                     false
+                   </static>
+                   <callDepth>
+                     0
+                   </callDepth>
+                   ...
+                 </callState>
+                 <substate>
+                   <log>
+                     .List
+                   </log>
+                   <refund>
+                     0
+                   </refund>
+                   <accessedAccounts>
+                     SetItem ( 645326474426547203313410069153905908525362434349 )
+                   </accessedAccounts>
+                   <accessedStorage>
+                     .Map
+                   </accessedStorage>
+                   <createdAccounts>
+                     .Set
+                   </createdAccounts>
+                   ...
+                 </substate>
+                 <origin>
+                   ORIGIN_ID:Int
+                 </origin>
+                 <block>
+                   <number>
+                     NUMBER_CELL:Int
+                   </number>
+                   <timestamp>
+                     TIMESTAMP_CELL:Int
+                   </timestamp>
+                   ...
+                 </block>
+                 ...
+               </evm>
+               <network>
+                 <chainID>
+                   1
+                 </chainID>
+                 <accounts>
+                   ( <account>
+                     <acctID>
+                       645326474426547203313410069153905908525362434349
+                     </acctID>
+                     <balance>
+                       0
+                     </balance>
+                     <storage>
+                       .Map
+                     </storage>
+                     <origStorage>
+                       .Map
+                     </origStorage>
+                     <transientStorage>
+                       .Map
+                     </transientStorage>
+                     <nonce>
+                       0
+                     </nonce>
+                     ...
+                   </account>
+                   <account>
+                     <acctID>
+                       728815563385977040452943777879061427756277306518
+                     </acctID>
+                     <balance>
+                       0
+                     </balance>
+                     <storage>
+                       .Map
+                     </storage>
+                     <origStorage>
+                       .Map
+                     </origStorage>
+                     <transientStorage>
+                       .Map
+                     </transientStorage>
+                     <nonce>
+                       1
+                     </nonce>
+                     ...
+                   </account> )
+                 </accounts>
+                 ...
+               </network>
+             </ethereum>
+             ...
+           </kevm>
+           <stackChecks>
+             false
+           </stackChecks>
+           <cheatcodes>
+             <prank>
+               <active>
+                 false
+               </active>
+               <singleCall>
+                 false
+               </singleCall>
+               ...
+             </prank>
+             <expectedRevert>
+               <isRevertExpected>
+                 false
+               </isRevertExpected>
+               ...
+             </expectedRevert>
+             <expectedOpcode>
+               <isOpcodeExpected>
+                 false
+               </isOpcodeExpected>
+               ...
+             </expectedOpcode>
+             <expectEmit>
+               <recordEvent>
+                 false
+               </recordEvent>
+               <isEventExpected>
+                 false
+               </isEventExpected>
+               ...
+             </expectEmit>
+             <whitelist>
+               <isCallWhitelistActive>
+                 false
+               </isCallWhitelistActive>
+               <isStorageWhitelistActive>
+                 false
+               </isStorageWhitelistActive>
+               <addressList>
+                 .List
+               </addressList>
+               <storageSlotList>
+                 .List
+               </storageSlotList>
+             </whitelist>
+             <mockCalls>
+               .MockCallCellMap
+             </mockCalls>
+             <mockFunctions>
+               .MockFunctionCellMap
+             </mockFunctions>
+           </cheatcodes>
+           <KEVMTracing>
+             <activeTracing>
+               false
+             </activeTracing>
+             <traceStorage>
+               false
+             </traceStorage>
+             <traceWordStack>
+               false
+             </traceWordStack>
+             <traceMemory>
+               false
+             </traceMemory>
+             <recordedTrace>
+               false
+             </recordedTrace>
+             <traceData>
+               .List
+             </traceData>
+           </KEVMTracing>
+         </foundry>
+      requires ( 0 <=Int KV0_x:Int
+       andBool ( 200 <Int KV0_x:Int
+       andBool ( 0 <=Int CALLER_ID:Int
+       andBool ( 0 <=Int ORIGIN_ID:Int
+       andBool ( pow24 <Int NUMBER_CELL:Int
+       andBool ( NUMBER_CELL:Int <Int pow32
+       andBool ( 1073741824 <Int TIMESTAMP_CELL:Int
+       andBool ( TIMESTAMP_CELL:Int <Int 34359738368
+       andBool ( CALLER_ID:Int <Int pow160
+       andBool ( ORIGIN_ID:Int <Int pow160
+       andBool ( KV0_x:Int <Int pow256
+       andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349
+       andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349
+       andBool ( _C_FORGETBRANCHTEST_ID =/=Int 645326474426547203313410069153905908525362434349
+       andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
+       andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
+               ))))))))))))))))
+      [priority(20), label(BASIC-BLOCK-7-TO-9)]
+
+endmodule
+0 Failure nodes. (0 pending and 0 failing)
+
+Join the Runtime Verification Discord server (https://discord.com/invite/CurfmXNtbN) or Telegram group (https://t.me/rv_kontrol) for support.
+
+See `foundry_success` predicate for more information:
+https://github.com/runtimeverification/kontrol/blob/master/src/kontrol/kdist/foundry.md#foundry-success-predicate
+
+Access documentation for Kontrol at https://docs.runtimeverification.com/kontrol
\ No newline at end of file
diff --git a/src/tests/integration/test-data/src/ForgetBranch.t.sol b/src/tests/integration/test-data/src/ForgetBranch.t.sol
new file mode 100644
index 000000000..fe4064aa8
--- /dev/null
+++ b/src/tests/integration/test-data/src/ForgetBranch.t.sol
@@ -0,0 +1,21 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity >=0.8.13;
+
+import {Test, console} from "forge-std/Test.sol";
+import "kontrol-cheatcodes/KontrolCheats.sol";
+
+
+contract ForgetBranchTest is Test, KontrolCheats {
+
+    function test_forgetBranch(uint256 x) public {
+        uint256 y;
+
+        vm.assume(x > 200);
+        kevm.forgetBranch(x, KontrolCheatsBase.ComparisonOperator.GreaterThan, 200);
+        if(x > 200){
+            y = 21;
+        } else {
+            y = 42;
+        }
+    }
+}
\ No newline at end of file