diff --git a/pyk/package/version b/pyk/package/version index 5abb16f50c6..8cc010e6a3c 100644 --- a/pyk/package/version +++ b/pyk/package/version @@ -1 +1 @@ -0.1.443 +0.1.444 diff --git a/pyk/pyproject.toml b/pyk/pyproject.toml index 73447ac3ad3..7dcb3ba3c8f 100644 --- a/pyk/pyproject.toml +++ b/pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.443" +version = "0.1.444" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/pyk/src/pyk/kcfg/explore.py b/pyk/src/pyk/kcfg/explore.py index 0c77167a343..68cf785efc1 100644 --- a/pyk/src/pyk/kcfg/explore.py +++ b/pyk/src/pyk/kcfg/explore.py @@ -377,14 +377,19 @@ def extend( if self._check_abstract(node, kcfg): return - if not kcfg.splits(target_id=node.id): - branches = self.kcfg_semantics.extract_branches(node.cterm) - if branches: - kcfg.split_on_constraints(node.id, branches) - _LOGGER.info( - f'Found {len(branches)} branches using heuristic for node {node.id}: {shorten_hashes(node.id)}: {[self.kprint.pretty_print(bc) for bc in branches]}' - ) - return + _branches = self.kcfg_semantics.extract_branches(node.cterm) + branches = [] + for constraint in _branches: + kast = mlAnd(list(node.cterm.constraints) + [constraint]) + kast, _ = self.kast_simplify(kast) + if not CTerm._is_bottom(kast): + branches.append(constraint) + if len(branches) > 1: + kcfg.split_on_constraints(node.id, branches) + _LOGGER.info( + f'Found {len(branches)} branches using heuristic for node {node.id}: {shorten_hashes(node.id)}: {[self.kprint.pretty_print(bc) for bc in branches]}' + ) + return _LOGGER.info(f'Extending KCFG from node {self.id}: {shorten_hashes(node.id)}') _is_vacuous, depth, cterm, next_cterms, next_node_logs = self.cterm_execute(