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

ehildenb · ehildenb · commit a1f85cd8c2de · 2022-11-11T03:51:20.000Z
diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py
@@ -389,7 +389,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
`@@ -389,7 +389,7 @@ def prove_it(id_and_cfg: Tuple[str, Tuple[KCFG, Path]]) -> bool:`
`389`	`389`	`f'Target state reached at depth {depth}, inserted edge from {shorten_hashes((curr_node.id))} to {shorten_hashes((target_node.id))}.'`
`390`	`390`	`)`
`391`	`391`
`392`		`- next_state = CTerm(result)`
	`392`	`+ next_state = CTerm(sanitize_config(foundry.definition, result))`
`393`	`393`	`next_node = cfg.get_or_create_node(next_state)`
`394`	`394`	`if next_node != curr_node:`
`395`	`395`	`_LOGGER.info(f'Found basic block at depth {depth}: {shorten_hashes((curr_node.id, next_node.id))}.')`