From 6e751c6f22a0691f7bfea1a7446a77abe929f46f Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Fri, 4 Oct 2024 00:02:49 +0100 Subject: [PATCH] Simplifying nodes by need --- src/kontrol/prove.py | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index 2ea670ec3..ac68b974c 100644 --- a/src/kontrol/prove.py +++ b/src/kontrol/prove.py @@ -664,18 +664,15 @@ def _method_to_initialized_cfg( init_term = KDefinition__expand_macros(foundry.kevm.definition, init_term) init_cterm = CTerm.from_kast(init_term) _LOGGER.info(f'Computing definedness constraint for node {node_id} for test: {test.name}') - init_cterm = kcfg_explore.cterm_symbolic.assume_defined(init_cterm) + init_cterm, _ = kcfg_explore.cterm_symbolic.simplify(kcfg_explore.cterm_symbolic.assume_defined(init_cterm)) kcfg.let_node(node_id, cterm=init_cterm) _LOGGER.info(f'Expanding macros in target state for test: {test.name}') target_term = kcfg.node(target_node_id).cterm.kast target_term = KDefinition__expand_macros(foundry.kevm.definition, target_term) - target_cterm = CTerm.from_kast(target_term) + target_cterm, _ = kcfg_explore.cterm_symbolic.simplify(CTerm.from_kast(target_term)) kcfg.let_node(target_node_id, cterm=target_cterm) - _LOGGER.info(f'Simplifying KCFG for test: {test.name}') - kcfg_explore.simplify(kcfg, {}) - return kcfg, init_node_id, target_node_id, bounded_node_ids