runtimeverification · rv-jenkins · Sep 8, 2023 · Sep 5, 2023 · Sep 5, 2023 · Sep 6, 2023
diff --git a/deps/k_release b/deps/k_release
@@ -1 +1 @@
-6.0.69
+6.0.87
diff --git a/package/version b/package/version
@@ -1 +1 @@
-0.1.436
+0.1.437
diff --git a/pyproject.toml b/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pyk"
-version = "0.1.436"
+version = "0.1.437"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git a/src/pyk/__init__.py b/src/pyk/__init__.py
@@ -6,4 +6,4 @@
     from typing import Final
 
 
-K_VERSION: Final = '6.0.69'
+K_VERSION: Final = '6.0.87'
diff --git a/src/pyk/cterm.py b/src/pyk/cterm.py
@@ -110,7 +110,11 @@ def _is_bottom(kast: KInner) -> bool:
         flat = flatten_label('#And', kast)
         if len(flat) == 1:
             return is_bottom(single(flat))
-        return all(CTerm._is_bottom(term) for term in flat)
+        return any(CTerm._is_bottom(term) for term in flat)
+
+    @property
+    def is_bottom(self) -> bool:
+        return CTerm._is_bottom(self.config) or any(CTerm._is_bottom(cterm) for cterm in self.constraints)
 
     @staticmethod
     def _constraint_sort_key(term: KInner) -> tuple[int, str]:

diff --git a/src/pyk/kcfg/explore.py b/src/pyk/kcfg/explore.py
@@ -93,6 +93,7 @@ def cterm_execute(
         next_state = CTerm.from_kast(self.kprint.kore_to_kast(er.state.kore))
         _next_states = er.next_states if er.next_states is not None else []
         next_states = [CTerm.from_kast(self.kprint.kore_to_kast(ns.kore)) for ns in _next_states]
+        next_states = [cterm for cterm in next_states if not cterm.is_bottom]
         if len(next_states) == 1 and len(next_states) < len(_next_states):
             return depth + 1, next_states[0], [], er.logs
         elif len(next_states) == 1:
Original file line number	Diff line number	Diff line change
Expand Up		@@ -6,4 +6,4 @@
		from typing import Final


		K_VERSION: Final = '6.0.69'
		K_VERSION: Final = '6.0.87'