kevm-pyk/__main__: after discovering proven state, dont also try to extract branches

Author: ehildenb

kevm-pyk/src/kevm_pyk/__main__.py

@@ -385,34 +385,35 @@ def prove_it(id_and_cfg: Tuple[str, Tuple[KCFG, Path]]) -> bool:
                     f'Target state reached at depth {depth}, inserted edge from {shorten_hashes((curr_node.id))} to {shorten_hashes((target_node.id))}.'
                 )
 
-            next_state = CTerm(sanitize_config(foundry.definition, result))
-            next_node = cfg.get_or_create_node(next_state)
-            if next_node != curr_node:
-                _LOGGER.info(f'Found basic block at depth {depth}: {shorten_hashes((curr_node.id, next_node.id))}.')
-                cfg.create_edge(curr_node.id, next_node.id, mlTop(), depth)
-
-            if KEVM.is_terminal(next_node.cterm):
-                cfg.add_expanded(next_node.id)
-                _LOGGER.info(f'Terminal node: {shorten_hashes((curr_node.id))}.')
-
-            elif branching:
-                branches = KEVM.extract_branches(next_state)
-                if not branches:
-                    raise ValueError(
-                        f'Could not extract branch condition:\n{foundry.pretty_print(minimize_term(result))}'
+            else:
+                next_state = CTerm(sanitize_config(foundry.definition, result))
+                next_node = cfg.get_or_create_node(next_state)
+                if next_node != curr_node:
+                    _LOGGER.info(f'Found basic block at depth {depth}: {shorten_hashes((curr_node.id, next_node.id))}.')
+                    cfg.create_edge(curr_node.id, next_node.id, mlTop(), depth)
+
+                if KEVM.is_terminal(next_node.cterm):
+                    cfg.add_expanded(next_node.id)
+                    _LOGGER.info(f'Terminal node: {shorten_hashes((curr_node.id))}.')
+
+                elif branching:
+                    branches = KEVM.extract_branches(next_state)
+                    if not branches:
+                        raise ValueError(
+                            f'Could not extract branch condition:\n{foundry.pretty_print(minimize_term(result))}'
+                        )
+                    cfg.add_expanded(next_node.id)
+                    _LOGGER.info(
+                        f'Found {len(list(branches))} branches at depth {depth}: {[foundry.pretty_print(b) for b in branches]}'
                     )
-                cfg.add_expanded(next_node.id)
-                _LOGGER.info(
-                    f'Found {len(list(branches))} branches at depth {depth}: {[foundry.pretty_print(b) for b in branches]}'
-                )
-                for branch in branches:
-                    branch_cterm = next_state.add_constraint(branch)
-                    branch_node = cfg.get_or_create_node(branch_cterm)
-                    cfg.create_edge(next_node.id, branch_node.id, branch, 0)
-                    _LOGGER.info(f'Made split: {shorten_hashes((next_node.id, branch_node.id))}')
-                    # TODO: have to store case splits as rewrites because of how frontier is handled for covers
-                    # cfg.create_cover(branch_node.id, next_node.id)
-                    # _LOGGER.info(f'Made cover: {shorten_hashes((branch_node.id, next_node.id))}')
+                    for branch in branches:
+                        branch_cterm = next_state.add_constraint(branch)
+                        branch_node = cfg.get_or_create_node(branch_cterm)
+                        cfg.create_edge(next_node.id, branch_node.id, branch, 0)
+                        _LOGGER.info(f'Made split: {shorten_hashes((next_node.id, branch_node.id))}')
+                        # TODO: have to store case splits as rewrites because of how frontier is handled for covers
+                        # cfg.create_cover(branch_node.id, next_node.id)
+                        # _LOGGER.info(f'Made cover: {shorten_hashes((branch_node.id, next_node.id))}')
 
             _write_cfg(cfg, cfgpath)