From cf656e3ae59e90c09c7b97d0784b535e43767f9a Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Sat, 22 Aug 2026 16:17:03 +1000
Subject: [PATCH 1/3] Use default LLVM lib directory when resuming a proof
 without recompilation

Since the definition is not recompiled any more for specific programs with the LLVM backend, the `KompiledSymbolic` class always uses
the standard LLVM backend library from the semantics.precompiled definition.
The execution path for reloading a proof without having to re-process the definition.kore was still using a custom value where the
compiled LLVM backend library was previously stored.

To reproduce the bug:
1. Run a proof: `kmir prove my_program.rs --proof-dir fubar`
2. Re-run the proof (without `--reload`, same command as above)

The parameter for the LLVM backend library in `KompiledSymbolic` is maybe still used in other contexts but could be omitted for this use.
---
 kmir/src/kmir/kompile.py | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/kmir/src/kmir/kompile.py b/kmir/src/kmir/kompile.py
index b4b1c310d..74424821f 100644
--- a/kmir/src/kmir/kompile.py
+++ b/kmir/src/kmir/kompile.py
@@ -256,13 +256,12 @@ def kompile_smir(
     )
 
     target_hs_path = target_dir / 'haskell'
-    target_llvm_lib_path = target_dir / 'llvm-library'
     target_llvm_path = target_dir / 'llvm'
 
     if kompile_digest == expected_digest:
         _LOGGER.info(f'Kompiled SMIR up-to-date, no kompilation necessary: {target_dir}')
         if symbolic:
-            return KompiledSymbolic(haskell_dir=target_hs_path, llvm_lib_dir=target_llvm_lib_path)
+            return KompiledSymbolic(haskell_dir=target_hs_path, llvm_lib_dir=kdist.which(llvm_lib_target))
         else:
             return KompiledConcrete(llvm_dir=target_llvm_path)
 

From 0ca80d9c72e83e020e77aca24ea76856ec736e9a Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Sat, 22 Aug 2026 16:38:42 +1000
Subject: [PATCH 2/3] github test.yml: Remove invalid token from checkout
 actions

---
 .github/workflows/test.yml | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 5cd4fb0b4..0404d6fab 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -86,7 +86,6 @@ jobs:
       - name: 'Check out code'
         uses: actions/checkout@v4
         with:
-          token: ${{ secrets.JENKINS_GITHUB_PAT }}
           submodules: recursive
       - name: 'Set up Docker'
         uses: ./.github/actions/with-docker
@@ -110,7 +109,6 @@ jobs:
       - name: 'Check out code'
         uses: actions/checkout@v4
         with:
-          token: ${{ secrets.JENKINS_GITHUB_PAT }}
           submodules: recursive
       - name: 'Set up Docker'
         uses: ./.github/actions/with-docker
@@ -212,7 +210,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        runner: [normal, MacM1]  # MacM1 / normal are self-hosted, 
+        runner: [normal, MacM1]  # MacM1 / normal are self-hosted,
     runs-on: ${{ matrix.runner }}
     timeout-minutes: 20
     steps:
@@ -243,4 +241,3 @@ jobs:
           set -euxo pipefail
           nix --version
           nix flake check # build and run smoke test
-

From 166c4775dd89098fd246b55b62e26e4efa895fe2 Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Sat, 22 Aug 2026 16:40:36 +1000
Subject: [PATCH 3/3] github test.yml: bump checkout actions version to v7

---
 .github/workflows/test.yml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 0404d6fab..d833f286d 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -12,7 +12,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v4
+        uses: actions/checkout@v7
       - name: 'Get uv release'
         id: uv_release
         run: |
@@ -37,7 +37,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v4
+        uses: actions/checkout@v7
       - name: 'Get uv release'
         id: uv_release
         run: |
@@ -84,7 +84,7 @@ jobs:
             timeout: 60
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v4
+        uses: actions/checkout@v7
         with:
           submodules: recursive
       - name: 'Set up Docker'
@@ -107,7 +107,7 @@ jobs:
     runs-on: [self-hosted, linux, normal]
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v4
+        uses: actions/checkout@v7
         with:
           submodules: recursive
       - name: 'Set up Docker'
@@ -137,7 +137,7 @@ jobs:
       short-sha: ${{ steps.set-image-name.outputs.short-sha }}
     steps:
       - name: Checkout code
-        uses: actions/checkout@v4
+        uses: actions/checkout@v7
         with:
           submodules: recursive
 
@@ -215,7 +215,7 @@ jobs:
     timeout-minutes: 20
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v4
+        uses: actions/checkout@v7
         with:
           # Check out pull request HEAD instead of merge commit.
           ref: ${{ github.event.pull_request.head.sha }}