From ce79c6c9fa83e7e9abac67e41459bc888032fa80 Mon Sep 17 00:00:00 2001
From: Andrei <16517508+anvacaru@users.noreply.github.com>
Date: Tue, 3 Dec 2024 11:55:47 +0200
Subject: [PATCH 01/17] draft FOUNDRYSemantics

---
 src/kontrol/foundry.py          | 87 +++++++++++++++++++++++++++++----
 src/kontrol/kdist/cheatcodes.md | 21 ++++++++
 src/kontrol/kdist/foundry.md    |  4 ++
 src/kontrol/prove.py            | 14 ++++--
 4 files changed, 111 insertions(+), 15 deletions(-)

diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py
index a690ea6fd..3c37df2a8 100644
--- a/src/kontrol/foundry.py
+++ b/src/kontrol/foundry.py
@@ -17,13 +17,22 @@
 from typing import TYPE_CHECKING
 
 import tomlkit
-from kevm_pyk.kevm import KEVM, KEVMNodePrinter, KEVMSemantics
+from kevm_pyk.kevm import KEVM, KEVMNodePrinter, KEVMSemantics, compute_jumpdests
 from kevm_pyk.utils import byte_offset_to_lines, legacy_explore, print_failure_info, print_model
 from pyk.cterm import CTerm
-from pyk.kast.inner import KApply, KInner, KSort, KToken, KVariable
-from pyk.kast.manip import cell_label_to_var_name, collect, extract_lhs, flatten_label, minimize_term, top_down
+from pyk.kast.inner import KApply, KInner, KSequence, KSort, KToken, KVariable
+from pyk.kast.manip import (
+    cell_label_to_var_name,
+    collect,
+    extract_lhs,
+    flatten_label,
+    minimize_term,
+    set_cell,
+    top_down,
+)
 from pyk.kast.outer import KDefinition, KFlatModule, KImport, KRequire
 from pyk.kcfg import KCFG
+from pyk.kcfg.kcfg import Step
 from pyk.kcfg.minimize import KCFGMinimizer
 from pyk.prelude.bytes import bytesToken
 from pyk.prelude.collections import map_empty
@@ -57,6 +66,7 @@
 
     from pyk.kast.outer import KAst
     from pyk.kcfg.kcfg import NodeIdLike
+    from pyk.kcfg.semantics import KCFGExtendResult
     from pyk.kcfg.tui import KCFGElem
     from pyk.proof.implies import RefutationProof
     from pyk.proof.show import NodePrinter
@@ -82,6 +92,63 @@
 _LOGGER: Final = logging.getLogger(__name__)
 
 
+class FOUNDRYSemantics(KEVMSemantics):
+    def _check_load_pattern(self, cterm: CTerm) -> bool:
+        """Given a CTerm, check if the rule 'EVM.program.load' is at the top of the K_CELL.
+
+        This method checks if the `EVM.program.load` 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.
+        """
+        load_pattern = KSequence([KApply('loadProgram', KVariable('###BYTECODE')), KVariable('###CONTINUATION')])
+        self._cached_subst = load_pattern.match(cterm.cell('K_CELL'))
+        return self._cached_subst is not None
+
+    def _check_abstract_pattern(self, cterm: CTerm) -> bool:
+        """Given a CTerm, check if the rule 'FOUNDRY.abstract' is at the top of the K_CELL.
+
+        This method checks if the `FOUNDRY.abstract` 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_abstract', [KVariable('###CONDITION1'), KVariable('###CONDITION2')]),
+                KVariable('###CONTINUATION'),
+            ]
+        )
+        self._cached_subst = abstract_pattern.match(cterm.cell('K_CELL'))
+        print('CHECKING ABSTRACT PATTERN')
+        return self._cached_subst is not None
+
+    def custom_step(self, cterm: CTerm) -> KCFGExtendResult | None:
+        """Given a CTerm, update the JUMPDESTS_CELL and PROGRAM_CELL if the rule 'EVM.program.load' is at the top of the K_CELL.
+
+        :param cterm: CTerm of a proof node.
+        :return: If the K_CELL matches the load_pattern, a Step with depth 1 is returned together with the new configuration, also registering that the `EVM.program.load` rule has been applied. Otherwise, None is returned.
+        """
+        if self._check_load_pattern(cterm):
+            subst = self._cached_subst
+            assert subst is not None
+            bytecode_sections = flatten_label('_+Bytes__BYTES-HOOKED_Bytes_Bytes_Bytes', subst['###BYTECODE'])
+            jumpdests_set = compute_jumpdests(bytecode_sections)
+            new_cterm = CTerm.from_kast(set_cell(cterm.kast, 'JUMPDESTS_CELL', jumpdests_set))
+            new_cterm = CTerm.from_kast(set_cell(new_cterm.kast, 'PROGRAM_CELL', subst['###BYTECODE']))
+            new_cterm = CTerm.from_kast(set_cell(new_cterm.kast, 'K_CELL', KSequence(subst['###CONTINUATION'])))
+            return Step(new_cterm, 1, (), ['EVM.program.load'], cut=True)
+        elif self._check_abstract_pattern(cterm):
+            print('ABSTRACT PATTERN CONFIRMED')
+            subst = self._cached_subst
+            assert subst is not None
+            fst_condition = subst['###CONDITION1']
+            snd_condition = subst['###CONDITION2']
+            print('fst', fst_condition)
+            print('snd', snd_condition)
+        return None
+
+
 class FoundryKEVM(KEVM):
     foundry: Foundry
 
@@ -841,7 +908,7 @@ def foundry_show(
     if options.failure_info:
         with legacy_explore(
             foundry.kevm,
-            kcfg_semantics=KEVMSemantics(),
+            kcfg_semantics=FOUNDRYSemantics(),
             id=test_id,
             smt_timeout=options.smt_timeout,
             smt_retry_limit=options.smt_retry_limit,
@@ -908,7 +975,7 @@ def _collect_klabel(_k: KInner) -> None:
         ]
         sentences = [sent for sent in sentences if not _contains_foundry_klabel(sent.body)]
         sentences = [
-            sent for sent in sentences if not KEVMSemantics().is_terminal(CTerm.from_kast(extract_lhs(sent.body)))
+            sent for sent in sentences if not FOUNDRYSemantics().is_terminal(CTerm.from_kast(extract_lhs(sent.body)))
         ]
         if len(sentences) == 0:
             _LOGGER.warning(f'No claims or rules retained for proof {proof.id}')
@@ -1098,7 +1165,7 @@ def foundry_simplify_node(
 
     with legacy_explore(
         foundry.kevm,
-        kcfg_semantics=KEVMSemantics(),
+        kcfg_semantics=FOUNDRYSemantics(),
         id=apr_proof.id,
         bug_report=options.bug_report,
         kore_rpc_command=kore_rpc_command,
@@ -1146,7 +1213,7 @@ def check_cells_equal(cell: str, nodes: Iterable[KCFG.Node]) -> bool:
     check_cells_ne = [check_cell for check_cell in check_cells if not check_cells_equal(check_cell, nodes)]
 
     if check_cells_ne:
-        if not all(KEVMSemantics().same_loop(nodes[0].cterm, nd.cterm) for nd in nodes):
+        if not all(FOUNDRYSemantics().same_loop(nodes[0].cterm, nd.cterm) for nd in nodes):
             raise ValueError(f'Nodes {options.nodes} cannot be merged because they differ in: {check_cells_ne}')
 
     anti_unification = nodes[0].cterm
@@ -1186,7 +1253,7 @@ def foundry_step_node(
 
     with legacy_explore(
         foundry.kevm,
-        kcfg_semantics=KEVMSemantics(),
+        kcfg_semantics=FOUNDRYSemantics(),
         id=apr_proof.id,
         bug_report=options.bug_report,
         kore_rpc_command=kore_rpc_command,
@@ -1262,7 +1329,7 @@ def foundry_section_edge(
 
     with legacy_explore(
         foundry.kevm,
-        kcfg_semantics=KEVMSemantics(),
+        kcfg_semantics=FOUNDRYSemantics(),
         id=apr_proof.id,
         bug_report=options.bug_report,
         kore_rpc_command=kore_rpc_command,
@@ -1313,7 +1380,7 @@ def foundry_get_model(
 
     with legacy_explore(
         foundry.kevm,
-        kcfg_semantics=KEVMSemantics(),
+        kcfg_semantics=FOUNDRYSemantics(),
         id=proof.id,
         bug_report=options.bug_report,
         kore_rpc_command=kore_rpc_command,
diff --git a/src/kontrol/kdist/cheatcodes.md b/src/kontrol/kdist/cheatcodes.md
index 35892fc00..6ce0672f8 100644
--- a/src/kontrol/kdist/cheatcodes.md
+++ b/src/kontrol/kdist/cheatcodes.md
@@ -1106,6 +1106,25 @@ Mock functions
       [priority(30)]
 ```
 
+
+Abstraction functions
+---------------------
+
+#### `abstract` - replaces the first condition in the current constraints with the second one provided.
+
+```
+    function abstract(bool cond1, bool cond2) external;
+```
+
+```k
+    rule [cheatcode.call.abstract]:
+         <k> #cheatcode_call SELECTOR ARGS
+          => #abstract ( #range(ARGS,0,32), #range(ARGS,32,32))
+          ...
+         </k>
+      requires SELECTOR ==Int selector ( "replace_constraint(bool,bool)" )
+```
+
 Utils
 -----
 
@@ -1691,6 +1710,8 @@ 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 ( "replace_constraint(bool,bool)" )            => 1408652492 )
+    rule ( selector ( "forget(bool)" )                             => 589442177  )
 ```
 
 Selectors for **unimplemented** cheat code functions.
diff --git a/src/kontrol/kdist/foundry.md b/src/kontrol/kdist/foundry.md
index 2ac8861a7..740eb6a34 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 ::= #abstract ( Bytes , Bytes ) [symbol(cheatcode_abstract)]
+ // -----------------------------------------------------------------------
+    rule [abstract]: <k> #abstract(_C1, _C2) => .K ... </k>
 ```
 
 #### Structure of execution
diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py
index 3f0446730..109ab4774 100644
--- a/src/kontrol/prove.py
+++ b/src/kontrol/prove.py
@@ -11,7 +11,7 @@
 from typing import TYPE_CHECKING, Any, ContextManager, NamedTuple
 
 from kevm_pyk.cli import EVMChainOptions
-from kevm_pyk.kevm import KEVM, KEVMSemantics, _process_jumpdests
+from kevm_pyk.kevm import KEVM, _process_jumpdests
 from kevm_pyk.utils import KDefinition__expand_macros, abstract_cell_vars, run_prover
 from multiprocess.pool import Pool  # type: ignore
 from pyk.cterm import CTerm, CTermSymbolic
@@ -35,7 +35,7 @@
 from pyk.utils import hash_str, run_process_2, single, unique
 from rich.progress import Progress, SpinnerColumn, TaskID, TextColumn, TimeElapsedColumn
 
-from .foundry import Foundry, foundry_to_xml
+from .foundry import Foundry, FOUNDRYSemantics, foundry_to_xml
 from .hevm import Hevm
 from .options import ConfigType, TraceOptions
 from .solc_to_k import Contract, hex_string_to_int
@@ -381,7 +381,7 @@ def create_kcfg_explore() -> KCFGExplore:
                 )
                 return KCFGExplore(
                     cterm_symbolic,
-                    kcfg_semantics=KEVMSemantics(auto_abstract_gas=options.auto_abstract_gas),
+                    kcfg_semantics=FOUNDRYSemantics(auto_abstract_gas=options.auto_abstract_gas),
                     id=test.id,
                 )
 
@@ -425,7 +425,7 @@ def create_kcfg_explore() -> KCFGExplore:
                         }
                     ),
                 )
-            cut_point_rules = KEVMSemantics.cut_point_rules(
+            cut_point_rules = FOUNDRYSemantics.cut_point_rules(
                 options.break_on_jumpi,
                 options.break_on_jump,
                 options.break_on_calls,
@@ -441,6 +441,10 @@ def create_kcfg_explore() -> KCFGExplore:
                     rule.label for rule in foundry.kevm.definition.all_modules_dict['KONTROL-ASSERTIONS'].rules
                 )
 
+            cut_point_rules.append('FOUNDRY-ACCOUNTS.abstract')
+            print('CUT POINT RULES')
+            print(cut_point_rules)
+
             extra_lemmas_module: KFlatModule | None = None
             if options.extra_module:
                 extra_module_file, extra_module_name, *_ = options.extra_module.split(':')
@@ -465,7 +469,7 @@ def create_kcfg_explore() -> KCFGExplore:
                 max_depth=options.max_depth,
                 max_iterations=options.max_iterations,
                 cut_point_rules=cut_point_rules,
-                terminal_rules=KEVMSemantics.terminal_rules(options.break_every_step),
+                terminal_rules=FOUNDRYSemantics.terminal_rules(options.break_every_step),
                 counterexample_info=options.counterexample_info,
                 max_frontier_parallel=options.max_frontier_parallel,
                 fail_fast=options.fail_fast,

From d2c69f40cd4c38dc5eada05ef01ad2755fa990ac Mon Sep 17 00:00:00 2001
From: Andrei <16517508+anvacaru@users.noreply.github.com>
Date: Tue, 3 Dec 2024 14:06:56 +0200
Subject: [PATCH 02/17] forgetBranch

---
 src/kontrol/foundry.py          | 35 ++++++++++++++++++++++-----------
 src/kontrol/kdist/cheatcodes.md | 13 ++++++------
 src/kontrol/kdist/foundry.md    |  4 ++--
 src/kontrol/prove.py            |  2 +-
 4 files changed, 34 insertions(+), 20 deletions(-)

diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py
index 3c37df2a8..9bbaff38c 100644
--- a/src/kontrol/foundry.py
+++ b/src/kontrol/foundry.py
@@ -105,22 +105,22 @@ def _check_load_pattern(self, cterm: CTerm) -> bool:
         self._cached_subst = load_pattern.match(cterm.cell('K_CELL'))
         return self._cached_subst is not None
 
-    def _check_abstract_pattern(self, cterm: CTerm) -> bool:
-        """Given a CTerm, check if the rule 'FOUNDRY.abstract' is at the top of the K_CELL.
+    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.abstract` rule is at the top of the `K_CELL` in the given `cterm`.
+        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_abstract', [KVariable('###CONDITION1'), KVariable('###CONDITION2')]),
+                KApply('cheatcode_forget', [KVariable('###TERM1'), KVariable('###OPERATOR'), KVariable('###TERM2')]),
                 KVariable('###CONTINUATION'),
             ]
         )
         self._cached_subst = abstract_pattern.match(cterm.cell('K_CELL'))
-        print('CHECKING ABSTRACT PATTERN')
+        print('CHECKING FORGET PATTERN')
         return self._cached_subst is not None
 
     def custom_step(self, cterm: CTerm) -> KCFGExtendResult | None:
@@ -138,14 +138,27 @@ def custom_step(self, cterm: CTerm) -> KCFGExtendResult | None:
             new_cterm = CTerm.from_kast(set_cell(new_cterm.kast, 'PROGRAM_CELL', subst['###BYTECODE']))
             new_cterm = CTerm.from_kast(set_cell(new_cterm.kast, 'K_CELL', KSequence(subst['###CONTINUATION'])))
             return Step(new_cterm, 1, (), ['EVM.program.load'], cut=True)
-        elif self._check_abstract_pattern(cterm):
-            print('ABSTRACT PATTERN CONFIRMED')
+
+        elif self._check_forget_pattern(cterm):
+            _operators = ['_==Int_','_!=Int_', '_<=Int_', '_<Int_', '_>=Int_', '_>Int_']
+            print('FORGET PATTERN CONFIRMED')
             subst = self._cached_subst
             assert subst is not None
-            fst_condition = subst['###CONDITION1']
-            snd_condition = subst['###CONDITION2']
-            print('fst', fst_condition)
-            print('snd', snd_condition)
+            fst_term = subst['###TERM1']
+            snd_term = subst['###TERM2']
+            operator = subst['###OPERATOR']
+            print('fst', fst_term)
+            print('snd', snd_term)
+            print('operator', operator)
+            assert type(operator) is KToken
+            eq = KApply(_operators[int(operator.token)],fst_term, snd_term)
+            print('kapply',eq)
+            print('cterms', cterm.constraints)
+            print(eq in cterm.constraints)
+            new_cterm = CTerm.from_kast(set_cell(cterm.kast, 'K_CELL', KSequence(subst['###CONTINUATION'])))
+            new_constraints = ( c for c in cterm.constraints if c is not eq )
+            return Step(CTerm(new_cterm.config, new_constraints), 1, (), ['cheatcode_forget'], cut=True)
+
         return None
 
 
diff --git a/src/kontrol/kdist/cheatcodes.md b/src/kontrol/kdist/cheatcodes.md
index 6ce0672f8..9259dda7a 100644
--- a/src/kontrol/kdist/cheatcodes.md
+++ b/src/kontrol/kdist/cheatcodes.md
@@ -1110,19 +1110,20 @@ Mock functions
 Abstraction functions
 ---------------------
 
-#### `abstract` - replaces the first condition in the current constraints with the second one provided.
+#### `forgetBranch` - removes a given path constraint.
 
 ```
-    function abstract(bool cond1, bool cond2) external;
+    function forgetBranch(uint256 op1, ComparisonOperator op, uint256 op2) external;
 ```
 
 ```k
     rule [cheatcode.call.abstract]:
          <k> #cheatcode_call SELECTOR ARGS
-          => #abstract ( #range(ARGS,0,32), #range(ARGS,32,32))
+          => #forget ( #asWord(#range(ARGS,0,32)), #asWord(#range(ARGS,32,32)), #asWord(#range(ARGS,64,32)))
           ...
          </k>
-      requires SELECTOR ==Int selector ( "replace_constraint(bool,bool)" )
+      requires SELECTOR ==Int selector ( "forgetBranch(uint256,uint8,uint256)" )
+
 ```
 
 Utils
@@ -1710,8 +1711,8 @@ 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 ( "replace_constraint(bool,bool)" )            => 1408652492 )
-    rule ( selector ( "forget(bool)" )                             => 589442177  )
+    rule ( selector ( "replaceConstraint(uint256,uint8,uint256,bool)" ) => 1408652492 )
+    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 740eb6a34..871f0dd18 100644
--- a/src/kontrol/kdist/foundry.md
+++ b/src/kontrol/kdist/foundry.md
@@ -79,9 +79,9 @@ Then, we define helpers in K which can:
              ...
            </account>
 
-    syntax KItem ::= #abstract ( Bytes , Bytes ) [symbol(cheatcode_abstract)]
+    syntax KItem ::= #forget ( Int , Int , Int ) [symbol(cheatcode_forget)]
  // -----------------------------------------------------------------------
-    rule [abstract]: <k> #abstract(_C1, _C2) => .K ... </k>
+    rule [forget]: <k> #forget(_C1,_OP,_C2) => .K ... </k>
 ```
 
 #### Structure of execution
diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py
index 109ab4774..bf4708efe 100644
--- a/src/kontrol/prove.py
+++ b/src/kontrol/prove.py
@@ -441,7 +441,7 @@ def create_kcfg_explore() -> KCFGExplore:
                     rule.label for rule in foundry.kevm.definition.all_modules_dict['KONTROL-ASSERTIONS'].rules
                 )
 
-            cut_point_rules.append('FOUNDRY-ACCOUNTS.abstract')
+            cut_point_rules.append('FOUNDRY-ACCOUNTS.forget')
             print('CUT POINT RULES')
             print(cut_point_rules)
 

From 5784068d8dd2ecc8920169d13eba3267bd7483a6 Mon Sep 17 00:00:00 2001
From: Andrei <16517508+anvacaru@users.noreply.github.com>
Date: Tue, 3 Dec 2024 14:12:15 +0200
Subject: [PATCH 03/17] add mlEqualsTrue

---
 src/kontrol/foundry.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py
index 9bbaff38c..6a5cf1413 100644
--- a/src/kontrol/foundry.py
+++ b/src/kontrol/foundry.py
@@ -151,7 +151,7 @@ def custom_step(self, cterm: CTerm) -> KCFGExtendResult | None:
             print('snd', snd_term)
             print('operator', operator)
             assert type(operator) is KToken
-            eq = KApply(_operators[int(operator.token)],fst_term, snd_term)
+            eq = mlEqualsTrue( KApply(_operators[int(operator.token)],fst_term, snd_term))
             print('kapply',eq)
             print('cterms', cterm.constraints)
             print(eq in cterm.constraints)

From 190c61d1c9eb890d431ed4ce64a6d31eb30ff544 Mon Sep 17 00:00:00 2001
From: Petar Maksimovic <petar.maksimovic@runtimeverification.com>
Date: Tue, 3 Dec 2024 15:36:32 +0000
Subject: [PATCH 04/17] minor corrections

---
 src/kontrol/foundry.py                        | 21 ++++++++++---------
 .../test-data/foundry/test/ForgetBranch.t.sol | 20 ++++++++++++++++++
 2 files changed, 31 insertions(+), 10 deletions(-)
 create mode 100644 src/tests/integration/test-data/foundry/test/ForgetBranch.t.sol

diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py
index 6a5cf1413..d61650fa1 100644
--- a/src/kontrol/foundry.py
+++ b/src/kontrol/foundry.py
@@ -140,23 +140,24 @@ def custom_step(self, cterm: CTerm) -> KCFGExtendResult | None:
             return Step(new_cterm, 1, (), ['EVM.program.load'], cut=True)
 
         elif self._check_forget_pattern(cterm):
-            _operators = ['_==Int_','_!=Int_', '_<=Int_', '_<Int_', '_>=Int_', '_>Int_']
-            print('FORGET PATTERN CONFIRMED')
+            _operators = ['_==Int_', '_<=Int_', '_<Int_', '_>=Int_', '_>Int_']
+            print('Custom step: Forget pattern confirmed')
             subst = self._cached_subst
             assert subst is not None
             fst_term = subst['###TERM1']
             snd_term = subst['###TERM2']
             operator = subst['###OPERATOR']
-            print('fst', fst_term)
-            print('snd', snd_term)
-            print('operator', operator)
+            print('LHS:', fst_term)
+            print('Operator:', operator)
+            print('RHS:', snd_term)
             assert type(operator) is KToken
-            eq = mlEqualsTrue( KApply(_operators[int(operator.token)],fst_term, snd_term))
-            print('kapply',eq)
-            print('cterms', cterm.constraints)
-            print(eq in cterm.constraints)
+            eq = mlEqualsTrue(KApply(_operators[int(operator.token)], fst_term, snd_term))
+            print('Constraint to forget:', eq)
+            print(f'Current constraints:\n{cterm.constraints}')
+            print(f'Constraint to forget found: {eq in cterm.constraints}')
             new_cterm = CTerm.from_kast(set_cell(cterm.kast, 'K_CELL', KSequence(subst['###CONTINUATION'])))
-            new_constraints = ( c for c in cterm.constraints if c is not eq )
+            new_constraints: tuple[KInner, ...] = tuple(c for c in cterm.constraints if c != eq)
+            print(f'New constraints:\n{new_constraints}')
             return Step(CTerm(new_cterm.config, new_constraints), 1, (), ['cheatcode_forget'], cut=True)
 
         return None
diff --git a/src/tests/integration/test-data/foundry/test/ForgetBranch.t.sol b/src/tests/integration/test-data/foundry/test/ForgetBranch.t.sol
new file mode 100644
index 000000000..53ac90f3e
--- /dev/null
+++ b/src/tests/integration/test-data/foundry/test/ForgetBranch.t.sol
@@ -0,0 +1,20 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity >=0.8.13;
+
+import "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(200, 2, x);
+        if(x > 200){
+            y = 21;
+        } else {
+            y = 42;
+        }
+    }
+}
\ No newline at end of file

From adb8a704a9f8127b55c8c494abfe6603aa937fcf Mon Sep 17 00:00:00 2001
From: Andrei <16517508+anvacaru@users.noreply.github.com>
Date: Wed, 4 Dec 2024 14:43:50 +0200
Subject: [PATCH 05/17] add simplification step

---
 src/kontrol/foundry.py | 82 ++++++++++++++++++------------------------
 1 file changed, 34 insertions(+), 48 deletions(-)

diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py
index d61650fa1..abc67251d 100644
--- a/src/kontrol/foundry.py
+++ b/src/kontrol/foundry.py
@@ -17,7 +17,7 @@
 from typing import TYPE_CHECKING
 
 import tomlkit
-from kevm_pyk.kevm import KEVM, KEVMNodePrinter, KEVMSemantics, compute_jumpdests
+from kevm_pyk.kevm import KEVM, KEVMNodePrinter, KEVMSemantics
 from kevm_pyk.utils import byte_offset_to_lines, legacy_explore, print_failure_info, print_model
 from pyk.cterm import CTerm
 from pyk.kast.inner import KApply, KInner, KSequence, KSort, KToken, KVariable
@@ -34,9 +34,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
@@ -64,6 +65,7 @@
     from collections.abc import Iterable
     from typing import Any, Final
 
+    from pyk.cterm import CTermSymbolic
     from pyk.kast.outer import KAst
     from pyk.kcfg.kcfg import NodeIdLike
     from pyk.kcfg.semantics import KCFGExtendResult
@@ -93,17 +95,6 @@
 
 
 class FOUNDRYSemantics(KEVMSemantics):
-    def _check_load_pattern(self, cterm: CTerm) -> bool:
-        """Given a CTerm, check if the rule 'EVM.program.load' is at the top of the K_CELL.
-
-        This method checks if the `EVM.program.load` 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.
-        """
-        load_pattern = KSequence([KApply('loadProgram', KVariable('###BYTECODE')), KVariable('###CONTINUATION')])
-        self._cached_subst = load_pattern.match(cterm.cell('K_CELL'))
-        return self._cached_subst is not 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.
@@ -120,47 +111,42 @@ def _check_forget_pattern(self, cterm: CTerm) -> bool:
             ]
         )
         self._cached_subst = abstract_pattern.match(cterm.cell('K_CELL'))
-        print('CHECKING FORGET PATTERN')
         return self._cached_subst is not None
 
-    def custom_step(self, cterm: CTerm) -> KCFGExtendResult | None:
-        """Given a CTerm, update the JUMPDESTS_CELL and PROGRAM_CELL if the rule 'EVM.program.load' is at the top of the K_CELL.
+    def _exec_forget_custom_step(self, cterm: CTerm, cterm_symbolic: CTermSymbolic) -> KCFGExtendResult:
+        """Given a CTerm, remove the constraint that's placed at the top of the K_CELL in the 'FOUNDRY-ACCOUNTS.forget' cut-rule.
 
         :param cterm: CTerm of a proof node.
-        :return: If the K_CELL matches the load_pattern, a Step with depth 1 is returned together with the new configuration, also registering that the `EVM.program.load` rule has been applied. Otherwise, None is returned.
+        :cterm_symbolic: CTermSymbolic instance
+        :return: If the K_CELL matches the forget_pattern, a Step with depth 1 is returned together with the new configuration, also registering that the `FOUNDRY-ACCOUNTS.forget` rule has been applied.
         """
-        if self._check_load_pattern(cterm):
-            subst = self._cached_subst
-            assert subst is not None
-            bytecode_sections = flatten_label('_+Bytes__BYTES-HOOKED_Bytes_Bytes_Bytes', subst['###BYTECODE'])
-            jumpdests_set = compute_jumpdests(bytecode_sections)
-            new_cterm = CTerm.from_kast(set_cell(cterm.kast, 'JUMPDESTS_CELL', jumpdests_set))
-            new_cterm = CTerm.from_kast(set_cell(new_cterm.kast, 'PROGRAM_CELL', subst['###BYTECODE']))
-            new_cterm = CTerm.from_kast(set_cell(new_cterm.kast, 'K_CELL', KSequence(subst['###CONTINUATION'])))
-            return Step(new_cterm, 1, (), ['EVM.program.load'], cut=True)
-
-        elif self._check_forget_pattern(cterm):
-            _operators = ['_==Int_', '_<=Int_', '_<Int_', '_>=Int_', '_>Int_']
-            print('Custom step: Forget pattern confirmed')
-            subst = self._cached_subst
-            assert subst is not None
-            fst_term = subst['###TERM1']
-            snd_term = subst['###TERM2']
-            operator = subst['###OPERATOR']
-            print('LHS:', fst_term)
-            print('Operator:', operator)
-            print('RHS:', snd_term)
-            assert type(operator) is KToken
-            eq = mlEqualsTrue(KApply(_operators[int(operator.token)], fst_term, snd_term))
-            print('Constraint to forget:', eq)
-            print(f'Current constraints:\n{cterm.constraints}')
-            print(f'Constraint to forget found: {eq in cterm.constraints}')
-            new_cterm = CTerm.from_kast(set_cell(cterm.kast, 'K_CELL', KSequence(subst['###CONTINUATION'])))
-            new_constraints: tuple[KInner, ...] = tuple(c for c in cterm.constraints if c != eq)
-            print(f'New constraints:\n{new_constraints}')
-            return Step(CTerm(new_cterm.config, new_constraints), 1, (), ['cheatcode_forget'], cut=True)
+        _operators = ['_==Int_', '_<=Int_', '_<Int_', '_>=Int_', '_>Int_']
+        _LOGGER.info('Custom step: Forget pattern confirmed')
+        subst = self._cached_subst
+        assert subst is not None
+        fst_term = subst['###TERM1']
+        snd_term = subst['###TERM2']
+        operator = subst['###OPERATOR']
+        assert type(operator) is KToken
+        eq = mlEqualsTrue(KApply(_operators[int(operator.token)], fst_term, snd_term))
+        kevm = KEVM(kdist.get('kontrol.foundry'))
+        empty_config = kevm.definition.empty_config(GENERATED_TOP_CELL)
+        simplification_cterm = CTerm.from_kast(empty_config).add_constraint(eq)
+        result_cterm, _ = cterm_symbolic.simplify(simplification_cterm)
+        target_constraint = single(result_cterm.constraints)
+        new_cterm = CTerm.from_kast(set_cell(cterm.kast, 'K_CELL', KSequence(subst['###CONTINUATION'])))
+        new_constraints: tuple[KInner, ...] = tuple(c for c in cterm.constraints if c != target_constraint)
+        _LOGGER.info(f'Custom step: removing constraint: {target_constraint}')
+        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_forget_pattern(cterm):
+            return self._exec_forget_custom_step(cterm, cterm_symbolic)
+        else:
+            return super().custom_step(cterm, cterm_symbolic)
 
-        return None
+    def can_make_custom_step(self, cterm: CTerm) -> bool:
+        return self._check_forget_pattern(cterm) or super().can_make_custom_step(cterm)
 
 
 class FoundryKEVM(KEVM):

From c5aff319a93397bb47d138fe6a683d298d6b6eac Mon Sep 17 00:00:00 2001
From: Andrei <16517508+anvacaru@users.noreply.github.com>
Date: Wed, 4 Dec 2024 15:07:44 +0200
Subject: [PATCH 06/17] formatting

---
 src/kontrol/foundry.py | 30 ++++++++++++++++++++++--------
 src/kontrol/prove.py   |  2 --
 2 files changed, 22 insertions(+), 10 deletions(-)

diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py
index abc67251d..36aef9c76 100644
--- a/src/kontrol/foundry.py
+++ b/src/kontrol/foundry.py
@@ -113,30 +113,44 @@ def _check_forget_pattern(self, cterm: CTerm) -> bool:
         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:
+    def _exec_forget_custom_step(self, cterm: CTerm, cterm_symbolic: CTermSymbolic) -> KCFGExtendResult | None:
         """Given a CTerm, remove the constraint that's placed at the top of the K_CELL in the 'FOUNDRY-ACCOUNTS.forget' cut-rule.
 
         :param cterm: CTerm of a proof node.
-        :cterm_symbolic: CTermSymbolic instance
-        :return: If the K_CELL matches the forget_pattern, a Step with depth 1 is returned together with the new configuration, also registering that the `FOUNDRY-ACCOUNTS.forget` rule has been applied.
+        :param cterm_symbolic: CTermSymbolic instance
+        :return: If the K_CELL matches the forget_pattern and the constraint is successfully removed, returns a Step with depth 1 along with the new configuration, registering that the `cheatcode_forget` rule has been applied. If the constraint is not found, returns None.
         """
         _operators = ['_==Int_', '_<=Int_', '_<Int_', '_>=Int_', '_>Int_']
         _LOGGER.info('Custom step: Forget pattern confirmed')
         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 type(operator) is KToken
-        eq = mlEqualsTrue(KApply(_operators[int(operator.token)], fst_term, snd_term))
+        assert isinstance(operator, KToken)
+        constraint = mlEqualsTrue(KApply(_operators[int(operator.token)], fst_term, snd_term))
+
+        # Simplify the constraint
         kevm = KEVM(kdist.get('kontrol.foundry'))
         empty_config = kevm.definition.empty_config(GENERATED_TOP_CELL)
-        simplification_cterm = CTerm.from_kast(empty_config).add_constraint(eq)
+        simplification_cterm = CTerm.from_kast(empty_config).add_constraint(constraint)
         result_cterm, _ = cterm_symbolic.simplify(simplification_cterm)
         target_constraint = single(result_cterm.constraints)
-        new_cterm = CTerm.from_kast(set_cell(cterm.kast, 'K_CELL', KSequence(subst['###CONTINUATION'])))
+
+        # Remove the target constraint from the current constraints
         new_constraints: tuple[KInner, ...] = tuple(c for c in cterm.constraints if c != target_constraint)
-        _LOGGER.info(f'Custom step: removing constraint: {target_constraint}')
+
+        # Check if the constraints have changed
+        if new_constraints == cterm.constraints:
+            _LOGGER.info('Custom step: Target constraint not found in path conditions; returning None')
+            return None
+
+        _LOGGER.info(f'Custom step: Removing constraint: {target_constraint}')
+
+        # 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:
diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py
index bf4708efe..ac248b39a 100644
--- a/src/kontrol/prove.py
+++ b/src/kontrol/prove.py
@@ -442,8 +442,6 @@ def create_kcfg_explore() -> KCFGExplore:
                 )
 
             cut_point_rules.append('FOUNDRY-ACCOUNTS.forget')
-            print('CUT POINT RULES')
-            print(cut_point_rules)
 
             extra_lemmas_module: KFlatModule | None = None
             if options.extra_module:

From ae0ceb0d3d8c24b9c817d7650760ef9662725283 Mon Sep 17 00:00:00 2001
From: Andrei <16517508+anvacaru@users.noreply.github.com>
Date: Wed, 4 Dec 2024 16:52:15 +0200
Subject: [PATCH 07/17] add back not equal

---
 src/kontrol/foundry.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py
index 36aef9c76..83dd9e1fb 100644
--- a/src/kontrol/foundry.py
+++ b/src/kontrol/foundry.py
@@ -120,7 +120,7 @@ def _exec_forget_custom_step(self, cterm: CTerm, cterm_symbolic: CTermSymbolic)
         :param cterm_symbolic: CTermSymbolic instance
         :return: If the K_CELL matches the forget_pattern and the constraint is successfully removed, returns a Step with depth 1 along with the new configuration, registering that the `cheatcode_forget` rule has been applied. If the constraint is not found, returns None.
         """
-        _operators = ['_==Int_', '_<=Int_', '_<Int_', '_>=Int_', '_>Int_']
+        _operators = ['_==Int_', '_!=Int_', '_<=Int_', '_<Int_', '_>=Int_', '_>Int_']
         _LOGGER.info('Custom step: Forget pattern confirmed')
         subst = self._cached_subst
         assert subst is not None

From 88de162d751d020fcd888732f0efa7127d06ad27 Mon Sep 17 00:00:00 2001
From: Andrei <16517508+anvacaru@users.noreply.github.com>
Date: Thu, 5 Dec 2024 08:23:56 +0200
Subject: [PATCH 08/17] rename FOUNDRYSemantics to KontrolSemantics

---
 src/kontrol/foundry.py | 16 ++++++++--------
 src/kontrol/prove.py   |  8 ++++----
 2 files changed, 12 insertions(+), 12 deletions(-)

diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py
index 83dd9e1fb..ca1947eb4 100644
--- a/src/kontrol/foundry.py
+++ b/src/kontrol/foundry.py
@@ -94,7 +94,7 @@
 _LOGGER: Final = logging.getLogger(__name__)
 
 
-class FOUNDRYSemantics(KEVMSemantics):
+class KontrolSemantics(KEVMSemantics):
 
     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.
@@ -922,7 +922,7 @@ def foundry_show(
     if options.failure_info:
         with legacy_explore(
             foundry.kevm,
-            kcfg_semantics=FOUNDRYSemantics(),
+            kcfg_semantics=KontrolSemantics(),
             id=test_id,
             smt_timeout=options.smt_timeout,
             smt_retry_limit=options.smt_retry_limit,
@@ -989,7 +989,7 @@ def _collect_klabel(_k: KInner) -> None:
         ]
         sentences = [sent for sent in sentences if not _contains_foundry_klabel(sent.body)]
         sentences = [
-            sent for sent in sentences if not FOUNDRYSemantics().is_terminal(CTerm.from_kast(extract_lhs(sent.body)))
+            sent for sent in sentences if not KontrolSemantics().is_terminal(CTerm.from_kast(extract_lhs(sent.body)))
         ]
         if len(sentences) == 0:
             _LOGGER.warning(f'No claims or rules retained for proof {proof.id}')
@@ -1179,7 +1179,7 @@ def foundry_simplify_node(
 
     with legacy_explore(
         foundry.kevm,
-        kcfg_semantics=FOUNDRYSemantics(),
+        kcfg_semantics=KontrolSemantics(),
         id=apr_proof.id,
         bug_report=options.bug_report,
         kore_rpc_command=kore_rpc_command,
@@ -1227,7 +1227,7 @@ def check_cells_equal(cell: str, nodes: Iterable[KCFG.Node]) -> bool:
     check_cells_ne = [check_cell for check_cell in check_cells if not check_cells_equal(check_cell, nodes)]
 
     if check_cells_ne:
-        if not all(FOUNDRYSemantics().same_loop(nodes[0].cterm, nd.cterm) for nd in nodes):
+        if not all(KontrolSemantics().same_loop(nodes[0].cterm, nd.cterm) for nd in nodes):
             raise ValueError(f'Nodes {options.nodes} cannot be merged because they differ in: {check_cells_ne}')
 
     anti_unification = nodes[0].cterm
@@ -1267,7 +1267,7 @@ def foundry_step_node(
 
     with legacy_explore(
         foundry.kevm,
-        kcfg_semantics=FOUNDRYSemantics(),
+        kcfg_semantics=KontrolSemantics(),
         id=apr_proof.id,
         bug_report=options.bug_report,
         kore_rpc_command=kore_rpc_command,
@@ -1343,7 +1343,7 @@ def foundry_section_edge(
 
     with legacy_explore(
         foundry.kevm,
-        kcfg_semantics=FOUNDRYSemantics(),
+        kcfg_semantics=KontrolSemantics(),
         id=apr_proof.id,
         bug_report=options.bug_report,
         kore_rpc_command=kore_rpc_command,
@@ -1394,7 +1394,7 @@ def foundry_get_model(
 
     with legacy_explore(
         foundry.kevm,
-        kcfg_semantics=FOUNDRYSemantics(),
+        kcfg_semantics=KontrolSemantics(),
         id=proof.id,
         bug_report=options.bug_report,
         kore_rpc_command=kore_rpc_command,
diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py
index ac248b39a..c0ac3bc3d 100644
--- a/src/kontrol/prove.py
+++ b/src/kontrol/prove.py
@@ -35,7 +35,7 @@
 from pyk.utils import hash_str, run_process_2, single, unique
 from rich.progress import Progress, SpinnerColumn, TaskID, TextColumn, TimeElapsedColumn
 
-from .foundry import Foundry, FOUNDRYSemantics, foundry_to_xml
+from .foundry import Foundry, KontrolSemantics, foundry_to_xml
 from .hevm import Hevm
 from .options import ConfigType, TraceOptions
 from .solc_to_k import Contract, hex_string_to_int
@@ -381,7 +381,7 @@ def create_kcfg_explore() -> KCFGExplore:
                 )
                 return KCFGExplore(
                     cterm_symbolic,
-                    kcfg_semantics=FOUNDRYSemantics(auto_abstract_gas=options.auto_abstract_gas),
+                    kcfg_semantics=KontrolSemantics(auto_abstract_gas=options.auto_abstract_gas),
                     id=test.id,
                 )
 
@@ -425,7 +425,7 @@ def create_kcfg_explore() -> KCFGExplore:
                         }
                     ),
                 )
-            cut_point_rules = FOUNDRYSemantics.cut_point_rules(
+            cut_point_rules = KontrolSemantics.cut_point_rules(
                 options.break_on_jumpi,
                 options.break_on_jump,
                 options.break_on_calls,
@@ -467,7 +467,7 @@ def create_kcfg_explore() -> KCFGExplore:
                 max_depth=options.max_depth,
                 max_iterations=options.max_iterations,
                 cut_point_rules=cut_point_rules,
-                terminal_rules=FOUNDRYSemantics.terminal_rules(options.break_every_step),
+                terminal_rules=KontrolSemantics.terminal_rules(options.break_every_step),
                 counterexample_info=options.counterexample_info,
                 max_frontier_parallel=options.max_frontier_parallel,
                 fail_fast=options.fail_fast,

From 2c6bf19373ad724a75a1acb115c3576168514dab Mon Sep 17 00:00:00 2001
From: Petar Maksimovic <petar.maksimovic@runtimeverification.com>
Date: Fri, 6 Dec 2024 16:02:05 +0100
Subject: [PATCH 09/17] checking for negation as well

---
 src/kontrol/foundry.py | 32 +++++++++++++++++---------------
 1 file changed, 17 insertions(+), 15 deletions(-)

diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py
index ca1947eb4..619399912 100644
--- a/src/kontrol/foundry.py
+++ b/src/kontrol/foundry.py
@@ -130,28 +130,30 @@ def _exec_forget_custom_step(self, cterm: CTerm, cterm_symbolic: CTermSymbolic)
         snd_term = subst['###TERM2']
         operator = subst['###OPERATOR']
         assert isinstance(operator, KToken)
-        constraint = mlEqualsTrue(KApply(_operators[int(operator.token)], fst_term, snd_term))
+        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)))
 
         # Simplify the constraint
         kevm = KEVM(kdist.get('kontrol.foundry'))
         empty_config = kevm.definition.empty_config(GENERATED_TOP_CELL)
-        simplification_cterm = CTerm.from_kast(empty_config).add_constraint(constraint)
-        result_cterm, _ = cterm_symbolic.simplify(simplification_cterm)
-        target_constraint = single(result_cterm.constraints)
+        for constraint in [pos_constraint, neg_constraint]:
+            simplification_cterm = CTerm.from_kast(empty_config).add_constraint(constraint)
+            result_cterm, _ = cterm_symbolic.simplify(simplification_cterm)
+            target_constraint = single(result_cterm.constraints)
 
-        # Remove the target constraint from the current constraints
-        new_constraints: tuple[KInner, ...] = tuple(c for c in cterm.constraints if c != target_constraint)
+            # Remove the target constraint from the current constraints
+            new_constraints: tuple[KInner, ...] = tuple(c for c in cterm.constraints if c != target_constraint)
 
-        # Check if the constraints have changed
-        if new_constraints == cterm.constraints:
-            _LOGGER.info('Custom step: Target constraint not found in path conditions; returning None')
-            return None
-
-        _LOGGER.info(f'Custom step: Removing constraint: {target_constraint}')
+            # Check if the constraints have changed
+            if new_constraints == cterm.constraints:
+                _LOGGER.info(f'Custom step: Target constraint:\n{target_constraint}\nnot found in current constraints')
+            else:
+                _LOGGER.info(f'Custom step: Removing constraint:\n{target_constraint}')
 
-        # 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)
+            # 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)
+        return None
 
     def custom_step(self, cterm: CTerm, cterm_symbolic: CTermSymbolic) -> KCFGExtendResult | None:
         if self._check_forget_pattern(cterm):

From 7e474932ec829d131f1dfa666a8332ba2cb0e927 Mon Sep 17 00:00:00 2001
From: Petar Maksimovic <petar.maksimovic@runtimeverification.com>
Date: Fri, 6 Dec 2024 21:00:06 +0100
Subject: [PATCH 10/17] correcting indentation

---
 src/kontrol/foundry.py | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py
index 619399912..76b1d6349 100644
--- a/src/kontrol/foundry.py
+++ b/src/kontrol/foundry.py
@@ -150,9 +150,9 @@ def _exec_forget_custom_step(self, cterm: CTerm, cterm_symbolic: CTermSymbolic)
             else:
                 _LOGGER.info(f'Custom step: Removing constraint:\n{target_constraint}')
 
-            # 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)
+                # 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)
         return None
 
     def custom_step(self, cterm: CTerm, cterm_symbolic: CTermSymbolic) -> KCFGExtendResult | None:

From 088a17462c3e60490fdb19945ba925e28a53f25d Mon Sep 17 00:00:00 2001
From: Petar Maksimovic <petar.maksimovic@runtimeverification.com>
Date: Sun, 8 Dec 2024 19:17:13 +0100
Subject: [PATCH 11/17] expanding functionality

---
 src/kontrol/foundry.py | 67 ++++++++++++++++++++++++++++++------------
 1 file changed, 48 insertions(+), 19 deletions(-)

diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py
index 76b1d6349..8d0c911f7 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,
@@ -130,30 +131,58 @@ def _exec_forget_custom_step(self, cterm: CTerm, cterm_symbolic: CTermSymbolic)
         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)))
+        # Pinpoint variables of interest
+        variables_to_look_for: frozenset[str] = free_vars(fst_term).union(free_vars(snd_term))
+        # Range-constraint patterns
+        range_constraint_patterns: list[KInner] = [
+            mlEqualsTrue(KApply('_<=Int_', KToken('###NUM', INT), KVariable('###VAR'))),
+            mlEqualsTrue(KApply('_<=Int_', KVariable('###VAR'), KToken('###NUM', INT))),
+            mlEqualsTrue(KApply('_<Int_', KToken('###NUM', INT), KVariable('###VAR'))),
+            mlEqualsTrue(KApply('_<Int_', KVariable('###VAR'), KToken('###NUM', INT))),
+            mlEqualsTrue(notBool(KApply('_==Int_', KToken('###NUM', INT), KVariable('###VAR')))),
+            mlEqualsTrue(notBool(KApply('_==Int_', KVariable('###VAR'), KToken('###NUM', INT)))),
+        ]
+        # Preserve range constraints of variables of intereset
+        constraints_to_keep: set[KInner] = set()
+        for constraint in cterm.constraints:
+            if any(
+                subst['###VAR'] in variables_to_look_for
+                for pattern in range_constraint_patterns
+                if (subst := constraint.match(pattern)) and subst is not None
+            ):
+                _LOGGER.info(f'forgetBranch: keeping constraint: {constraint}')
+                constraints_to_keep.add(constraint)
 
-        # Simplify the constraint
+        # Set up analysis
         kevm = KEVM(kdist.get('kontrol.foundry'))
-        empty_config = kevm.definition.empty_config(GENERATED_TOP_CELL)
+        empty_config: CTerm = CTerm.from_kast(kevm.definition.empty_config(GENERATED_TOP_CELL))
+        new_constraints: set[KInner] = set(cterm.constraints)
+        initial_cterm, _ = cterm_symbolic.simplify(CTerm(empty_config.config, constraints_to_keep))
+        constraints_to_keep = set(initial_cterm.constraints)
+        found: bool = False
+        # 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
         for constraint in [pos_constraint, neg_constraint]:
-            simplification_cterm = CTerm.from_kast(empty_config).add_constraint(constraint)
-            result_cterm, _ = cterm_symbolic.simplify(simplification_cterm)
-            target_constraint = single(result_cterm.constraints)
-
-            # Remove the target constraint from the current constraints
-            new_constraints: tuple[KInner, ...] = tuple(c for c in cterm.constraints if c != target_constraint)
-
-            # Check if the constraints have changed
-            if new_constraints == cterm.constraints:
-                _LOGGER.info(f'Custom step: Target constraint:\n{target_constraint}\nnot found in current constraints')
-            else:
-                _LOGGER.info(f'Custom step: Removing constraint:\n{target_constraint}')
-
-                # 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)
-        return None
+            if not found:
+                simplification_cterm = initial_cterm.add_constraint(constraint)
+                result_cterm, _ = cterm_symbolic.simplify(simplification_cterm)
+                result_constraints = set(result_cterm.constraints).difference(constraints_to_keep)
+                if len(result_constraints) == 1:
+                    target_constraint = single(result_cterm.constraints)
+                    # Remove the target constraint from the current constraints
+                    if constraint in new_constraints:
+                        _LOGGER.info(f'forgetBranch: removing constraint: {target_constraint}')
+                        new_constraints.remove(constraint)
+                        found = True
+                    else:
+                        _LOGGER.info(f'forgetBranch: constraint: {target_constraint} not found in current constraints')
+
+        # 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_forget_pattern(cterm):

From 92bf19639d38ce7015b5955cfbfd4ddd7f24ac70 Mon Sep 17 00:00:00 2001
From: Petar Maksimovic <petar.maksimovic@runtimeverification.com>
Date: Sun, 8 Dec 2024 23:06:54 +0100
Subject: [PATCH 12/17] heuristic simplifications

---
 src/kontrol/foundry.py | 83 ++++++++++++++++++++++--------------------
 1 file changed, 43 insertions(+), 40 deletions(-)

diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py
index 8d0c911f7..0411e01c6 100644
--- a/src/kontrol/foundry.py
+++ b/src/kontrol/foundry.py
@@ -115,17 +115,19 @@ def _check_forget_pattern(self, cterm: CTerm) -> bool:
         return self._cached_subst is not None
 
     def _exec_forget_custom_step(self, cterm: CTerm, cterm_symbolic: CTermSymbolic) -> KCFGExtendResult | None:
-        """Given a CTerm, remove the constraint that's placed at the top of the K_CELL in the 'FOUNDRY-ACCOUNTS.forget' cut-rule.
+        """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 of a proof node.
+        :param cterm: CTerm representing a proof node
         :param cterm_symbolic: CTermSymbolic instance
-        :return: If the K_CELL matches the forget_pattern and the constraint is successfully removed, returns a Step with depth 1 along with the new configuration, registering that the `cheatcode_forget` rule has been applied. If the constraint is not found, returns None.
+        :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.
         """
+        _LOGGER.info('forgetBranch: pattern confirmed')
         _operators = ['_==Int_', '_!=Int_', '_<=Int_', '_<Int_', '_>=Int_', '_>Int_']
-        _LOGGER.info('Custom step: Forget pattern confirmed')
         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']
@@ -134,52 +136,53 @@ def _exec_forget_custom_step(self, cterm: CTerm, cterm_symbolic: CTermSymbolic)
         # 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)))
-        # Pinpoint variables of interest
-        variables_to_look_for: frozenset[str] = free_vars(fst_term).union(free_vars(snd_term))
-        # Range-constraint patterns
-        range_constraint_patterns: list[KInner] = [
-            mlEqualsTrue(KApply('_<=Int_', KToken('###NUM', INT), KVariable('###VAR'))),
-            mlEqualsTrue(KApply('_<=Int_', KVariable('###VAR'), KToken('###NUM', INT))),
-            mlEqualsTrue(KApply('_<Int_', KToken('###NUM', INT), KVariable('###VAR'))),
-            mlEqualsTrue(KApply('_<Int_', KVariable('###VAR'), KToken('###NUM', INT))),
-            mlEqualsTrue(notBool(KApply('_==Int_', KToken('###NUM', INT), KVariable('###VAR')))),
-            mlEqualsTrue(notBool(KApply('_==Int_', KVariable('###VAR'), KToken('###NUM', INT)))),
+        # 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))
+        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)))),
         ]
-        # Preserve range constraints of variables of intereset
         constraints_to_keep: set[KInner] = set()
         for constraint in cterm.constraints:
-            if any(
-                subst['###VAR'] in variables_to_look_for
-                for pattern in range_constraint_patterns
-                if (subst := constraint.match(pattern)) and subst is not None
-            ):
-                _LOGGER.info(f'forgetBranch: keeping constraint: {constraint}')
-                constraints_to_keep.add(constraint)
-
-        # Set up analysis
+            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
+        # 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))
         new_constraints: set[KInner] = set(cterm.constraints)
         initial_cterm, _ = cterm_symbolic.simplify(CTerm(empty_config.config, constraints_to_keep))
         constraints_to_keep = set(initial_cterm.constraints)
-        found: bool = False
         # 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
         for constraint in [pos_constraint, neg_constraint]:
-            if not found:
-                simplification_cterm = initial_cterm.add_constraint(constraint)
-                result_cterm, _ = cterm_symbolic.simplify(simplification_cterm)
-                result_constraints = set(result_cterm.constraints).difference(constraints_to_keep)
-                if len(result_constraints) == 1:
-                    target_constraint = single(result_cterm.constraints)
-                    # Remove the target constraint from the current constraints
-                    if constraint in new_constraints:
-                        _LOGGER.info(f'forgetBranch: removing constraint: {target_constraint}')
-                        new_constraints.remove(constraint)
-                        found = True
-                    else:
-                        _LOGGER.info(f'forgetBranch: constraint: {target_constraint} not found in current constraints')
-
+            simplification_cterm = initial_cterm.add_constraint(constraint)
+            result_cterm, _ = cterm_symbolic.simplify(simplification_cterm)
+            result_constraints = set(result_cterm.constraints).difference(constraints_to_keep)
+            if len(result_constraints) == 1:
+                target_constraint = single(result_constraints)
+                # Remove the target constraint from the current constraints
+                if target_constraint in new_constraints:
+                    _LOGGER.info(f'forgetBranch: removing constraint: {target_constraint}')
+                    new_constraints.remove(target_constraint)
+                    break
+                else:
+                    _LOGGER.info(f'forgetBranch: constraint: {target_constraint} not found in current constraints')
         # 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)

From 5d6c91304dfd829376fc09a8e5fcb8741f96d3c4 Mon Sep 17 00:00:00 2001
From: Petar Maksimovic <petar.maksimovic@runtimeverification.com>
Date: Mon, 9 Dec 2024 18:26:24 +0100
Subject: [PATCH 13/17] further refinement

---
 src/kontrol/foundry.py | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py
index 0411e01c6..7784759a7 100644
--- a/src/kontrol/foundry.py
+++ b/src/kontrol/foundry.py
@@ -183,6 +183,13 @@ def _exec_forget_custom_step(self, cterm: CTerm, cterm_symbolic: CTermSymbolic)
                     break
                 else:
                     _LOGGER.info(f'forgetBranch: constraint: {target_constraint} not found in current constraints')
+            else:
+                if len(result_constraints) == 0:
+                    _LOGGER.info(f'forgetBranch: constraint {constraint} entailed by remaining constraints')
+                else:
+                    _LOGGER.info(
+                        f'forgetBranch: more than one constraint found after simplification and removal:\n{result_constraints}'
+                    )
         # 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)

From d71a3ce1fe440e65e654d7baee3924aebcaa5cc5 Mon Sep 17 00:00:00 2001
From: Andrei <16517508+anvacaru@users.noreply.github.com>
Date: Tue, 10 Dec 2024 11:14:58 +0200
Subject: [PATCH 14/17] refactoring _exec_forget_custom_step

---
 src/kontrol/foundry.py | 112 ++++++++++++++++++++++++-----------------
 src/kontrol/prove.py   |   2 -
 2 files changed, 65 insertions(+), 49 deletions(-)

diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py
index b2ddc782d..a97e8deb2 100644
--- a/src/kontrol/foundry.py
+++ b/src/kontrol/foundry.py
@@ -107,7 +107,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,
@@ -182,8 +182,65 @@ def _exec_forget_custom_step(self, cterm: CTerm, cterm_symbolic: CTermSymbolic)
                  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.
         """
-        _LOGGER.info('forgetBranch: pattern confirmed')
-        _operators = ['_==Int_', '_!=Int_', '_<=Int_', '_<Int_', '_>=Int_', '_>Int_']
+
+        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],
+        ) -> 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')
+                    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
@@ -196,58 +253,19 @@ def _exec_forget_custom_step(self, cterm: CTerm, cterm_symbolic: CTermSymbolic)
         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))
-        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
+        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))
-        new_constraints: set[KInner] = set(cterm.constraints)
         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
-        for constraint in [pos_constraint, neg_constraint]:
-            simplification_cterm = initial_cterm.add_constraint(constraint)
-            result_cterm, _ = cterm_symbolic.simplify(simplification_cterm)
-            result_constraints = set(result_cterm.constraints).difference(constraints_to_keep)
-            if len(result_constraints) == 1:
-                target_constraint = single(result_constraints)
-                # Remove the target constraint from the current constraints
-                if target_constraint in new_constraints:
-                    _LOGGER.info(f'forgetBranch: removing constraint: {target_constraint}')
-                    new_constraints.remove(target_constraint)
-                    break
-                else:
-                    _LOGGER.info(f'forgetBranch: constraint: {target_constraint} not found in current constraints')
-            else:
-                if len(result_constraints) == 0:
-                    _LOGGER.info(f'forgetBranch: constraint {constraint} entailed by remaining constraints')
-                else:
-                    _LOGGER.info(
-                        f'forgetBranch: more than one constraint found after simplification and removal:\n{result_constraints}'
-                    )
+        new_constraints: set[KInner] = _filter_constraints_by_simplification(
+            cterm_symbolic, initial_cterm, [pos_constraint, neg_constraint], constraints_to_keep, set(cterm.constraints)
+        )
         # 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)
diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py
index c0ac3bc3d..58fa15991 100644
--- a/src/kontrol/prove.py
+++ b/src/kontrol/prove.py
@@ -441,8 +441,6 @@ def create_kcfg_explore() -> KCFGExplore:
                     rule.label for rule in foundry.kevm.definition.all_modules_dict['KONTROL-ASSERTIONS'].rules
                 )
 
-            cut_point_rules.append('FOUNDRY-ACCOUNTS.forget')
-
             extra_lemmas_module: KFlatModule | None = None
             if options.extra_module:
                 extra_module_file, extra_module_name, *_ = options.extra_module.split(':')

From 9e05d194c36ee68c0e5f39b6a1ce5712b94f96f6 Mon Sep 17 00:00:00 2001
From: Andrei <16517508+anvacaru@users.noreply.github.com>
Date: Tue, 10 Dec 2024 11:46:18 +0200
Subject: [PATCH 15/17] add show test

---
 src/kontrol/kdist/cheatcodes.md               |   1 -
 .../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 | 787 ++++++++++++++++++
 .../{foundry/test => src}/ForgetBranch.t.sol  |   5 +-
 6 files changed, 823 insertions(+), 34 deletions(-)
 create mode 100644 src/tests/integration/test-data/show/ForgetBranchTest.test_forgetBranch(uint256).expected
 rename src/tests/integration/test-data/{foundry/test => src}/ForgetBranch.t.sol (72%)

diff --git a/src/kontrol/kdist/cheatcodes.md b/src/kontrol/kdist/cheatcodes.md
index dac8848a8..15da6c2a9 100644
--- a/src/kontrol/kdist/cheatcodes.md
+++ b/src/kontrol/kdist/cheatcodes.md
@@ -1771,7 +1771,6 @@ 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 ( "replaceConstraint(uint256,uint8,uint256,bool)" ) => 1408652492 )
     rule ( selector ( "forgetBranch(uint256,uint8,uint256)" )      => 1720990067 )
 ```
 
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..5a44b8953
--- /dev/null
+++ b/src/tests/integration/test-data/show/ForgetBranchTest.test_forgetBranch(uint256).expected
@@ -0,0 +1,787 @@
+
+┌─ 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 ( 200 , 5 , KV0_x:Int ) ~> #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)
+│
+│  (112 steps)
+├─ 5 (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 ( 200 , 5 , KV0_x:Int )
+               ~> #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\x00\x00\x00\x00\x00\x00\x00\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\x00\x00\x00\x00\x00\x00\x00\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" +Bytes #buf ( 32 , KV0_x:Int ) )
+                   </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>
+                   ...
+                 </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 ( 200 , 5 , KV0_x:Int ) ~> .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\x00\x00\x00\x00\x00\x00\x00\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\x00\x00\x00\x00\x00\x00\x00\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" +Bytes #buf ( 32 , KV0_x:Int )
+                   </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>
+                   ...
+                 </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 ]
+               ~> #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>
+                     ( ( 228 => selector ( "test_forgetBranch(uint256)" ) ) : ( ( selector ( "forgetBranch(uint256,uint8,uint256)" ) : ( 645326474426547203313410069153905908525362434349 : ( 0 : ( 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\x00\x00\x00\x00\x00\x00\x00\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\x00\x00\x00\x00\x00\x00\x00\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" +Bytes #buf ( 32 , KV0_x:Int )
+                   </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>
+                   ...
+                 </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-4-TO-5)]
+
+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/foundry/test/ForgetBranch.t.sol b/src/tests/integration/test-data/src/ForgetBranch.t.sol
similarity index 72%
rename from src/tests/integration/test-data/foundry/test/ForgetBranch.t.sol
rename to src/tests/integration/test-data/src/ForgetBranch.t.sol
index 53ac90f3e..a813ac129 100644
--- a/src/tests/integration/test-data/foundry/test/ForgetBranch.t.sol
+++ b/src/tests/integration/test-data/src/ForgetBranch.t.sol
@@ -1,16 +1,17 @@
 // SPDX-License-Identifier: UNLICENSED
 pragma solidity >=0.8.13;
 
-import "forge-std/Test.sol";
+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(200, 2, x);
+        kevm.forgetBranch(200, KontrolCheatsBase.ComparisonOperator.GreaterThan, x);
         if(x > 200){
             y = 21;
         } else {

From 49cee7babad42435d44a277b7cace14ef39fd27d Mon Sep 17 00:00:00 2001
From: Andrei <16517508+anvacaru@users.noreply.github.com>
Date: Tue, 10 Dec 2024 13:40:40 +0200
Subject: [PATCH 16/17] fix test

---
 src/kontrol/foundry.py                        |  16 +-
 ...chTest.test_forgetBranch(uint256).expected | 582 +++++++++++++++++-
 .../test-data/src/ForgetBranch.t.sol          |   2 +-
 3 files changed, 575 insertions(+), 25 deletions(-)

diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py
index a97e8deb2..b46764db5 100644
--- a/src/kontrol/foundry.py
+++ b/src/kontrol/foundry.py
@@ -215,6 +215,7 @@ def _filter_constraints_by_simplification(
             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)
@@ -234,6 +235,12 @@ def _filter_constraints_by_simplification(
                     # 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}'
@@ -261,11 +268,18 @@ def _filter_constraints_by_simplification(
         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, initial_cterm, [pos_constraint, neg_constraint], constraints_to_keep, set(cterm.constraints)
+            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)
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
index 5a44b8953..75243bf5d 100644
--- a/src/tests/integration/test-data/show/ForgetBranchTest.test_forgetBranch(uint256).expected
+++ b/src/tests/integration/test-data/show/ForgetBranchTest.test_forgetBranch(uint256).expected
@@ -9,7 +9,7 @@
 │
 │  (755 steps)
 ├─ 3
-│   k: #forget ( 200 , 5 , KV0_x:Int ) ~> #cheatcode_return 128 0 ~> #pc [ CALL ] ~> #e ...
+│   k: #forget ( KV0_x:Int , 5 , 200 ) ~> #cheatcode_return 128 0 ~> #pc [ CALL ] ~> #e ...
 │   pc: 1294
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
@@ -25,22 +25,73 @@
 │   src: test/ForgetBranch.t.sol:14:14
 │   method: test%ForgetBranchTest.test_forgetBranch(uint256)
 │
-│  (112 steps)
-├─ 5 (terminal)
-│   k: #halt ~> CONTINUATION:K
-│   pc: 320
+│  (72 steps)
+├─ 5 (split)
+│   k: JUMPI 1326 bool2Word ( KV0_x:Int <=Int 200 ) ~> #pc [ JUMPI ] ~> #execute ~> CON ...
+│   pc: 1322
 │   callDepth: 0
-│   statusCode: EVMC_SUCCESS
-│   src: test/ForgetBranch.t.sol:10:20
+│   statusCode: STATUSCODE:StatusCode
+│   src: test/ForgetBranch.t.sol:15:19
 │   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
+┃
+┃ (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
 
 
 
@@ -51,7 +102,7 @@ module SUMMARY-TEST%FORGETBRANCHTEST.TEST-FORGETBRANCH(UINT256):0
     rule [BASIC-BLOCK-1-TO-3]: <foundry>
            <kevm>
              <k>
-               ( .K => #forget ( 200 , 5 , KV0_x:Int )
+               ( .K => #forget ( KV0_x:Int , 5 , 200 )
                ~> #cheatcode_return 128 0
                ~> #pc [ CALL ] )
                ~> #execute
@@ -97,7 +148,7 @@ module SUMMARY-TEST%FORGETBRANCHTEST.TEST-FORGETBRANCH(UINT256):0
                      ( .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\x00\x00\x00\x00\x00\x00\x00\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\x00\x00\x00\x00\x00\x00\x00\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" +Bytes #buf ( 32 , KV0_x:Int ) )
+                     ( 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
@@ -293,7 +344,7 @@ module SUMMARY-TEST%FORGETBRANCHTEST.TEST-FORGETBRANCH(UINT256):0
     rule [BASIC-BLOCK-3-TO-4]: <foundry>
            <kevm>
              <k>
-               ( #forget ( 200 , 5 , KV0_x:Int ) ~> .K => .K )
+               ( #forget ( KV0_x:Int , 5 , 200 ) ~> .K => .K )
                ~> #cheatcode_return 128 0
                ~> #pc [ CALL ]
                ~> #execute
@@ -339,7 +390,7 @@ module SUMMARY-TEST%FORGETBRANCHTEST.TEST-FORGETBRANCH(UINT256):0
                      ( 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\x00\x00\x00\x00\x00\x00\x00\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\x00\x00\x00\x00\x00\x00\x00\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" +Bytes #buf ( 32 , KV0_x:Int )
+                     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
@@ -536,7 +587,248 @@ module SUMMARY-TEST%FORGETBRANCHTEST.TEST-FORGETBRANCH(UINT256):0
            <kevm>
              <k>
                ( #cheatcode_return 128 0
-               ~> #pc [ CALL ]
+               ~> #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>
+                   ...
+                 </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>
@@ -580,10 +872,254 @@ module SUMMARY-TEST%FORGETBRANCHTEST.TEST-FORGETBRANCH(UINT256):0
                      0
                    </callValue>
                    <wordStack>
-                     ( ( 228 => selector ( "test_forgetBranch(uint256)" ) ) : ( ( selector ( "forgetBranch(uint256,uint8,uint256)" ) : ( 645326474426547203313410069153905908525362434349 : ( 0 : ( KV0_x:Int : ( 319 : ( selector ( "test_forgetBranch(uint256)" ) : .WordStack ) ) ) ) ) ) => .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\x00\x00\x00\x00\x00\x00\x00\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\x00\x00\x00\x00\x00\x00\x00\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" +Bytes #buf ( 32 , KV0_x:Int )
+                     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>
+                   ...
+                 </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
@@ -774,7 +1310,7 @@ module SUMMARY-TEST%FORGETBRANCHTEST.TEST-FORGETBRANCH(UINT256):0
        andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
                ))))))))))))))))
-      [priority(20), label(BASIC-BLOCK-4-TO-5)]
+      [priority(20), label(BASIC-BLOCK-7-TO-9)]
 
 endmodule
 0 Failure nodes. (0 pending and 0 failing)
diff --git a/src/tests/integration/test-data/src/ForgetBranch.t.sol b/src/tests/integration/test-data/src/ForgetBranch.t.sol
index a813ac129..fe4064aa8 100644
--- a/src/tests/integration/test-data/src/ForgetBranch.t.sol
+++ b/src/tests/integration/test-data/src/ForgetBranch.t.sol
@@ -11,7 +11,7 @@ contract ForgetBranchTest is Test, KontrolCheats {
         uint256 y;
 
         vm.assume(x > 200);
-        kevm.forgetBranch(200, KontrolCheatsBase.ComparisonOperator.GreaterThan, x);
+        kevm.forgetBranch(x, KontrolCheatsBase.ComparisonOperator.GreaterThan, 200);
         if(x > 200){
             y = 21;
         } else {

From 2652f5874a62abdaa15a00b5777b7cf488d8b873 Mon Sep 17 00:00:00 2001
From: Andrei <16517508+anvacaru@users.noreply.github.com>
Date: Thu, 23 Jan 2025 09:52:06 +0200
Subject: [PATCH 17/17] update expected output

---
 ...BranchTest.test_forgetBranch(uint256).expected | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

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
index 75243bf5d..aec40fd4a 100644
--- a/src/tests/integration/test-data/show/ForgetBranchTest.test_forgetBranch(uint256).expected
+++ b/src/tests/integration/test-data/show/ForgetBranchTest.test_forgetBranch(uint256).expected
@@ -177,6 +177,9 @@ module SUMMARY-TEST%FORGETBRANCHTEST.TEST-FORGETBRANCH(UINT256):0
                    <accessedStorage>
                      .Map
                    </accessedStorage>
+                   <createdAccounts>
+                     .Set
+                   </createdAccounts>
                    ...
                  </substate>
                  <origin>
@@ -419,6 +422,9 @@ module SUMMARY-TEST%FORGETBRANCHTEST.TEST-FORGETBRANCH(UINT256):0
                    <accessedStorage>
                      .Map
                    </accessedStorage>
+                   <createdAccounts>
+                     .Set
+                   </createdAccounts>
                    ...
                  </substate>
                  <origin>
@@ -661,6 +667,9 @@ module SUMMARY-TEST%FORGETBRANCHTEST.TEST-FORGETBRANCH(UINT256):0
                    <accessedStorage>
                      .Map
                    </accessedStorage>
+                   <createdAccounts>
+                     .Set
+                   </createdAccounts>
                    ...
                  </substate>
                  <origin>
@@ -904,6 +913,9 @@ module SUMMARY-TEST%FORGETBRANCHTEST.TEST-FORGETBRANCH(UINT256):0
                    <accessedStorage>
                      .Map
                    </accessedStorage>
+                   <createdAccounts>
+                     .Set
+                   </createdAccounts>
                    ...
                  </substate>
                  <origin>
@@ -1148,6 +1160,9 @@ module SUMMARY-TEST%FORGETBRANCHTEST.TEST-FORGETBRANCH(UINT256):0
                    <accessedStorage>
                      .Map
                    </accessedStorage>
+                   <createdAccounts>
+                     .Set
+                   </createdAccounts>
                    ...
                  </substate>
                  <origin>