diff --git a/build.gradle b/build.gradle
index ca72be8edcc..52b702d33e7 100644
--- a/build.gradle
+++ b/build.gradle
@@ -32,16 +32,6 @@ idea {
     }
 }
 
-// Helper function that calls "git rev-parse" to
-// find names/SHAs for commits
-static def gitRevParse(String args) {
-    try {
-        return "git rev-parse $args".execute().text.trim()
-    } catch (Exception e) {
-        return ""
-    }
-}
-
 static def getDate() {
     return new Date().format('yyyyMMdd')
 }
diff --git a/key.core/build.gradle b/key.core/build.gradle
index 62895ba3c50..3b2162777de 100644
--- a/key.core/build.gradle
+++ b/key.core/build.gradle
@@ -172,6 +172,7 @@ task generateVersionFiles() {
     def branch = new File(outputFolder, "branch")
     def versionf = new File(outputFolder, "version")
 
+    inputs.files "$project.rootDir/.git/HEAD"
     outputs.files sha1, branch, versionf
 
     def gitRevision = gitRevParse('HEAD')
@@ -184,6 +185,16 @@ task generateVersionFiles() {
     }
 }
 
+// Helper function that calls "git rev-parse" to
+// find names/SHAs for commits
+static def gitRevParse(String args) {
+    try {
+        return "git rev-parse $args".execute().text.trim()
+    } catch (Exception e) {
+        return ""
+    }
+}
+
 // @AW: Say something here. From POV this explain by itself.
 processResources.dependsOn generateVersionFiles
 
diff --git a/key.core/src/main/java/de/uka/ilkd/key/control/KeYEnvironment.java b/key.core/src/main/java/de/uka/ilkd/key/control/KeYEnvironment.java
index 37b3d972fcc..33a03426646 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/control/KeYEnvironment.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/control/KeYEnvironment.java
@@ -318,5 +318,4 @@ public boolean isDisposed() {
     public Pair<String, Location> getProofScript() {
         return proofScript;
     }
-
 }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/Services.java b/key.core/src/main/java/de/uka/ilkd/key/java/Services.java
index 78a42e81497..68bc26462bc 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/Services.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/Services.java
@@ -14,6 +14,7 @@
 import de.uka.ilkd.key.proof.init.InitConfig;
 import de.uka.ilkd.key.proof.init.Profile;
 import de.uka.ilkd.key.proof.mgt.SpecificationRepository;
+import de.uka.ilkd.key.settings.ProofIndependentSettings;
 import de.uka.ilkd.key.util.Debug;
 import de.uka.ilkd.key.util.KeYRecoderExcHandler;
 
@@ -298,6 +299,10 @@ public void setProof(Proof p_proof) {
                 "Services are already owned by another proof:" + proof.name());
         }
         proof = p_proof;
+        if (!ProofIndependentSettings.DEFAULT_INSTANCE.getTermLabelSettings().getUseOriginLabels()
+                || !proof.getSettings().getTermLabelSettings().getUseOriginLabels()) {
+            profile.getTermLabelManager().disableOriginLabelRefactorings();
+        }
     }
 
 
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabelManager.java b/key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabelManager.java
index 07a64fd030b..f1c89eb4c7f 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabelManager.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabelManager.java
@@ -5,6 +5,8 @@
 
 import java.util.*;
 import java.util.Map.Entry;
+import java.util.Set;
+import java.util.stream.Collectors;
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.logic.*;
@@ -16,6 +18,11 @@
 import de.uka.ilkd.key.rule.Rule;
 import de.uka.ilkd.key.rule.RuleApp;
 import de.uka.ilkd.key.rule.label.*;
+import de.uka.ilkd.key.rule.label.ChildTermLabelPolicy;
+import de.uka.ilkd.key.rule.label.OriginTermLabelRefactoring;
+import de.uka.ilkd.key.rule.label.TermLabelMerger;
+import de.uka.ilkd.key.rule.label.TermLabelPolicy;
+import de.uka.ilkd.key.rule.label.TermLabelRefactoring;
 import de.uka.ilkd.key.rule.label.TermLabelRefactoring.RefactoringScope;
 import de.uka.ilkd.key.util.LinkedHashMap;
 import de.uka.ilkd.key.util.Pair;
@@ -2194,4 +2201,14 @@ protected void mergeLabels(SequentChangeInfo currentSequent, Services services,
             }
         }
     }
+
+    /**
+     * Fully disable origin tracking. This will remove the {@link OriginTermLabelRefactoring} from
+     * the manager.
+     */
+    public void disableOriginLabelRefactorings() {
+        allRulesRefactorings = ImmutableList.fromList(
+            allRulesRefactorings.stream().filter(x -> !(x instanceof OriginTermLabelRefactoring))
+                    .collect(Collectors.toList()));
+    }
 }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/ProofMacroFinishedInfo.java b/key.core/src/main/java/de/uka/ilkd/key/macros/ProofMacroFinishedInfo.java
index 921e5f47d39..ab7ab283541 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/macros/ProofMacroFinishedInfo.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/macros/ProofMacroFinishedInfo.java
@@ -4,9 +4,11 @@
 package de.uka.ilkd.key.macros;
 
 import java.util.HashMap;
+import java.util.List;
 import java.util.Map;
 
 import de.uka.ilkd.key.proof.Goal;
+import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.proof.Statistics;
 import de.uka.ilkd.key.prover.impl.ApplyStrategyInfo;
@@ -70,6 +72,12 @@ public ProofMacroFinishedInfo(ProofMacro macro, ImmutableList<Goal> goals) {
         this(macro, goals, goals.isEmpty() ? null : goals.head().proof(), false);
     }
 
+    public ProofMacroFinishedInfo(ProofMacro macro, ImmutableList<Goal> goals,
+            List<Node> statisticNodes) {
+        this(macro, goals, goals.isEmpty() ? null : goals.head().proof(),
+            statisticNodes.isEmpty() ? null : new Statistics(statisticNodes));
+    }
+
     public ProofMacroFinishedInfo(ProofMacro macro, Proof proof) {
         this(macro, proof.openEnabledGoals(), proof, false);
     }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/StrategyProofMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/StrategyProofMacro.java
index fe275f66318..9c4b7906378 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/macros/StrategyProofMacro.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/macros/StrategyProofMacro.java
@@ -3,9 +3,13 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.macros;
 
+import java.util.List;
+import java.util.stream.Collectors;
+
 import de.uka.ilkd.key.control.UserInterfaceControl;
 import de.uka.ilkd.key.logic.PosInOccurrence;
 import de.uka.ilkd.key.proof.Goal;
+import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.prover.GoalChooser;
 import de.uka.ilkd.key.prover.ProverCore;
@@ -72,6 +76,7 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof,
             // false
             return null;
         }
+        List<Node> nodes = goals.stream().map(Goal::node).collect(Collectors.toList());
 
         final GoalChooser goalChooser =
             proof.getInitConfig().getProfile().getSelectedGoalChooserBuilder().create();
@@ -84,9 +89,9 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof,
             new ProgressBarListener(goals.size(), getMaxSteps(proof), listener);
         applyStrategy.addProverTaskObserver(pml);
         // add a focus manager if there is a focus
-        if (posInOcc != null && goals != null) {
-            AutomatedRuleApplicationManager realManager = null;
-            FocussedRuleApplicationManager manager = null;
+        if (posInOcc != null) {
+            AutomatedRuleApplicationManager realManager;
+            FocussedRuleApplicationManager manager;
             for (Goal goal : goals) {
                 realManager = goal.getRuleAppManager();
                 realManager.clearCache();
@@ -99,7 +104,7 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof,
         Strategy oldStrategy = proof.getActiveStrategy();
         proof.setActiveStrategy(createStrategy(proof, posInOcc));
 
-        ProofMacroFinishedInfo info = new ProofMacroFinishedInfo(this, goals, proof, false);
+        ProofMacroFinishedInfo info;
         try {
             // find the relevant goals
             // and start
@@ -125,7 +130,8 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof,
             }
             final ImmutableList<Goal> resultingGoals =
                 setDifference(proof.openGoals(), ignoredOpenGoals);
-            info = new ProofMacroFinishedInfo(this, resultingGoals);
+            info = new ProofMacroFinishedInfo(this, resultingGoals,
+                nodes);
             proof.setActiveStrategy(oldStrategy);
             doPostProcessing(proof);
             applyStrategy.removeProverTaskObserver(pml);
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/Statistics.java b/key.core/src/main/java/de/uka/ilkd/key/proof/Statistics.java
index 33a4cfd705c..c9bbdb1d129 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/Statistics.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/Statistics.java
@@ -73,6 +73,78 @@ protected Statistics(int nodes, int branches, int cachedBranches, int interactiv
         this.timePerStepInMillis = timePerStepInMillis;
     }
 
+    public Statistics(List<Node> startNodes) {
+        if (startNodes.isEmpty()) {
+            throw new IllegalArgumentException("can't generate statistics on zero nodes");
+        }
+
+        int nodes = 0;
+        int branches = 0;
+        int cachedBranches = 0;
+        int interactiveSteps = 0;
+        int symbExApps = 0;
+        int quantifierInstantiations = 0;
+        int ossApps = 0;
+        int mergeRuleApps = 0;
+        int totalRuleApps = 0;
+        int smtSolverApps = 0;
+        int dependencyContractApps = 0;
+        int operationContractApps = 0;
+        int blockLoopContractApps = 0;
+        int loopInvApps = 0;
+        long autoModeTimeInMillis = 0;
+        long timeInMillis = 0;
+
+        for (Node startNode : startNodes) {
+            final Iterator<Node> it = startNode.subtreeIterator();
+
+            TemporaryStatistics tmp = new TemporaryStatistics();
+
+            Node node;
+            while (it.hasNext()) {
+                node = it.next();
+                tmp.changeOnNode(node, interactiveAppsDetails);
+            }
+
+            nodes += tmp.nodes;
+            branches = tmp.branches;
+            cachedBranches = tmp.cachedBranches;
+            interactiveSteps = tmp.interactive;
+            symbExApps = tmp.symbExApps;
+            quantifierInstantiations = tmp.quant;
+            ossApps = tmp.oss;
+            mergeRuleApps = tmp.mergeApps;
+            totalRuleApps = tmp.nodes + tmp.ossCaptured - 1;
+            smtSolverApps = tmp.smt;
+            dependencyContractApps = tmp.dep;
+            operationContractApps = tmp.contr;
+            blockLoopContractApps = tmp.block;
+            loopInvApps = tmp.inv;
+            autoModeTimeInMillis = startNode.proof().getAutoModeTime();
+            timeInMillis = (System.currentTimeMillis() - startNode.proof().creationTime);
+        }
+
+        this.nodes = nodes;
+        this.branches = branches;
+        this.cachedBranches = cachedBranches;
+        this.interactiveSteps = interactiveSteps;
+        this.symbExApps = symbExApps;
+        this.quantifierInstantiations = quantifierInstantiations;
+        this.ossApps = ossApps;
+        this.mergeRuleApps = mergeRuleApps;
+        this.totalRuleApps = totalRuleApps;
+        this.smtSolverApps = smtSolverApps;
+        this.dependencyContractApps = dependencyContractApps;
+        this.operationContractApps = operationContractApps;
+        this.blockLoopContractApps = blockLoopContractApps;
+        this.loopInvApps = loopInvApps;
+        this.autoModeTimeInMillis = autoModeTimeInMillis;
+        this.timeInMillis = timeInMillis;
+        this.timePerStepInMillis = nodes <= 1 ? .0f : (autoModeTimeInMillis / (float) (nodes - 1));
+
+        generateSummary(startNodes.get(0).proof());
+    }
+
     Statistics(Node startNode) {
         final Iterator<Node> it = startNode.subtreeIterator();
 
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java b/key.core/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java
index 431376199b0..1b657eb58af 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java
@@ -92,7 +92,7 @@ public static ClosedBy findPreviousProof(DefaultListModel<Proof> previousProofs,
                 // for each node, check that the sequent in the reference is
                 // a subset of the new sequent
                 Node n = nodesToCheck.remove();
-                if (checkedNodes.contains(n)) {
+                if (checkedNodes.contains(n) || !n.isClosed()) {
                     continue;
                 }
                 checkedNodes.add(n);
diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/communication/ExternalProcessLauncher.java b/key.core/src/main/java/de/uka/ilkd/key/smt/communication/ExternalProcessLauncher.java
index 0c115b5fdfc..a8b76174271 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/smt/communication/ExternalProcessLauncher.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/smt/communication/ExternalProcessLauncher.java
@@ -76,7 +76,9 @@ public void launch(final String[] command) throws IOException {
      */
     public void stop() {
         if (process != null) {
-            process.destroy();
+            // make sure the solver process is properly killed,
+            // otherwise it may consume excessive CPU and RAM
+            process.destroyForcibly();
         }
         // TODO: where to close the pipe?
         // pipe.close();
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlChecks.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlChecks.java
index eeda79c6916..9db4d4adbfa 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlChecks.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlChecks.java
@@ -81,7 +81,7 @@ private void checkRequires(List<JmlParser.ClauseContext> clauses) {
 
             if (isRequiresClause(clause) && otherClause) {
                 addWarning(clause,
-                    "Diverging Semantics form JML Reference: Requires does not initiate a new contract. "
+                    "Diverging Semantics from JML Reference: Requires does not initiate a new contract. "
                         + "See https://keyproject.github.io/key-docs/user/JMLGrammar/#TODO");
             }
         }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/MiscTools.java b/key.core/src/main/java/de/uka/ilkd/key/util/MiscTools.java
index 5eeecfc3891..abcb1f832c0 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/util/MiscTools.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/util/MiscTools.java
@@ -816,9 +816,15 @@ public static URI getURIFromTokenSource(String source) {
         }
 
         try {
-            return new URI(source);
+            URI uri = new URI(source);
+            if (uri.getScheme() != null) {
+                // use this URI only if there is an explicit scheme;
+                // otherwise parse it as a filename
+                return uri;
+            }
         } catch (URISyntaxException ignored) {
         }
+
         return Path.of(source).toUri();
     }
 
diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/TestOneStepSimplifier.java b/key.core/src/test/java/de/uka/ilkd/key/proof/TestOneStepSimplifier.java
index e48d938d861..406ea3e38fd 100644
--- a/key.core/src/test/java/de/uka/ilkd/key/proof/TestOneStepSimplifier.java
+++ b/key.core/src/test/java/de/uka/ilkd/key/proof/TestOneStepSimplifier.java
@@ -27,5 +27,6 @@ void loadWithRestriction() throws ProblemLoaderException {
             KeYEnvironment.load(new File(testCaseDirectory, "ossRestriction.proof"));
         Assertions.assertNotNull(env.getLoadedProof());
         Assertions.assertTrue(env.getLoadedProof().closed());
+        env.dispose();
     }
 }
diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/replay/TestCopyingReplayer.java b/key.core/src/test/java/de/uka/ilkd/key/proof/replay/TestCopyingReplayer.java
index 0acab036533..ffa13d6709d 100644
--- a/key.core/src/test/java/de/uka/ilkd/key/proof/replay/TestCopyingReplayer.java
+++ b/key.core/src/test/java/de/uka/ilkd/key/proof/replay/TestCopyingReplayer.java
@@ -51,5 +51,8 @@ void testJavaProof() throws Exception {
         Assertions.assertEquals(proof1.countNodes(), proof2.countNodes());
 
         GeneralSettings.noPruningClosed = true;
+
+        env.dispose();
+        env2.dispose();
     }
 }
diff --git a/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/NJmlTranslatorTests.java b/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/NJmlTranslatorTests.java
index 9841e195fe5..b51e58f6cc8 100644
--- a/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/NJmlTranslatorTests.java
+++ b/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/NJmlTranslatorTests.java
@@ -6,6 +6,7 @@
 import java.io.File;
 import java.net.URI;
 import java.net.URISyntaxException;
+import java.nio.file.Path;
 
 import de.uka.ilkd.key.java.JavaInfo;
 import de.uka.ilkd.key.java.Position;
@@ -79,7 +80,7 @@ public void testIgnoreOpenJML() {
     // }
 
     @Test
-    public void testWarnRequires() throws URISyntaxException {
+    void testWarnRequires() throws URISyntaxException {
         preParser.clearWarnings();
         String contract = "/*@ requires true; ensures true; requires true;";
         ImmutableList<TextualJMLConstruct> result =
@@ -88,8 +89,9 @@ public void testWarnRequires() throws URISyntaxException {
         ImmutableList<PositionedString> warnings = preParser.getWarnings();
         PositionedString message = warnings.head();
         assertEquals(
-            "Diverging Semantics form JML Reference: Requires does not initiate a new contract. "
-                + "See https://keyproject.github.io/key-docs/user/JMLGrammar/#TODO (Test.java, 5/38)",
+            "Diverging Semantics from JML Reference: Requires does not initiate a new contract. "
+                + "See https://keyproject.github.io/key-docs/user/JMLGrammar/#TODO ("
+                + Path.of("Test.java").toUri() + ", 5/38)",
             message.toString());
     }
 
diff --git a/key.core/src/test/java/de/uka/ilkd/key/util/TestEqualsModProofIrrelevancy.java b/key.core/src/test/java/de/uka/ilkd/key/util/TestEqualsModProofIrrelevancy.java
index 6f468df05ed..f8347da086e 100644
--- a/key.core/src/test/java/de/uka/ilkd/key/util/TestEqualsModProofIrrelevancy.java
+++ b/key.core/src/test/java/de/uka/ilkd/key/util/TestEqualsModProofIrrelevancy.java
@@ -57,5 +57,7 @@ void testJavaProof() throws Exception {
                     node1.getAppliedRuleApp().equalsModProofIrrelevancy(node2.getAppliedRuleApp()));
             }
         }
+        env.dispose();
+        env2.dispose();
     }
 }
diff --git a/key.ui/src/main/java/de/uka/ilkd/key/core/KeYMediator.java b/key.ui/src/main/java/de/uka/ilkd/key/core/KeYMediator.java
index 72bc9e54fd0..5eeb1ee4448 100644
--- a/key.ui/src/main/java/de/uka/ilkd/key/core/KeYMediator.java
+++ b/key.ui/src/main/java/de/uka/ilkd/key/core/KeYMediator.java
@@ -16,6 +16,7 @@
 import de.uka.ilkd.key.control.ProofControl;
 import de.uka.ilkd.key.gui.GUIListener;
 import de.uka.ilkd.key.gui.InspectorForDecisionPredicates;
+import de.uka.ilkd.key.gui.MainWindow;
 import de.uka.ilkd.key.gui.UserActionListener;
 import de.uka.ilkd.key.gui.actions.useractions.UserAction;
 import de.uka.ilkd.key.gui.notification.events.ExceptionFailureEvent;
@@ -566,6 +567,7 @@ public void interrupt() {
      * @param b true iff interactive mode is to be turned on
      */
     public void setInteractive(boolean b) {
+        MainWindow.getInstance().getAutoModeAction().setEnabled(true);
         if (getSelectedProof() != null) {
             if (b) {
                 getSelectedProof().setRuleAppIndexToInteractiveMode();
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 ff500afa208..0c45b171895 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
@@ -775,6 +775,14 @@ public void setStandardStatusLine() {
         ThreadUtilities.invokeOnEventQueue(this::setStandardStatusLineImmediately);
     }
 
+    /**
+     * Hide the progress bar if it is currently visible.
+     */
+    public void hideStatusProgress() {
+        getStatusLine().setProgress(0);
+        statusLine.setProgressPanelVisible(false);
+    }
+
     private void setStatusLineImmediately(String str, int max) {
         // statusLine.reset();
         statusLine.setStatusText(str);
diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java
index b14de3dc315..9c889ed5e1e 100644
--- a/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java
+++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java
@@ -197,7 +197,7 @@ private void taskFinishedInternal(TaskFinishedInfo info) {
             mainWindow.displayResults(info.toString());
         } else if (info != null && info.getSource() instanceof ProofMacro) {
             if (!isAtLeastOneMacroRunning()) {
-                resetStatus(this);
+                mainWindow.hideStatusProgress();
                 assert info instanceof ProofMacroFinishedInfo;
                 Proof proof = info.getProof();
                 if (proof != null && !proof.closed()
diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/AutoModeAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/AutoModeAction.java
index 8abe866558e..3cc42ee6380 100644
--- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/AutoModeAction.java
+++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/AutoModeAction.java
@@ -168,6 +168,7 @@ public void actionPerformed(ActionEvent e) {
             // This method delegates the request only to the UserInterfaceControl which implements
             // the functionality.
             // No functionality is allowed in this method body!
+            setEnabled(false);
             getMediator().getUI().getProofControl().stopAutoMode();
         }
     }
diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeModel.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeModel.java
index 19e498bd817..617b1696f41 100644
--- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeModel.java
+++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeModel.java
@@ -147,9 +147,15 @@ public void proofGoalRemoved(ProofTreeEvent e) {
      * This can be used to pause tree updates when many goals get their state changed at once. The
      * tree is updated automatically after this is set to false.
      */
-    public void setBatchGoalStateChange(boolean value) {
+    public void setBatchGoalStateChange(boolean value, Collection<Node> nodesToUpdate) {
         if (!value && batchGoalStateChange) {
-            updateTree((TreeNode) null);
+            if (nodesToUpdate == null || nodesToUpdate.isEmpty()) {
+                updateTree((TreeNode) null);
+            } else {
+                for (Node n : nodesToUpdate) {
+                    updateTree(n);
+                }
+            }
         }
         batchGoalStateChange = value;
     }
diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreePopupFactory.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreePopupFactory.java
index f8573f7f833..579ab9df197 100644
--- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreePopupFactory.java
+++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreePopupFactory.java
@@ -4,7 +4,9 @@
 package de.uka.ilkd.key.gui.prooftree;
 
 import java.awt.event.ActionEvent;
+import java.util.ArrayList;
 import java.util.Iterator;
+import java.util.List;
 import java.util.function.Predicate;
 import javax.swing.*;
 import javax.swing.tree.TreeNode;
@@ -470,17 +472,23 @@ public Iterable<Goal> getGoalList() {
             return context.proof.getSubtreeGoals(context.invokedNode);
         }
 
-        /*
+        /**
          * In addition to marking setting goals, update the tree model so that the label sizes are
          * recalculated
          */
         @Override
         public void actionPerformed(ActionEvent e) {
-            context.delegateModel.setBatchGoalStateChange(true);
+            var selectedNode = context.proofTreeView.getSelectedNode();
+            context.delegateModel.setBatchGoalStateChange(true, null);
             super.actionPerformed(e);
-            context.delegateModel.setBatchGoalStateChange(false);
-            // trigger repainting the tree after the completion of this event.
-            context.delegateView.repaint();
+            List<Node> goals = new ArrayList<>();
+            getGoalList().forEach(x -> goals.add(x.node()));
+            context.delegateModel.setBatchGoalStateChange(false, goals);
+            // make sure the node is selected again
+            if (selectedNode != null) {
+                context.proofTreeView.makeNodeVisible(selectedNode);
+            }
+            // repainting the tree after the completion of this event is done automatically
         }
     }
 
diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java
index 47271582b18..df3f3a2de7d 100644
--- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java
+++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java
@@ -1313,4 +1313,15 @@ public Component getTreeCellRendererComponent(JTree tree, Object value, boolean
             return this;
         }
     }
+
+    public Node getSelectedNode() {
+        TreePath sp = delegateView.getSelectionPath();
+        if (sp == null) {
+            return null;
+        }
+        Object treeNode = sp.getLastPathComponent();
+        return (treeNode instanceof GUIAbstractTreeNode)
+                ? ((GUIAbstractTreeNode) treeNode).getNode()
+                : null;
+    }
 }
diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/analysis/DependencyAnalyzer.java b/keyext.slicing/src/main/java/org/key_project/slicing/analysis/DependencyAnalyzer.java
index 1a777728575..a0433f4874e 100644
--- a/keyext.slicing/src/main/java/org/key_project/slicing/analysis/DependencyAnalyzer.java
+++ b/keyext.slicing/src/main/java/org/key_project/slicing/analysis/DependencyAnalyzer.java
@@ -45,6 +45,7 @@
 import org.key_project.slicing.graph.ClosedGoal;
 import org.key_project.slicing.graph.DependencyGraph;
 import org.key_project.slicing.graph.GraphNode;
+import org.key_project.slicing.graph.PseudoOutput;
 import org.key_project.slicing.graph.TrackedFormula;
 import org.key_project.slicing.util.ExecutionTime;
 import org.key_project.util.EqualsModProofIrrelevancyWrapper;
@@ -385,7 +386,14 @@ private void analyzeDependenciesBranches() {
             Map<BranchLocation, Collection<GraphNode>> groupedOutputs = new HashMap<>();
             node.childrenIterator().forEachRemaining(
                 x -> groupedOutputs.put(x.getBranchLocation(), new ArrayList<>()));
-            data.outputs.forEach(n -> groupedOutputs.get(n.getBranchLocation()).add(n));
+            data.outputs.forEach(n -> {
+                if (n instanceof PseudoOutput) {
+                    // cut did not any new formulas
+                    // (always leads to cutWasUseful = false)
+                    return;
+                }
+                groupedOutputs.get(n.getBranchLocation()).add(n);
+            });
             boolean cutWasUseful = groupedOutputs.values().stream()
                     .allMatch(l -> l.stream().anyMatch(usefulFormulas::contains));
             if (cutWasUseful) {