diff --git a/flake.lock b/flake.lock index caf2d5300..f143542a3 100644 --- a/flake.lock +++ b/flake.lock @@ -209,11 +209,11 @@ ] }, "locked": { - "lastModified": 1727946687, - "narHash": "sha256-V0oYWKhwcQx0VJ3BY/jDgWxm9MY9m+Fbpr1Pz/BVyfE=", + "lastModified": 1728033094, + "narHash": "sha256-6v9Nj+8PnALQE3CW6tSu8gmFB9U9UFIRHeo2VIlWblE=", "owner": "shazow", "repo": "foundry.nix", - "rev": "00f618d5572c5c3556a00e1ac5066d9526d95e2c", + "rev": "84be75ae73447a8c67ab8a0be2bc24d7bee87940", "type": "github" }, "original": { 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 diff --git a/src/tests/integration/test-data/show/AssertTest.checkFail_assert_false().expected b/src/tests/integration/test-data/show/AssertTest.checkFail_assert_false().expected index 1a2da4b40..824a8d766 100644 --- a/src/tests/integration/test-data/show/AssertTest.checkFail_assert_false().expected +++ b/src/tests/integration/test-data/show/AssertTest.checkFail_assert_false().expected @@ -525,11 +525,11 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0 andBool ( NUMBER_CELL:Int #pc [ JUMPI ] ~> #execute ~> CONTINUATION:K +┃ │ k: JUMPI 508 bool2Word ( ?WORD:Int <=Int 0 ) ~> #pc [ JUMPI ] ~> #execute ~> CONTIN ... ┃ │ pc: 465 ┃ │ callDepth: 0 ┃ │ statusCode: STATUSCODE:StatusCode @@ -475,7 +475,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 rule [BASIC-BLOCK-4-TO-6]: - ( JUMPI 508 1 + ( JUMPI 508 bool2Word ( ?WORD:Int <=Int 0 ) ~> #pc [ JUMPI ] ~> #execute => #halt ~> .K ) ~> _CONTINUATION @@ -702,12 +702,12 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 andBool ( NUMBER_CELL:Int