diff --git a/LICENSE.TXT b/LICENSE.TXT
index dbafedb51f2..1a701bdf921 100644
--- a/LICENSE.TXT
+++ b/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
 
diff --git a/README.md b/README.md
index 993387c3307..afefe0b4eff 100644
--- a/README.md
+++ b/README.md
@@ -2,6 +2,7 @@
 
 [![Tests](https://github.com/KeYProject/key/actions/workflows/tests.yml/badge.svg)](https://github.com/KeYProject/key/actions/workflows/tests.yml) [![CodeQuality](https://github.com/KeYProject/key/actions/workflows/code_quality.yml/badge.svg)](https://github.com/KeYProject/key/actions/workflows/code_quality.yml)
 
+![Maven metadata URL](https://img.shields.io/maven-metadata/v?metadataUrl=https%3A%2F%2Fcentral.sonatype.com%2Frepository%2Fmaven-snapshots%2Forg%2Fkey-project%2Fkey.core%2Fmaven-metadata.xml&label=maven%20snapshots)
 ![Maven metadata URL](https://img.shields.io/maven-metadata/v?metadataUrl=https%3A%2F%2Frepo1.maven.org%2Fmaven2%2Forg%2Fkey-project%2Fkey.core%2Fmaven-metadata.xml&label=maven%20central)
 
 
@@ -29,7 +30,7 @@ Feel free to use the project templates to get started using KeY:
 
 * Hardware: >=2 GB RAM
 * Operating System: Linux/Unix, MacOSX, Windows
-* Java 21 or newer
+* Java 17 or newer
 * Optionally, KeY can make use of the following binaries:
   * SMT Solvers:
     * [Z3](https://github.com/Z3Prover/z3#z3)
diff --git a/build.gradle b/build.gradle
index 87ffcd8eb76..b6a7211b062 100644
--- a/build.gradle
+++ b/build.gradle
@@ -19,8 +19,20 @@ plugins {
 
     // Plugin for publishing via the new Nexus API
     alias(libs.plugins.maven.publish) apply false
+
+    //alias(libs.plugins.license.report)
 }
 
+/* // required for generated the license report THIRD_PARTY_LICENSES.txt
+licenseReport {
+    unionParentPomLicenses = false
+    outputDir = layout.buildDirectory.dir("licenses").get().asFile
+    projects = [project] + project.subprojects
+    configurations = ['runtimeClasspath']
+    excludeOwnGroup = true
+    excludeBoms = false
+}
+*/
 
 // Configure this project for use inside IntelliJ:
 idea {
@@ -46,6 +58,8 @@ subprojects {
     apply plugin: "idea"
     apply plugin: "eclipse"
 
+//    apply plugin: libs.plugins.license.report
+
     apply plugin: "com.diffplug.spotless"
     apply plugin: "org.checkerframework"
     apply plugin: "com.vanniktech.maven.publish"
@@ -299,7 +313,11 @@ subprojects {
 
         pom {
             name = project.name
-            description = project.description
+            afterEvaluate {
+                description = project.description
+                assert (project.description != null && project.description != "") : "Description of modules are required at maven-central"
+                print(project.description)
+            }
             url = 'https://key-project.org/'
 
             licenses {
diff --git a/gradle.properties b/gradle.properties
index 7937f1c737f..e12aa899dbf 100644
--- a/gradle.properties
+++ b/gradle.properties
@@ -1 +1,4 @@
-org.gradle.jvmargs=-Xmx2g -XX:MaxMetaspaceSize=512m -Dfile.encoding=UTF-8
\ No newline at end of file
+org.gradle.jvmargs=-Xmx2g -XX:MaxMetaspaceSize=512m -Dfile.encoding=UTF-8
+
+# do not release automatically at Maven Central
+mavenCentralAutomaticPublishing=false
diff --git a/gradle/libs.versions.toml b/gradle/libs.versions.toml
index e87424ba15a..3e5c71cc9f9 100644
--- a/gradle/libs.versions.toml
+++ b/gradle/libs.versions.toml
@@ -98,3 +98,4 @@ spotless = { id = "com.diffplug.spotless", version.ref = "spotless" }
 checkerframework = { id = "org.checkerframework", version.ref = "checkerframework-gradle" }
 maven-publish = { id = "com.vanniktech.maven.publish", version.ref = "maven-publish" }
 shadow = { id = "com.gradleup.shadow", version.ref = "shadow" }
+license-report = { id = "com.github.jk1.dependency-license-report", version = "3.1.4" }
\ No newline at end of file
diff --git a/key.core.infflow/build.gradle b/key.core.infflow/build.gradle
index 208feccfd64..a5d119bc749 100644
--- a/key.core.infflow/build.gradle
+++ b/key.core.infflow/build.gradle
@@ -1,3 +1,4 @@
+description = "Information-Flow / Non-interference calculus for Java using the KeY theorem prover"
 
 
 dependencies {
diff --git a/key.core.wd/build.gradle b/key.core.wd/build.gradle
index ccf546b22cc..233b71c8d66 100644
--- a/key.core.wd/build.gradle
+++ b/key.core.wd/build.gradle
@@ -1,3 +1,6 @@
+description = "Well-defined calculus for JML specifciation and Java using the KeY theorem prover"
+
+
 dependencies {
     api(project(":key.core"))
 
diff --git a/key.core/src/main/java/de/uka/ilkd/key/control/InstantiationFileHandler.java b/key.core/src/main/java/de/uka/ilkd/key/control/InstantiationFileHandler.java
index a19b7ae7be3..846b2974dc7 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/control/InstantiationFileHandler.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/control/InstantiationFileHandler.java
@@ -5,8 +5,7 @@
 
 import java.io.*;
 import java.nio.charset.StandardCharsets;
-import java.nio.file.Files;
-import java.nio.file.Path;
+import java.nio.file.*;
 import java.util.*;
 
 import de.uka.ilkd.key.control.instantiation_model.TacletFindModel;
@@ -33,30 +32,44 @@ public class InstantiationFileHandler {
 
     private static Map<String, List<List<String>>> hm;
 
-    /// Finds the current place to store used instantiation. If there was a version switch
+    /// Finds the current place to store used instantiations. If there was a version change
     /// (the folder does not exist), this method tries to copy previous instantiations to
-    /// the new directory silently.
-    ///
-    /// It is guaranteed, that the folder exists.
+    /// the new directory silently. However, if both old and new instantiations exist, they are not
+    /// merge, i.e. only the new ones are used currently.
     private static Path getStoragePath() {
         Path cur = PathConfig.currentPaths.keyConfigDir.resolve("instantiations");
         if (Files.exists(cur)) {
+            /*
+             * At the moment, we do not merge when old and new instantiations are
+             * present. In the future, we could go one step further and try to merge.
+             */
             return cur;
         }
-
-        Path prev = PathConfig.previousPaths.keyConfigDir.resolve("instantiations");
+        // create the directory for storing instantiations
         try {
             Files.createDirectories(cur);
+        } catch (IOException e) {
+            LOGGER.warn("Could not create the instantiations folder {}", cur, e);
+        }
+
+        // Check if instantiations from older key version exist. If so, try to copy them over.
+        Path prev = PathConfig.previousPaths.keyConfigDir.resolve("instantiations");
+        if (Files.exists(prev)) {
             try (var files = Files.walk(prev)) {
                 files.forEach(path -> {
                     try {
-                        Files.copy(path, cur.resolve(path.relativize(prev)));
-                    } catch (IOException ignore) {
+                        Path target = cur.resolve(prev.relativize(path));
+                        // Do not overwrite existing file!
+                        if (!Files.exists(target)) {
+                            Files.copy(path, target);
+                        }
+                    } catch (IOException inner) {
+                        LOGGER.warn("Could not copy instantiation file {}", path, inner);
                     }
                 });
+            } catch (IOException e) {
+                LOGGER.warn("Could not copy instantiation files from {} to {}", prev, cur, e);
             }
-        } catch (IOException e) {
-            throw new RuntimeException(e);
         }
         return cur;
     }
@@ -82,9 +95,9 @@ private static void createHashMap() {
         hm = new TreeMap<>();
         try (var stream = Files.list(INSTANTIATION_DIR)) {
             // using a TreeMap here avoids non-determinsm introduce by the file system.
-            stream.forEach(file -> hm.put(file.toString(), null));
+            stream.forEach(file -> hm.put(file.getFileName().toString(), null));
         } catch (IOException e) {
-            LOGGER.warn("Could not read the instantions folder {}", INSTANTIATION_DIR, e);
+            LOGGER.warn("Could not read the instantiations folder {}", INSTANTIATION_DIR, e);
         }
     }
 
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/InitConfig.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/InitConfig.java
index 9b2da179fb6..281cdc20579 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/InitConfig.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/InitConfig.java
@@ -80,6 +80,7 @@ public class InitConfig {
 
     /** HashMap for quick lookups taclet name->taclet */
     private Map<Name, Taclet> activatedTacletCache = null;
+    private boolean defaultsComputed;
 
     /** the fileRepo which is responsible for consistency between source code and proof */
     private FileRepo fileRepo;
@@ -104,6 +105,9 @@ public InitConfig(Services services) {
     /// combines the found choices in KeY files, together with the current settings.
     /// The namespace of choices has to be filled.
     public void computeDefaults(ChoiceInformation ci) {
+        if (defaultsComputed) {
+            return;
+        }
         var currentDefaultChoices =
             ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().getDefaultChoices();
 
@@ -145,6 +149,8 @@ public void computeDefaults(ChoiceInformation ci) {
             }
             settings.getChoiceSettings().setDefaultChoices(defaults);
         }
+        activatedTacletCache = null;
+        defaultsComputed = true;
     }
 
     /**
@@ -203,6 +209,14 @@ public Map<Taclet, TacletBuilder<? extends Taclet>> getTaclet2Builder() {
     }
 
 
+    /**
+     * @return an immutable mapping from a category to its default choice
+     */
+    public @NonNull Map<String, Choice> getCategory2DefaultChoices() {
+        return Collections.unmodifiableMap(category2DefaultChoice);
+    }
+
+
     /**
      * sets the set of activated choices of this initial configuration. For categories without a
      * specified choice the default choice contained in category2DefaultChoice is added.
@@ -448,6 +462,7 @@ public InitConfig copyWithServices(Services services) {
         ic.header = header;
         ic.justifInfo = justifInfo.copy();
         ic.fileRepo = fileRepo; // TODO: copy instead? delete via dispose method?
+        ic.defaultsComputed = defaultsComputed;
         return ic;
     }
 
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java
index f60e1578a60..ffea403696b 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java
@@ -23,6 +23,7 @@
 import de.uka.ilkd.key.logic.label.OriginTermLabelFactory;
 import de.uka.ilkd.key.logic.op.*;
 import de.uka.ilkd.key.logic.sort.GenericSort;
+import de.uka.ilkd.key.nparser.ChoiceInformation;
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.JavaModel;
 import de.uka.ilkd.key.proof.Proof;
@@ -392,11 +393,14 @@ private void populateNamespaces(Proof proof) {
         }
     }
 
-    // what is the purpose of this method?
+    /**
+     * Updates the global settings the taclet options that declared in
+     * {@code optionDeclaration.key}.
+     * A proof created afterwards inherits these settings unless it overwrites it.
+     */
     private InitConfig determineEnvironment(ProofOblInput po, InitConfig initConfig) {
-        // TODO: what does this actually do?
         ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().updateChoices(initConfig.choiceNS(),
-            false);
+            initConfig.getCategory2DefaultChoices(), false);
         return initConfig;
     }
 
@@ -505,7 +509,7 @@ public InitConfig prepare(EnvInput envInput) throws ProofInputException {
         var warnings = ic.getProfile()
                 .prepareInitConfig(ic, additionalProfileOptions);
         addWarnings(warnings);
-
+        ic.computeDefaults(new ChoiceInformation());
         return ic;
     }
 
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/KeYFile.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/KeYFile.java
index 29fe353e691..53a53f3218d 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/KeYFile.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/KeYFile.java
@@ -256,7 +256,7 @@ public Path readBootClassPath() {
         if (!bootClassPathFile.isAbsolute()) {
             // convert to absolute by resolving against the parent path of the parsed file
             Path parentDirectory = file.file().getParent();
-            bootClassPathFile = parentDirectory.resolve(bootClassPathFile);
+            bootClassPathFile = parentDirectory.resolve(bootClassPathFile).normalize();
         }
         if (!Files.isDirectory(bootClassPathFile)) {
             // Report the missing directory at the \bootclasspath declaration in the .key file,
@@ -297,7 +297,7 @@ private static Location locationOrUndefined(ProblemInformation pi, String path)
             } else {
                 var f = Paths.get(normalizeStoredPath(cp));
                 if (!f.isAbsolute()) {
-                    f = parentDirectory.resolve(f);
+                    f = parentDirectory.resolve(f).normalize();
                 }
                 if (!Files.exists(f)) {
                     // Point at the \classpath declaration in the .key file instead of letting the
@@ -321,7 +321,7 @@ public Path readJavaPath() throws ProofInputException {
             if (!absFile.isAbsolute()) {
                 // convert to absolute by resolving against the parent path of the parsed file
                 Path parent = file.file().getParent();
-                absFile = parent.resolve(javaPath);
+                absFile = parent.resolve(javaPath).normalize();
             }
             if (!Files.exists(absFile)) {
                 throw new ProofInputException(String.format(
diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/ChoiceSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/ChoiceSettings.java
index 9ecfe75f261..3cd1dc3dab2 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/settings/ChoiceSettings.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/settings/ChoiceSettings.java
@@ -97,9 +97,12 @@ public void setChoiceCategories(Map<String, Set<String>> c2C) {
      * updates <code>category2Choices</code> if new entries are found in <code>choiceNS</code> or if
      * entries of <code>category2Choices</code> are no longer present in <code>choiceNS</code>
      *
+     * @param choiceNS the choices declared by the loaded problem file
+     * @param defaults the default choice of each category
      * @param remove remove entries not present in <code>choiceNS</code>
      */
-    public void updateChoices(Namespace<Choice> choiceNS, boolean remove) {
+    public void updateChoices(Namespace<Choice> choiceNS, Map<String, Choice> defaults,
+            boolean remove) {
         // Translate the given namespace into a map of 'string -> list[string]'
         HashMap<String, Set<String>> c2C = new LinkedHashMap<>();
         for (Choice c : choiceNS.allElements()) {
@@ -118,11 +121,11 @@ public void updateChoices(Namespace<Choice> choiceNS, boolean remove) {
             }
         }
 
+        // ensure that default values are set if a key is present
         var defaultTmp = new HashMap<>(category2Default);
         for (var pair : category2Default.entrySet()) {
             var s = pair.getKey();
             var v = pair.getValue();
-            // if key is known then the default value should exist
             if (category2Choices.containsKey(s)) {
                 if (!category2Choices.get(s).contains(v)) {
                     defaultTmp.put(s, category2Choices.get(s).iterator().next());
@@ -131,6 +134,16 @@ public void updateChoices(Namespace<Choice> choiceNS, boolean remove) {
                 defaultTmp.remove(s);
             }
         }
+
+        for (var category : category2Choices.keySet()) {
+            if (!defaultTmp.containsKey(category)) {
+                var declared = defaults.get(category);
+                if (declared != null) {
+                    defaultTmp.put(category, declared.name().toString());
+                }
+            }
+        }
+
         setDefaultChoices(defaultTmp);
     }
 
diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/ProofSettings.java
index 7c855368250..f4ba250d607 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofSettings.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/settings/ProofSettings.java
@@ -229,7 +229,7 @@ public void loadSettings() {
                     loadSettingsFromJSONStream(in);
                 }
             } catch (Exception e) {
-                LOGGER.warn("No proof-settings could be loaded, using defaults", e);
+                LOGGER.warn("No proof settings could be loaded, using defaults");
             }
         }
     }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/KeYConstants.java b/key.core/src/main/java/de/uka/ilkd/key/util/KeYConstants.java
index ad764324f60..5a5f59039bc 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/util/KeYConstants.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/util/KeYConstants.java
@@ -10,6 +10,6 @@ public interface KeYConstants {
         KeYResourceManager.getManager().getVersion() + " (internal: " + INTERNAL_VERSION + ")";
 
     String COPYRIGHT = UnicodeHelper.COPYRIGHT + " Copyright 2001"
-        + UnicodeHelper.ENDASH + "2024 " + "Karlsruhe Institute of Technology, "
+        + UnicodeHelper.ENDASH + "2026 " + "Karlsruhe Institute of Technology, "
         + "Chalmers University of Technology, and Technische Universit\u00e4t Darmstadt";
 }
diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java
index 236fe99821b..8447fa0bb7c 100644
--- a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java
+++ b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java
@@ -212,9 +212,10 @@ public static ProofCollection automaticJavaDL() throws IOException {
          * If the fork mode is not set to noFork, the launched subprocesses
          * get the specified amount of heap memory.
          *
-         * Heap memory for subprocesses (like 500m or 2G)
+         * Heap memory for subprocesses (like 500m or 3G)
          */
-        // forkMemory = 1000m
+        settings.setForkMemory("3g");
+
 
         /*
          * To run the forked JVM in debug mode, set the TCP port to listen to here.
diff --git a/key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/TestFile.java b/key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/TestFile.java
index fa70826f758..cd7e6f53bc1 100644
--- a/key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/TestFile.java
+++ b/key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/TestFile.java
@@ -256,6 +256,7 @@ protected void reload(boolean verbose, Path proofFile, Proof loadedProof, boolea
         if (settings.reloadEnabled() && (testProperty == TestProperty.PROVABLE) && success) {
             // Save the available proof to a temporary file.
             ProofSaver.saveToFile(proofFile, loadedProof);
+            loadedProof.dispose();
             reloadProof(proofFile);
             if (verbose) {
                 LOGGER.debug("... success: reloaded.");
diff --git a/key.ncore.calculus/build.gradle b/key.ncore.calculus/build.gradle
index e54af4cf6bb..c2a26ef8629 100644
--- a/key.ncore.calculus/build.gradle
+++ b/key.ncore.calculus/build.gradle
@@ -1,3 +1,5 @@
+description = "Pattern Matchern New core KeY theorem prover"
+
 repositories {
     mavenCentral()
 }
diff --git a/key.ncore.matcher/build.gradle b/key.ncore.matcher/build.gradle
index 0ae89f3256f..a4014c8f4ec 100644
--- a/key.ncore.matcher/build.gradle
+++ b/key.ncore.matcher/build.gradle
@@ -1,6 +1,4 @@
-repositories {
-    mavenCentral()
-}
+description = "Compiling Matching Algorithm of the KeY theorem prover"
 
 dependencies {
     api project(':key.util')
diff --git a/key.ui/examples/heap/FM2024Tutorial/ArrayList/src/List.java b/key.ui/examples/heap/FM2024Tutorial/ArrayList/src/List.java
index 9b7b769942b..15a08b41876 100644
--- a/key.ui/examples/heap/FM2024Tutorial/ArrayList/src/List.java
+++ b/key.ui/examples/heap/FM2024Tutorial/ArrayList/src/List.java
@@ -5,7 +5,7 @@ public interface List {
 
     //@ public instance invariant \subset(\singleton(this.seq), footprint);
     //@ public instance invariant \subset(\singleton(this.footprint), footprint);
-    //@ public accessible \inv: footprint;
+    //@ accessible \inv: footprint;
 
     /*@ public normal_behaviour
       @   requires 0 <= index && index < seq.length;
diff --git a/key.ui/examples/newBook/Chapter_16/Sort/Sort.java b/key.ui/examples/newBook/Chapter_16/Sort/Sort.java
index 4a14d0923e1..29fe71ab084 100644
--- a/key.ui/examples/newBook/Chapter_16/Sort/Sort.java
+++ b/key.ui/examples/newBook/Chapter_16/Sort/Sort.java
@@ -6,7 +6,7 @@ public class Sort {
       @ ensures (\forall int i; start <= i && i<a.length;a[\result] >= a[i]);
       @ ensures start <= \result && \result < a.length;
       @ */
-    int /*@ strictly_pure @*/ max(int start) {
+    /*@ strictly_pure @*/ int max(int start) {
         int counter = start; int idx = start;
         /*@ loop_invariant  start<=counter && counter<=a.length
           @              && start<=idx && idx<a.length  && start<a.length
diff --git a/key.ui/examples/newBook/Chapter_16/SortPerm/SortPerm.java b/key.ui/examples/newBook/Chapter_16/SortPerm/SortPerm.java
index b254d1c46bf..62ae1868fd0 100644
--- a/key.ui/examples/newBook/Chapter_16/SortPerm/SortPerm.java
+++ b/key.ui/examples/newBook/Chapter_16/SortPerm/SortPerm.java
@@ -10,7 +10,7 @@ public class SortPerm {
       @ ensures (\forall int i;start<=i && i<a.length; a[\result] >= a[i]);
       @ ensures start <= \result && \result < a.length;
       @*/
-    int /*@ strictly_pure @*/ max(int start) {
+    /*@ strictly_pure @*/ int max(int start) {
         int counter = start;
         int idx = start;
         /*@ loop_invariant start<=counter && counter<=a.length
diff --git a/key.ui/examples/standard_key/java_dl/payCardJML/paycard/LimitedIntContainer.java b/key.ui/examples/standard_key/java_dl/payCardJML/paycard/LimitedIntContainer.java
index 6100333c72c..6882d449cc3 100644
--- a/key.ui/examples/standard_key/java_dl/payCardJML/paycard/LimitedIntContainer.java
+++ b/key.ui/examples/standard_key/java_dl/payCardJML/paycard/LimitedIntContainer.java
@@ -12,5 +12,5 @@ public interface LimitedIntContainer {
     /*@ public normal_behavior
       @   ensures regularState ==> \result == value;
       @*/
-    int /*@ pure @*/ available(); 
+    /*@ pure @*/ int available();
 }
diff --git a/key.ui/examples/standard_key/visualdebugger/src/paycard/LimitedIntContainer.java b/key.ui/examples/standard_key/visualdebugger/src/paycard/LimitedIntContainer.java
index a70776551c7..57ed1721678 100644
--- a/key.ui/examples/standard_key/visualdebugger/src/paycard/LimitedIntContainer.java
+++ b/key.ui/examples/standard_key/visualdebugger/src/paycard/LimitedIntContainer.java
@@ -10,6 +10,6 @@ public interface LimitedIntContainer{
     /*@ public normal_behavior
       @   ensures regularState ==> \result == value;
       @*/
-    int /*@ pure @*/ available(); 
+    /*@ pure @*/ int available();
 
 }
diff --git a/key.ui/src/main/java/de/uka/ilkd/key/core/Main.java b/key.ui/src/main/java/de/uka/ilkd/key/core/Main.java
index 5d41c039641..0b144d16d38 100644
--- a/key.ui/src/main/java/de/uka/ilkd/key/core/Main.java
+++ b/key.ui/src/main/java/de/uka/ilkd/key/core/Main.java
@@ -12,6 +12,7 @@
 import java.util.List;
 import java.util.Locale;
 import java.util.concurrent.Callable;
+import java.util.prefs.Preferences;
 import javax.xml.parsers.ParserConfigurationException;
 
 import de.uka.ilkd.key.control.UserInterfaceControl;
@@ -132,6 +133,9 @@ public final class Main implements Callable<Integer> {
     @Option(names = "--debug", description = "start KeY in debug mode")
     private boolean debug = false;
 
+    @Option(names = "--clear-prefs", description = "clear the GUI preferences")
+    private boolean clearPrefs = false;
+
     @Option(names = "--macro", paramLabel = "STRING", description = "apply automatic proof macro")
     private @Nullable String macro = null;
 
@@ -258,6 +262,17 @@ public Integer call() throws Exception {
             LOGGER.info("Assertion evaluation is enabled.");
         }
 
+        if (clearPrefs) {
+            try {
+                var prefs = Preferences.userNodeForPackage(MainWindow.class);
+                if (prefs != null) {
+                    prefs.clear();
+                }
+            } finally {
+                // nothing to do
+            }
+        }
+
         if (tacletDir != null) {
             System.setProperty(RuleSourceFactory.STD_TACLET_DIR_PROP_KEY,
                 tacletDir.toAbsolutePath().toString());
diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java
index 2487d19eb5b..9efdb7fac14 100644
--- a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java
+++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java
@@ -332,7 +332,14 @@ private MainWindow() {
         notificationManager = new NotificationManager(mediator, this);
         recentFileMenu = new RecentFileMenu(this);
         // Postpone load for faster UI creation.
-        SwingUtilities.invokeLater(recentFileMenu::loadEntries);
+        SwingUtilities.invokeLater(() -> {
+            recentFileMenu.loadEntries();
+            // otherwise open most recent cannot be used with a fresh started KeY
+            if (openMostRecentFileAction != null) {
+                // should always be the case, but better safe than sorry
+                openMostRecentFileAction.updateEnabledStatus();
+            }
+        });
 
         proofTreeView = new ProofTreeView(mediator);
         infoView = new InfoView(mediator);
diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java
index 1416a019c2a..7c645310d72 100644
--- a/key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java
+++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java
@@ -183,7 +183,7 @@ public JMenu getMenu() {
     /**
      * read the recent files from the given properties file
      */
-    public final void loadFrom(Path filename) {
+    final void loadFrom(Path filename) {
         try {
             if (!Files.exists(filename)) {
                 return;
diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/AboutAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/AboutAction.java
index a1f5b133083..1fb5cb65aa3 100644
--- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/AboutAction.java
+++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/AboutAction.java
@@ -22,7 +22,6 @@ public AboutAction(MainWindow mainWindow) {
         super(mainWindow);
         setName("About KeY");
         setIcon(IconFactory.help(16));
-        // About KeY
     }
 
     @Override
@@ -31,21 +30,10 @@ public void actionPerformed(ActionEvent e) {
     }
 
     public void showAbout() {
-
         JOptionPane.showMessageDialog(mainWindow,
             new Object[] { IconFactory.keyVersionLogo(),
                 KeYConstants.COPYRIGHT.replace("and", "\n" + UnicodeHelper.emSpaces(8) + "and")
                     + "\n\nWWW: http://key-project.org/" + "\n\nVersion " + KeYConstants.VERSION },
             "The KeY Project", JOptionPane.INFORMATION_MESSAGE);
-
-        // JOptionPane pane = new JOptionPane(
-        // KeYConstants.COPYRIGHT.replace("and", "\n"+UnicodeHelper.emSpaces(8)+"and")
-        // + "\n\nWWW: http://key-project.org/"
-        // + "\n\nVersion " + KeYConstants.VERSION
-        // , JOptionPane.INFORMATION_MESSAGE,
-        // JOptionPane.DEFAULT_OPTION, IconFactory.keyVersionLogo(108, 68));
-        // JDialog dialog = pane.createDialog(mainWindow, "The KeY Project");
-        // dialog.setVisible(true);
     }
-
 }
diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenFileAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenFileAction.java
index e7ff2c091cd..06465bf2ad8 100644
--- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenFileAction.java
+++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenFileAction.java
@@ -30,6 +30,8 @@ public OpenFileAction(MainWindow mainWindow) {
     public void actionPerformed(ActionEvent e) {
         KeYFileChooser fc = new KeYFileChooser(lastSelectedPath);
         fc.setDialogTitle("Select file to load proof or problem");
+        fc.setSelectedFile(KeYFileChooser.getFileChooser("Select file to load proof or problem")
+                .getSelectedFile());
         KeYFileChooserLoadingOptions options = fc.addLoadingOptions();
         fc.addBookmarkPanel();
         fc.prepare();
diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenMostRecentFileAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenMostRecentFileAction.java
index c9750f1d060..3216866acae 100644
--- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenMostRecentFileAction.java
+++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenMostRecentFileAction.java
@@ -27,9 +27,13 @@ public OpenMostRecentFileAction(MainWindow mainWindow) {
         setName("Reload");
         setIcon(IconFactory.openMostRecent(MainWindow.TOOLBAR_ICON_SIZE));
         setTooltip("Reload last opened file.");
+        updateEnabledStatus();
+        mainWindow.getMediator().addKeYSelectionListener(this);
+    }
+
+    public void updateEnabledStatus() {
         setEnabled(mainWindow.getRecentFiles() != null
                 && mainWindow.getRecentFiles().getMostRecent() != null);
-        mainWindow.getMediator().addKeYSelectionListener(this);
     }
 
     public void actionPerformed(ActionEvent e) {
diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SettingsTreeModel.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SettingsTreeModel.java
index e9336b37363..31051db3517 100644
--- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SettingsTreeModel.java
+++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SettingsTreeModel.java
@@ -12,6 +12,7 @@
 import javax.swing.tree.DefaultTreeModel;
 
 import de.uka.ilkd.key.gui.smt.OptionContentNode;
+import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.settings.ChoiceSettings;
 import de.uka.ilkd.key.settings.ProofIndependentSettings;
 import de.uka.ilkd.key.settings.ProofSettings;
@@ -19,6 +20,9 @@
 
 import org.key_project.logic.Choice;
 
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
+
 /**
  *
  * A swing model for {@link ShowActiveSettingsAction}.
@@ -28,18 +32,21 @@
 
 public class SettingsTreeModel extends DefaultTreeModel {
 
+    private static final Logger LOGGER = LoggerFactory.getLogger(SettingsTreeModel.class);
+
     private static final long serialVersionUID = -3282304543262262159L;
 
     private final ProofSettings proofSettings;
 
     private final ProofIndependentSettings independentSettings;
+    private final Proof proof;
     private OptionContentNode tacletOptionsItem;
 
-    public SettingsTreeModel(ProofSettings proofSettings,
-            ProofIndependentSettings independentSettings) {
+    public SettingsTreeModel(Proof proof) {
         super(new DefaultMutableTreeNode("All Settings"));
-        this.proofSettings = proofSettings;
-        this.independentSettings = independentSettings;
+        this.proof = proof;
+        this.proofSettings = proof == null ? null : proof.getSettings();
+        this.independentSettings = ProofIndependentSettings.DEFAULT_INSTANCE;
         generateTree();
     }
 
@@ -56,7 +63,6 @@ private void generateTree() {
                     "These are the proof dependent settings.");
             root.add(proofSettingsNode);
 
-            // ChoiceSettings choiceSettings = proofSettings.getChoiceSettings();
             ChoiceSettings choiceSettings = proofSettings.getChoiceSettings();
             tacletOptionsItem = generateTableNode("Taclet Options", choiceSettings);
             proofSettingsNode.add(tacletOptionsItem);
@@ -99,8 +105,23 @@ public JComponent getStartComponent() {
     private Properties getChoicesAsProperties(ChoiceSettings settings) {
         Properties prop = new Properties();
 
-        for (Choice choice : settings.getDefaultChoicesAsSet()) {
+        // Issue https://github.com/KeYProject/key/issues/3934 revealed a bug that the
+        // choices in proof settings were inconsistent with the actual settings the proof uses
+        // (determined by initConfig). We use the authorative source here and log inconsistencies
+        // for
+        // bug finding
+
+        // settings.getDefaultChoicesAsSet()
+        for (Choice choice : proof.getInitConfig().getActivatedChoices()) {
             prop.put(choice.category(), choice.name());
+
+            final String choiceName = settings.getDefaultChoices().get(choice.category());
+            if (choiceName != null && !choiceName.equals(choice.name().toString())) {
+                LOGGER.warn("Inconsistent proof settings for taclet option " + choice.category());
+            } else if (choiceName == null) {
+                LOGGER.warn("Taclet option active in proof but unknown by its choice settings "
+                    + choice.category());
+            }
         }
 
         return prop;
diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowActiveSettingsAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowActiveSettingsAction.java
index 40d266773b2..dd6f1c9a7b0 100644
--- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowActiveSettingsAction.java
+++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowActiveSettingsAction.java
@@ -14,8 +14,6 @@
 import de.uka.ilkd.key.gui.MainWindow;
 import de.uka.ilkd.key.gui.fonticons.IconFactory;
 import de.uka.ilkd.key.gui.smt.OptionContentNode;
-import de.uka.ilkd.key.settings.ProofIndependentSettings;
-import de.uka.ilkd.key.settings.ProofSettings;
 
 /**
  * for debugging - opens a window with the settings from current Proof and the default settings
@@ -36,11 +34,7 @@ public void actionPerformed(ActionEvent e) {
     }
 
     private ViewSettingsDialog showDialog() {
-        ProofSettings settings =
-            (getMediator().getSelectedProof() == null) ? null
-                    : getMediator().getSelectedProof().getSettings();
-        SettingsTreeModel model =
-            new SettingsTreeModel(settings, ProofIndependentSettings.DEFAULT_INSTANCE);
+        SettingsTreeModel model = new SettingsTreeModel(getMediator().getSelectedProof());
         ViewSettingsDialog dialog = new ViewSettingsDialog(model, model.getStartComponent());
         dialog.setTitle("All active settings");
         dialog.setLocationRelativeTo(mainWindow);
diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/fonticons/IconFactory.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/fonticons/IconFactory.java
index bd5006b3a56..d3503a96fcc 100644
--- a/key.ui/src/main/java/de/uka/ilkd/key/gui/fonticons/IconFactory.java
+++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/fonticons/IconFactory.java
@@ -169,7 +169,7 @@ public final class IconFactory {
     private static final Image keyLogo = getImage("images/key-color.png");
     private static final Image keyLogoShadow = getImage("images/key-shadow.png");
     // The following should be updated with every major version step.
-    private static final Image keyVersionLogo = getImage("images/key-shadow-2.12.png");
+    private static final Image keyVersionLogo = getImage("images/key-shadow-3.0.png");
     private static final Image keyLogoSmall = getImage("images/key-color-icon-square.gif");
     private static final Image oneStepSimplifier = getImage("images/toolbar/oneStepSimplifier.png");
 
diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/KeyStrokeSettings.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/KeyStrokeSettings.java
index b1f617a2a7b..0cdfefc4741 100644
--- a/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/KeyStrokeSettings.java
+++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/KeyStrokeSettings.java
@@ -196,7 +196,6 @@ KeyStroke getKeyStroke(String key, KeyStroke defaultValue) {
     }
 
     public void save() {
-        LOGGER.info("Save keyboard shortcuts to: {}", SETTINGS_FILE.toAbsolutePath());
         try {
             Files.createDirectories(SETTINGS_FILE.getParent());
             LOGGER.info("Save keyboard shortcuts to: {}", SETTINGS_FILE.toAbsolutePath());
diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/tacletmatch/TacletMatchDialog.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/tacletmatch/TacletMatchDialog.java
index 459e373774e..4fae38b9035 100644
--- a/key.ui/src/main/java/de/uka/ilkd/key/gui/tacletmatch/TacletMatchDialog.java
+++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/tacletmatch/TacletMatchDialog.java
@@ -162,7 +162,7 @@ private JComponent createInstantiationPanel() {
 
         alternatives = new JTabbedPane();
         for (int i = 0; i < model.length; i++) {
-            alternatives.addTab("Match " + (i + 1) + " of " + model.length, buildAlternative(i));
+            alternatives.addTab("Match " + (i + 1), buildAlternative(i));
         }
         alternatives.addChangeListener(e -> refreshStatus(current()));
         return alternatives;
@@ -181,8 +181,8 @@ private JComponent createFooter() {
         ButtonListener listener = new ButtonListener();
         cancelButton.addActionListener(listener);
         applyButton.addActionListener(listener);
-        buttons.add(cancelButton);
         buttons.add(applyButton);
+        buttons.add(cancelButton);
         footer.add(buttons, BorderLayout.EAST);
 
         setStatus(model[current()].getStatusString());
diff --git a/key.ui/src/main/resources/de/uka/ilkd/key/gui/THIRD_PARTY_LICENSES.txt b/key.ui/src/main/resources/de/uka/ilkd/key/gui/THIRD_PARTY_LICENSES.txt
index 777b1ff1bb0..d2c52785cc5 100644
--- a/key.ui/src/main/resources/de/uka/ilkd/key/gui/THIRD_PARTY_LICENSES.txt
+++ b/key.ui/src/main/resources/de/uka/ilkd/key/gui/THIRD_PARTY_LICENSES.txt
@@ -1,71 +1,232 @@
-===============================================================================
-Font Awesome 5.9
-Icons — CC BY 4.0 License
-https://fontawesome.com/license/free
-
-===============================================================================
-Docking Frames 1.1.3p1
-Project URL: http://www.docking-frames.org/
-License: LGPL 2.1 - https://www.gnu.org/licenses/old-licenses/lgpl-2.1.en.html
-
-===============================================================================
-Group: antlr  Name: antlr  Version: 2.7.7
-POM Project URL: http://www.antlr.org/
-POM License: BSD License - http://www.antlr.org/license.html
-
-===============================================================================
-Group: com.atlassian.commonmark  Name: commonmark  Version: 0.15.2
-POM License: Apache License, Version 2.0 - https://www.apache.org/licenses/LICENSE-2.0.txt
-POM License: Atlassian Customer Agreement - https://www.atlassian.com/legal/customer-agreement
-POM License: BSD 2-Clause License - http://opensource.org/licenses/BSD-2-Clause
-
-===============================================================================
-4. Group: com.atlassian.commonmark  Name: commonmark-ext-gfm-tables  Version: 0.15.2
-POM License: Apache License, Version 2.0 - https://www.apache.org/licenses/LICENSE-2.0.txt
-POM License: Atlassian Customer Agreement - https://www.atlassian.com/legal/customer-agreement
-POM License: BSD 2-Clause License - http://opensource.org/licenses/BSD-2-Clause
-
-===============================================================================
-Group: com.miglayout  Name: miglayout-core  Version: 5.2
+Dependency and their licenses of KeY
+This report was generated at Fri Jul 17 16:07:09 CEST 2026 .
+
+---
+
+1. Group: ch.qos.logback Name: logback-classic Version: 1.5.37
+
+Manifest Project URL: http://www.qos.ch
+POM License: EPL-2.0 - https://www.eclipse.org/legal/epl-v20.html
+POM License: LGPL-2.1-only - https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
+
+2. Group: ch.qos.logback Name: logback-core Version: 1.5.37
+
+Manifest Project URL: http://www.qos.ch
+POM License: EPL-2.0 - https://www.eclipse.org/legal/epl-v20.html
+POM License: LGPL-2.1-only - https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
+
+3. Group: com.formdev Name: flatlaf Version: 3.7.1
+
+POM Project URL: https://github.com/JFormDesigner/FlatLaf
+POM License: The Apache License, Version 2.0 - https://www.apache.org/licenses/LICENSE-2.0.txt
+Embedded license files: flatlaf-3.7.1.jar/META-INF/LICENSE
+
+4. Group: com.google.errorprone Name: error_prone_annotations Version: 2.41.0
+
+Manifest Project URL: https://errorprone.info/error_prone_annotations
+Manifest License: Apache 2.0
+POM License: Apache 2.0 - http://www.apache.org/licenses/LICENSE-2.0.txt
+
+5. Group: com.google.guava Name: failureaccess Version: 1.0.3
+
+Manifest Project URL: https://github.com/google/guava/
+POM License: Apache License, Version 2.0 - http://www.apache.org/licenses/LICENSE-2.0.txt
+Embedded license files: failureaccess-1.0.3.jar/META-INF/LICENSE
+
+6. Group: com.google.guava Name: guava Version: 33.5.0-jre
+
+Manifest Project URL: https://github.com/google/guava/
+POM Project URL: https://github.com/google/guava
+POM License: Apache License, Version 2.0 - http://www.apache.org/licenses/LICENSE-2.0.txt
+
+Embedded license files: guava-33.5.0-jre.jar/META-INF/LICENSE
+
+7. Group: com.google.guava Name: listenablefuture Version: 9999.0-empty-to-avoid-conflict-with-guava
+
+POM License: The Apache Software License, Version 2.0 - http://www.apache.org/licenses/LICENSE-2.0.txt
+
+8. Group: com.google.j2objc Name: j2objc-annotations Version: 3.1
+
+POM Project URL: https://github.com/google/j2objc/
+POM License: Apache License, Version 2.0 - http://www.apache.org/licenses/LICENSE-2.0.txt
+
+9. Group: com.ibm.icu Name: icu4j Version: 75.1
+
+POM License: Unicode-3.0 - https://raw.githubusercontent.com/unicode-org/icu/main/LICENSE
+Embedded license files: icu4j-75.1.jar/LICENSE
+
+10. Group: com.miglayout Name: miglayout-core Version: 11.4.3
+
+POM Project URL: http://www.miglayout.com/
 POM License: BSD - http://www.debian.org/misc/bsd.license
 
-===============================================================================
-Group: com.miglayout  Name: miglayout-swing  Version: 5.2
+11. Group: com.miglayout Name: miglayout-swing Version: 11.4.3
+
+POM Project URL: http://www.miglayout.com/
 POM License: BSD - http://www.debian.org/misc/bsd.license
 
-===============================================================================
-Group: javax.activation  Name: javax.activation-api  Version: 1.2.0
-Manifest Project URL: http://www.oracle.com
-POM License: CDDL/GPLv2+CE - https://github.com/javaee/activation/blob/master/LICENSE.txt
-
-===============================================================================
-Group: javax.xml.bind  Name: jaxb-api  Version: 2.4.0-b180830.0359
-Manifest Project URL: http://www.oracle.com/
-POM License: CDDL 1.1 - https://oss.oracle.com/licenses/CDDL+GPL-1.1
-POM License: GPL2 w/ CPE - https://oss.oracle.com/licenses/CDDL+GPL-1.1
-
-===============================================================================
-Group: net.java.dev.javacc  Name: javacc  Version: 4.0
-POM Project URL: http://javacc.dev.java.net/
-POM License: The BSD License - http://www.opensource.org/licenses/bsd-license.html
-
-===============================================================================
-Group: org.antlr  Name: ST4  Version: 4.0.8
-POM Project URL: http://www.stringtemplate.org
-POM License: BSD licence - http://antlr.org/license.html
+12. Group: com.squareup Name: javapoet Version: 1.13.0
 
-===============================================================================
-Group: org.antlr  Name: antlr  Version: 3.5.2
-POM License: BSD licence - http://antlr.org/license.html
+POM Project URL: http://github.com/square/javapoet/
+POM License: Apache 2.0 - http://www.apache.org/licenses/LICENSE-2.0.txt
+
+13. Group: commons-io Name: commons-io Version: 2.16.1
+
+Project URL: https://commons.apache.org/proper/commons-io/
+POM License: Apache-2.0 - https://www.apache.org/licenses/LICENSE-2.0.txt
+
+Embedded license files: commons-io-2.16.1.jar/META-INF/LICENSE.txt
+commons-io-2.16.1.jar/META-INF/NOTICE.txt
+
+14. Group: de.unruh Name: java-patterns Version: 0.1.0
+
+POM Project URL: https://github.com/dominique-unruh/java-patterns
+POM License: MIT - https://raw.githubusercontent.com/dominique-unruh/java-patterns/655c7cc5c71eb9ea0fcfee0ae797269e61845d8a/LICENSE
+
+15. Group: de.unruh Name: scala-isabelle_2.13 Version: 0.4.5
+
+POM Project URL: https://dominique-unruh.github.io/scala-isabelle
+POM License: Isabelle - https://raw.githubusercontent.com/dominique-unruh/scala-isabelle/5f28d8e6248f39dd7a31649d92c9850498e3985c/COPYRIGHT.Isabelle
+POM License: MIT - https://raw.githubusercontent.com/dominique-unruh/scala-isabelle/5f28d8e6248f39dd7a31649d92c9850498e3985c/LICENSE
+
+16. Group: info.picocli Name: picocli Version: 4.7.7
+
+POM Project URL: https://picocli.info
+POM License: The Apache Software License, version 2.0 - http://www.apache.org/licenses/LICENSE-2.0.txt
+
+17. Group: jakarta.json Name: jakarta.json-api Version: 2.1.3
+
+Manifest Project URL: https://www.eclipse.org
+POM Project URL: https://github.com/eclipse-ee4j/jsonp
+POM License: Eclipse Public License 2.0 - https://projects.eclipse.org/license/epl-2.0
+POM License: GNU General Public License, version 2 with the GNU Classpath Exception - https://projects.eclipse.org/license/secondary-gpl-2.0-cp
+
+Embedded license files: jakarta.json-api-2.1.3.jar/META-INF/LICENSE.md
+
+18. Group: org.antlr Name: ST4 Version: 4.3.4
+
+POM License: The BSD License - http://www.antlr.org/license.html
+
+19. Group: org.antlr Name: antlr-runtime Version: 3.5.3
 
-===============================================================================
-Group: org.antlr  Name: antlr-runtime  Version: 3.5.2
 POM Project URL: http://www.antlr.org
 POM License: BSD licence - http://antlr.org/license.html
 
-===============================================================================
-Group: org.jetbrains  Name: annotations  Version: 20.1.0
+20. Group: org.antlr Name: antlr4-runtime Version: 4.13.2
+
+Manifest Project URL: https://www.antlr.org/
+POM License: BSD-3-Clause - https://www.antlr.org/license.html
+
+21. Group: org.apache.commons Name: commons-lang3 Version: 3.14.0
+
+Project URL: https://commons.apache.org/proper/commons-lang/
+POM License: Apache-2.0 - https://www.apache.org/licenses/LICENSE-2.0.txt
+
+Embedded license files: commons-lang3-3.14.0.jar/META-INF/LICENSE.txt
+
+22. Group: org.apache.commons Name: commons-text Version: 1.12.0
+
+Project URL: https://commons.apache.org/proper/commons-text
+POM License: Apache-2.0 - https://www.apache.org/licenses/LICENSE-2.0.txt
+
+23. Group: org.checkerframework Name: checker-qual Version: 3.53.0
+
+Manifest License: MIT
+POM Project URL: https://checkerframework.org/
+POM License: The MIT License - http://opensource.org/licenses/MIT
+
+24. Group: org.javassist Name: javassist Version: 3.30.2-GA
+
+POM Project URL: https://www.javassist.org/
+POM License: Apache License 2.0 - https://www.apache.org/licenses/LICENSE-2.0
+POM License: LGPL 2.1 - https://www.gnu.org/licenses/lgpl-2.1.html
+POM License: MPL 1.1 - https://www.mozilla.org/en-US/MPL/1.1/
+
+25. Group: org.jetbrains Name: annotations Version: 24.1.0
+
 POM Project URL: https://github.com/JetBrains/java-annotations
 POM License: The Apache Software License, Version 2.0 - https://www.apache.org/licenses/LICENSE-2.0.txt
 
+26. Group: org.jspecify Name: jspecify Version: 1.0.0
+
+Manifest Project URL: https://jspecify.dev/docs/start-here
+POM Project URL: http://jspecify.org/
+POM License: The Apache License, Version 2.0 - http://www.apache.org/licenses/LICENSE-2.0.txt
+
+27. Group: org.junit Name: junit-bom Version: 5.14.2
+
+POM Project URL: https://junit.org/
+POM License: Eclipse Public License v2.0 - https://www.eclipse.org/legal/epl-v20.html
+
+28. Group: org.junit.jupiter Name: junit-jupiter-api Version: 5.14.2
+
+POM Project URL: https://junit.org/
+POM License: Eclipse Public License v2.0 - https://www.eclipse.org/legal/epl-v20.html
+
+
+29. Group: org.junit.jupiter Name: junit-jupiter-engine Version: 5.14.2
+
+POM Project URL: https://junit.org/
+POM License: Eclipse Public License v2.0 - https://www.eclipse.org/legal/epl-v20.html
+
+30. Group: org.junit.platform Name: junit-platform-commons Version: 1.14.2
+
+POM Project URL: https://junit.org/
+POM License: Eclipse Public License v2.0 - https://www.eclipse.org/legal/epl-v20.html
+
+
+31. Group: org.junit.platform Name: junit-platform-engine Version: 1.14.2
+
+POM Project URL: https://junit.org/
+POM License: Eclipse Public License v2.0 - https://www.eclipse.org/legal/epl-v20.html
+
+
+32. Group: org.key-project.proofjava Name: javaparser-core Version: 3.28.0-K13.5
+
+Manifest Project URL: https://javaparser.org
+Manifest License: Apache License, Version 2.0
+Manifest License: GNU Lesser General Public License
+
+POM Project URL: https://github.com/javaparser
+POM License: Apache License, Version 2.0 - http://www.apache.org/licenses/LICENSE-2.0.txt
+POM License: GNU Lesser General Public License - http://www.gnu.org/licenses/lgpl-3.0.html
+
+33. Group: org.key-project.proofjava Name: javaparser-core-serialization Version: 3.28.0-K13.5
+
+POM Project URL: https://github.com/javaparser
+POM License: Apache License, Version 2.0 - http://www.apache.org/licenses/LICENSE-2.0.txt
+POM License: GNU Lesser General Public License - http://www.gnu.org/licenses/lgpl-3.0.html
+
+34. Group: org.key-project.proofjava Name: javaparser-symbol-solver-core Version: 3.28.0-K13.5
+
+POM Project URL: https://github.com/javaparser
+POM License: Apache License, Version 2.0 - http://www.apache.org/licenses/LICENSE-2.0.txt
+POM License: GNU Lesser General Public License - http://www.gnu.org/licenses/lgpl-3.0.html
+
+35. Group: org.log4s Name: log4s_2.13 Version: 1.10.0
+
+POM Project URL: http://log4s.org/
+POM License: Apache License, Version 2.0 - http://www.apache.org/licenses/LICENSE-2.0.txt
+
+36. Group: org.opentest4j Name: opentest4j Version: 1.3.0
+
+Manifest License: The Apache License, Version 2.0
+POM Project URL: https://github.com/ota4j-team/opentest4j
+POM License: The Apache License, Version 2.0 - https://www.apache.org/licenses/LICENSE-2.0.txt
+
+Embedded license files: opentest4j-1.3.0.jar/META-INF/LICENSE
+
+37. Group: org.scala-lang Name: scala-library Version: 2.13.14
+
+POM Project URL: https://www.scala-lang.org/
+POM License: Apache-2.0 - https://www.apache.org/licenses/LICENSE-2.0
+
+38. Group: org.scalaz Name: scalaz-core_2.13 Version: 7.3.8
+
+POM Project URL: http://scalaz.org
+POM License: BSD-style - https://opensource.org/licenses/BSD-3-Clause
+
+39. Group: org.slf4j Name: slf4j-api Version: 2.0.18
 
+Project URL: http://www.slf4j.org
+POM License: MIT - https://opensource.org/license/mit
diff --git a/key.ui/src/main/resources/de/uka/ilkd/key/gui/images/key-shadow-3.0.png b/key.ui/src/main/resources/de/uka/ilkd/key/gui/images/key-shadow-3.0.png
new file mode 100644
index 00000000000..d900bee497e
Binary files /dev/null and b/key.ui/src/main/resources/de/uka/ilkd/key/gui/images/key-shadow-3.0.png differ
diff --git a/key.util/src/main/java/org/key_project/util/java/IOUtil.java b/key.util/src/main/java/org/key_project/util/java/IOUtil.java
index ea7caf8d9b3..1d866ac0fd1 100644
--- a/key.util/src/main/java/org/key_project/util/java/IOUtil.java
+++ b/key.util/src/main/java/org/key_project/util/java/IOUtil.java
@@ -908,11 +908,11 @@ public static String safePath(Path path) {
     public static String safePathRelativeTo(Path source, Path basePath) {
         if (Objects.equals(source.getRoot(), basePath.getRoot())) {
             // required on Windows
-            var abs = source.toAbsolutePath();
+            var abs = source.toAbsolutePath().normalize();
             return safePath(basePath.relativize(abs));
         } else {
             // fallback: return absolute path
-            return safePath(source.toAbsolutePath());
+            return safePath(source.toAbsolutePath().normalize());
         }
     }
 }
diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/IsabelleTranslationSettings.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/IsabelleTranslationSettings.java
index 0e3674527d5..d63f7ffadc7 100644
--- a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/IsabelleTranslationSettings.java
+++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/IsabelleTranslationSettings.java
@@ -156,7 +156,7 @@ public void save() {
     public void readSettings(Properties props) {
         isabellePath = Path.of(props.getProperty(isabellePathKey));
         Path newTranslationPath = Path.of(props.getProperty(translationPathKey));
-        if (newTranslationPath != translationPath) {
+        if (!newTranslationPath.equals(translationPath)) {
             translationPath = newTranslationPath;
             createSessionFiles();
         }
@@ -180,7 +180,7 @@ public void readSettings(@NonNull Configuration props) {
 
         Path newTranslationPath =
             Path.of(props.getString(translationPathKey, translationPath.toString()));
-        if (newTranslationPath != translationPath) {
+        if (!newTranslationPath.equals(translationPath)) {
             translationPath = newTranslationPath;
             createSessionFiles();
         }