Skip to content

Commit 87b87ab

Browse files
committed
kevm-pyk/__main__: pass in learned witness instead of inferring it
1 parent 689e7c6 commit 87b87ab

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

kevm-pyk/src/kevm_pyk/__main__.py

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -372,8 +372,8 @@ def prove_it(id_and_cfg: Tuple[str, Tuple[KCFG, Path]]) -> bool:
372372
iterations += 1
373373
curr_node = cfg.frontier[0]
374374

375-
if foundry.check_implication(curr_node.cterm, target_node.cterm) is not None:
376-
cfg.create_cover(curr_node.id, target_node.id)
375+
if subst := foundry.check_implication(curr_node.cterm, target_node.cterm):
376+
cfg.create_cover(curr_node.id, target_node.id, witness=(subst, mlTop()))
377377
_LOGGER.info(f'Subsumed into target node: {shorten_hashes((curr_node.id, target_node.id))}')
378378
continue
379379

0 commit comments

Comments
 (0)