Merge master into noah/node-attributes

Author: nwatson22

.github/workflows/test-pr.yml

@@ -104,7 +104,7 @@ jobs:
         with:
           install-k: true
       - name: 'Run integration tests'
-        run: make cov-integration COV_ARGS='-n4 --timeout 500'
+        run: make cov-integration COV_ARGS='-n4 --timeout 1500'
 
   regression-tests:
     needs: code-quality-checks

deps/k_release

@@ -1 +1 @@
-6.3.50
+6.3.58

docs/conf.py

@@ -9,8 +9,8 @@
 project = 'pyk'
 author = 'Runtime Verification, Inc'
 copyright = '2024, Runtime Verification, Inc'
-version = '0.1.729'
-release = '0.1.729'
+version = '0.1.731'
+release = '0.1.731'
 
 # -- General configuration ---------------------------------------------------
 # https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration

package/version

@@ -1 +1 @@
-0.1.729
+0.1.731

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pyk"
-version = "0.1.729"
+version = "0.1.731"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

src/pyk/__init__.py

@@ -6,4 +6,4 @@
     from typing import Final
 
 
-K_VERSION: Final = '6.3.50'
+K_VERSION: Final = '6.3.58'

src/pyk/testing/__init__.py

@@ -9,5 +9,6 @@
     KProveTest,
     KRunTest,
     RuntimeTest,
+    ServerType,
 )
 from ._profiler import Profiler

src/pyk/testing/_kompiler.py

@@ -167,7 +167,7 @@ class KoreClientTest(KompiledTest):
     KOMPILE_BACKEND: ClassVar = 'haskell'
     LLVM_ARGS: ClassVar[dict[str, Any]] = {}
 
-    CLIENT_TIMEOUT: ClassVar = 5000
+    CLIENT_TIMEOUT: ClassVar = 10000
 
     @pytest.fixture(scope='class', params=['legacy', 'booster'])
     def server_type(self, request: FixtureRequest, use_server: UseServer) -> ServerType:

src/tests/integration/kore/test_kore_client.py

@@ -32,6 +32,7 @@
     CutPointResult,
     DepthBoundResult,
     DuplicateModuleError,
+    GetModelResult,
     ImplicationError,
     ImpliesResult,
     InvalidModuleError,
@@ -47,7 +48,7 @@
 )
 from pyk.kore.syntax import And, App, Axiom, Bottom, Equals, EVar, Implies, Import, Module, Rewrites, Top
 from pyk.ktool.kompile import LLVMKompileType
-from pyk.testing import KoreClientTest
+from pyk.testing import KoreClientTest, ServerType
 
 from ..utils import K_FILES
 
@@ -56,7 +57,7 @@
     from pathlib import Path
     from typing import Any, Final
 
-    from pyk.kore.rpc import BoosterServerArgs, ExecuteResult, GetModelResult, KoreClient
+    from pyk.kore.rpc import BoosterServerArgs, ExecuteResult, KoreClient
     from pyk.kore.syntax import Pattern
     from pyk.testing import Kompiler
 
@@ -149,7 +150,15 @@ def state(n: int) -> State:
 
 GET_MODEL_TEST_DATA: Final = (
     ('unkown-config', term(0), None, UnknownResult()),
-    ('unknown-trivial', int_top, None, UnknownResult()),
+    (
+        'sat-trivial',
+        int_top,
+        None,
+        {
+            ServerType.LEGACY: UnknownResult(),
+            ServerType.BOOSTER: SatResult(None),
+        },
+    ),
     ('unsat-trivial', int_bottom, None, UnsatResult()),
     ('unsat-ineq', Equals(BOOL, INT, TRUE, and_bool(gt_int(x, int_dv(1)), le_int(x, int_dv(0)))), None, UnsatResult()),
     ('unsat-eq', Equals(BOOL, INT, TRUE, and_bool(eq_int(x, int_dv(0)), eq_int(x, int_dv(1)))), None, UnsatResult()),
@@ -345,13 +354,17 @@ def test_get_model(
         test_id: str,
         pattern: Pattern,
         module_name: str | None,
-        expected: GetModelResult,
+        server_type: ServerType,
+        expected: GetModelResult | Mapping[ServerType, GetModelResult],
     ) -> None:
         # When
         actual = kore_client.get_model(pattern, module_name)
 
         # Then
-        assert actual == expected
+        if isinstance(expected, GetModelResult):
+            assert actual == expected
+        else:
+            assert actual == expected[server_type]
 
     @pytest.mark.parametrize(
         'test_id,module',