kevm-pyk/__main__: call sanitize_config on output of get_claim_basic_block

ehildenb · ehildenb · commit b5023ef17cd6 · 2022-11-03T04:55:11.000Z
diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py
@@ -385,7 +385,7 @@ 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(result)
+            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))}.')

Original file line number	Diff line number	Diff line change
`@@ -385,7 +385,7 @@ def prove_it(id_and_cfg: Tuple[str, Tuple[KCFG, Path]]) -> bool:`
`385`	`385`	`f'Target state reached at depth {depth}, inserted edge from {shorten_hashes((curr_node.id))} to {shorten_hashes((target_node.id))}.'`
`386`	`386`	`)`
`387`	`387`
`388`		`- next_state = CTerm(result)`
	`388`	`+ next_state = CTerm(sanitize_config(foundry.definition, result))`
`389`	`389`	`next_node = cfg.get_or_create_node(next_state)`
`390`	`390`	`if next_node != curr_node:`
`391`	`391`	`_LOGGER.info(f'Found basic block at depth {depth}: {shorten_hashes((curr_node.id, next_node.id))}.')`