Prepare for KeY 2.12.4

.github/workflows/nightlydeploy.yml

@@ -3,7 +3,7 @@ name: Weekly Builds of KeY
 on:
   workflow_dispatch:
   schedule:
-    - cron:  '0 5 * * 1' # every monday morning
+    - cron: '0 5 * * 1' # every monday morning
 
 permissions:
   contents: write
@@ -12,7 +12,6 @@ permissions:
 env:
   JAVA_VERSION: 21
 
-
 jobs:
   build:
     runs-on: ubuntu-latest
@@ -24,84 +23,51 @@ jobs:
           java-version: ${{ env.JAVA_VERSION }}
           distribution: 'temurin'
           cache: 'gradle'
+          gpg-private-key: ${{ secrets.GPG_PRIVATE_KEY }}
+          gpg-passphrase: ${{ secrets.GPG_PASSPHRASE }}
 
       - name: Setup Gradle
         uses: gradle/actions/setup-gradle@v5
 
       - name: Build with Gradle
-        run: ./gradlew --parallel assemble
+        run: ./gradlew --parallel assemble javadoc alldoc
 
-  doc:
-    needs: [build]
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v6
-      - name: Set up JDK ${{ env.JAVA_VERSION }}
-        uses: actions/setup-java@v5
+      - name: Upload ShadowJar
+        uses: actions/upload-artifact@v7
         with:
-          java-version: ${{ env.JAVA_VERSION }}
-          distribution: 'temurin'
-          cache: 'gradle'
-
-      - name: Setup Gradle
-        uses: gradle/actions/setup-gradle@v5
-
-      - name: Build Documentation with Gradle
-        run: ./gradlew alldoc
+          name: shadowjars
+          path: "*/build/libs/*-exe.jar"
+          retention-days: 1
 
       - name: Package
         run: tar cvf key-javadoc.tar.xz build/docs/javadoc
 
-  deploy:
-    needs: [build, doc]
-    runs-on: ubuntu-latest
-    steps:
       - name: Upload Javadoc
         uses: actions/upload-artifact@v7
         with:
           name: javadoc
-          path: "javadoc.tar.xz"
-
-      - name: Upload ShadowJar
-        uses: actions/upload-artifact@v7
-        with:
-          name: shadowjars
-          path: "*/build/libs/*-exe.jar"
+          path: "key-javadoc.tar.xz"
+          retention-days: 1
 
       - name: Delete previous nightly release
         continue-on-error: true
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
         run: |
-          gh release delete nightly --yes --cleanup-tag 
+          gh release delete KEY-2.12.4-Release-Candidate --yes --cleanup-tag 
 
       - name: Create nightly release
         id: create_release
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-        run: |          
-          gh release create --generate-notes --title "Nightly Release" \
+        run: |
+          gh release create --generate-notes --title "KeY 2.12.4 Pre-Release" \
              --prerelease --notes-start-tag KEY-2.12.3 \
-             nightly key.ui/build/libs/key-*-exe.jar
-
-  deploy-maven:
-    needs: [ build, doc ]
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v6
-      - name: Set up JDK ${{ env.JAVA_VERSION }}
-        uses: actions/setup-java@v5
-        with:
-          java-version: ${{ env.JAVA_VERSION }}
-          distribution: 'temurin'
-          cache: 'gradle'
-
-      - name: Setup Gradle
-        uses: gradle/actions/setup-gradle@v5
+             KEY-2.12.4-Release-Candidate key.ui/build/libs/key-*-exe.jar key-javadoc.tar.xz
 
+      - run: export GPG_TTY=$(tty)
       - name: Upload to SNAPSHOT repository
-        run: ./gradlew publishMavenJavaPublicationToKEYLABRepository
+        run: ./gradlew --parallel publishMavenJavaPublicationToKEYLABRepository
         env:
           BUILD_NUMBER: "SNAPSHOT"
           GITLAB_DEPLOY_TOKEN: ${{ secrets.GITLAB_DEPLOY_TOKEN }}
-

LICENSE.TXT

@@ -3,7 +3,7 @@
        Copyright (C) 2001-2011 Universitaet Karlsruhe (TH), Germany
                                Universitaet Koblenz-Landau, Germany
                                Chalmers University of Technology, Sweden
-       Copyright (C) 2011-2019 Karlsruhe Institute of Technology, Germany
+       Copyright (C) 2011-2026 Karlsruhe Institute of Technology, Germany
                                Technical University Darmstadt, Germany
                                Chalmers University of Technology, Sweden
 

README.md

@@ -14,7 +14,7 @@ For more information, refer to
   * [Verification of `java.util.IdentityHashMap`](https://doi.org/10.1007/978-3-031-07727-2_4),
   * [Google Award for analysing a bug in `LinkedList`](https://www.key-project.org/2023/07/23/cwi-researchers-win-google-award-for-finding-a-bug-in-javas-linkedlist-using-key/)
 
-The current version of KeY is 2.12.2, licensed under GPL v2.
+The current version of KeY is 2.12.4, licensed under GPL v2.
 
 
 Feel free to use the project templates to get started using KeY:

key.core/src/main/java/de/uka/ilkd/key/java/reference/MethodReference.java

@@ -355,7 +355,8 @@ public void visit(Visitor v) {
     public KeYJavaType getKeYJavaType(Services services, ExecutionContext ec) {
         IProgramMethod meth = method(services, determineStaticPrefixType(services, ec), ec);
         if (meth == null) {
-            return ec.getTypeReference().getKeYJavaType();
+            throw new IllegalStateException(
+                "Could not determine type for method " + name.toString());
         }
         return meth.getReturnType();
 

key.core/src/main/java/de/uka/ilkd/key/logic/TermBuilder.java

@@ -157,14 +157,38 @@ public String newName(String baseName, NamespaceSet localNamespace) {
             return savedName.toString();
         }
 
+        final String result = freeName(baseName, localNamespace, null);
+
+        services.getNameRecorder().addProposal(new Name(result));
+
+        return result;
+    }
+
+    /**
+     * Returns the first name out of {@code baseName, baseName_0, baseName_1, ...} that is neither
+     * present in {@code localNamespace} nor contained in {@code taken}.
+     * <p>
+     * This is the side-effect-free core of the "find a fresh name" loop: it neither touches the
+     * name recorder nor advances any counter,
+     * so the result depends only on the supplied namespaces and the {@code taken} set. That makes
+     * it safe to call from contexts that run during (speculative) taclet matching, where a
+     * mutable side effect would render the result non-deterministic across proof reloads (see
+     * {@link de.uka.ilkd.key.rule.conditions.NewLocalVarsCondition} / issue #3834).
+     *
+     * @param baseName the base name (prefix)
+     * @param localNamespace the namespaces to check for collisions
+     * @param taken additional names to avoid (may be {@code null}); useful when several fresh
+     *        names are generated before any of them is registered in the namespaces
+     * @return a name not occurring in {@code localNamespace} or {@code taken}
+     */
+    public static String freeName(String baseName, NamespaceSet localNamespace,
+            java.util.Set<String> taken) {
         int i = 0;
         String result = baseName;
-        while (localNamespace.lookup(new Name(result)) != null) {
+        while (localNamespace.lookup(new Name(result)) != null
+                || (taken != null && taken.contains(result))) {
             result = baseName + "_" + i++;
         }
-
-        services.getNameRecorder().addProposal(new Name(result));
-
         return result;
     }
 

key.core/src/main/java/de/uka/ilkd/key/logic/VariableNamer.java

@@ -380,7 +380,14 @@ protected ProgramElementName getNameProposalForSchemaVariable(String basename,
                         collision = false;
                         for (String previousProposal : previousProposals) {
                             if (previousProposal.equals(result.toString())) {
-                                result = createName(basename, ++cnt, null);
+                                cnt += 1;
+                                result = createName(basename, cnt, null);
+
+                                while (services.getNamespaces().lookupLogicSymbol(result) != null) {
+                                    cnt += 1;
+                                    result = createName(basename, cnt, null);
+                                }
+
                                 collision = true;
                                 break;
                             }

key.core/src/main/java/de/uka/ilkd/key/proof/VariableNameProposer.java

@@ -138,7 +138,7 @@ private String getNameProposalForSkolemTermVariable(String name, Services servic
             name = basename + cnt;
             l_name = new Name(name);
             cnt++;
-        } while (nss.lookup(l_name) != null && !previousProposals.contains(name));
+        } while (nss.lookup(l_name) != null || previousProposals.contains(name));
 
 
         return name;

key.core/src/main/java/de/uka/ilkd/key/proof/io/UrlRuleSource.java

@@ -61,11 +61,11 @@ public Path file() {
             try {
                 return Paths.get(uri);
             } catch (FileSystemNotFoundException e) {
-                URI rootFs = URI.create(StringUtil.takeUntil(uri.toString(), "\\!"));
-                String internal = StringUtil.takeAfter(uri.toString(), "\\!");
-                try (FileSystem zipfs = FileSystems.newFileSystem(rootFs, new HashMap<>())) {
-                    return zipfs.getPath(internal);
-                }
+                URI rootFs = URI.create(StringUtil.takeUntil(uri.toString(), "!"));
+                String internal = StringUtil.takeAfter(uri.toString(), "!");
+                // keep the file system open.
+                FileSystem zipfs = FileSystems.newFileSystem(rootFs, new HashMap<>());
+                return zipfs.getPath(internal);
             }
         } catch (URISyntaxException | IOException e) {
             throw new RuntimeException(e);

key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewLocalVarsCondition.java

@@ -4,7 +4,9 @@
 package de.uka.ilkd.key.rule.conditions;
 
 import java.util.ArrayList;
+import java.util.HashSet;
 import java.util.List;
+import java.util.Set;
 
 import de.uka.ilkd.key.java.ProgramElement;
 import de.uka.ilkd.key.java.Services;
@@ -16,6 +18,8 @@
 import de.uka.ilkd.key.java.declaration.VariableSpecification;
 import de.uka.ilkd.key.java.reference.TypeRef;
 import de.uka.ilkd.key.logic.JTerm;
+import de.uka.ilkd.key.logic.ProgramElementName;
+import de.uka.ilkd.key.logic.TermBuilder;
 import de.uka.ilkd.key.logic.op.LocationVariable;
 import de.uka.ilkd.key.rule.inst.SVInstantiations;
 import de.uka.ilkd.key.util.MiscTools;
@@ -85,9 +89,18 @@ public MatchResultInfo check(SchemaVariable var, SyntaxElement instCandidate,
         ImmutableList<JTerm> updatesBefore = ImmutableSLList.nil();
         ImmutableList<JTerm> updatesFrame = ImmutableSLList.nil();
         var tb = services.getTermBuilder();
+        // Names of "before" variables generated within this single application; needed because
+        // the new variables are not yet registered in the namespaces while we build them.
+        final Set<String> reserved = new HashSet<>();
         for (var v : vars) {
-            final var newName =
-                services.getVariableNamer().getTemporaryNameProposal(v.name() + "_before");
+            // Deterministically derive a unique name from the current proof state instead of
+            // using getVariableNamer().getTemporaryNameProposal(), which appends a '#'-index
+            // taken from a proof-global counter. That counter is advanced as a side effect of
+            // (speculative) taclet matching, so the number of increments differs between a
+            // freshly created proof and a reloaded/pruned-and-reapplied one. The resulting name
+            // mismatch (e.g. k_before#0 vs. k_before#1) breaks the slicing mechanism, which
+            // relies on formula equivalence across reloads. See issue #3834.
+            final var newName = uniqueBeforeName(v.name() + "_before", services, reserved);
             KeYJavaType type = v.getKeYJavaType();
             var locVar = new LocationVariable(newName, type);
             var spec = new VariableSpecification(locVar);
@@ -109,6 +122,28 @@ public MatchResultInfo check(SchemaVariable var, SyntaxElement instCandidate,
                     .add(updateFrameSV, tb.parallel(updatesFrame), services));
     }
 
+    /**
+     * Produces a fresh {@link ProgramElementName} for a "before" variable that is deterministic
+     * w.r.t. the current proof state. The name is unique with respect to all current namespaces of
+     * {@code services} as well as the names already handed out within the current rule application
+     * ({@code reserved}). Unlike
+     * {@link de.uka.ilkd.key.logic.VariableNamer#getTemporaryNameProposal(String)}, this does not
+     * depend on a mutable proof-global counter, so it stays stable across proof reloads and
+     * prune/reapply cycles (issue #3834).
+     *
+     * @param basename the desired base name, e.g. {@code "k_before"}
+     * @param services the services whose namespaces are consulted for collisions
+     * @param reserved names already used within the current application; the chosen name is added
+     * @return a fresh, collision-free name
+     */
+    private static ProgramElementName uniqueBeforeName(String basename, Services services,
+            Set<String> reserved) {
+        final String candidate =
+            TermBuilder.freeName(basename, services.getNamespaces(), reserved);
+        reserved.add(candidate);
+        return new ProgramElementName(candidate);
+    }
+
     @Override
     public String toString() {
         return "\\newLocalVars(" + varDeclsSV + ", " + updateBeforeSV + ", " + updateFrameSV + ", "