diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java
index 960cd033f50..db3fb0d3fcc 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java
@@ -15,10 +15,7 @@
 import de.uka.ilkd.key.logic.PosInOccurrence;
 import de.uka.ilkd.key.logic.PosInTerm;
 import de.uka.ilkd.key.logic.Term;
-import de.uka.ilkd.key.logic.op.Equality;
-import de.uka.ilkd.key.logic.op.Junctor;
-import de.uka.ilkd.key.logic.op.Quantifier;
-import de.uka.ilkd.key.logic.op.SortDependingFunction;
+import de.uka.ilkd.key.logic.op.*;
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.proof.rulefilter.SetRuleFilter;
@@ -525,9 +522,14 @@ private RuleSetDispatchFeature setupCostComputationF() {
                 applyTF(instOf("uSub"), IsInductionVariable.INSTANCE), longConst(0), inftyConst()));
         }
 
+        setupTracingStrategy(d);
         return d;
     }
 
+    private void setupTracingStrategy(RuleSetDispatchFeature d) {
+        bindRuleSet(d, "retrace", longConst(-200));
+    }
+
     private void setupSelectSimplification(final RuleSetDispatchFeature d) {
         bindRuleSet(d, "pull_out_select",
             // pull out select only if it can be simplified
diff --git a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/JAVALANG.TXT b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/JAVALANG.TXT
index ece9cf04a53..ddd973f4f12 100644
--- a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/JAVALANG.TXT
+++ b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/JAVALANG.TXT
@@ -58,4 +58,4 @@ java.util.ListIteratorImpl
 java.util.Date
 java.util.LinkedHashMap
 java.util.LinkedList
-
+tracer.Trace
diff --git a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/tracer/Trace.java b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/tracer/Trace.java
new file mode 100644
index 00000000000..6d710db8d80
--- /dev/null
+++ b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/tracer/Trace.java
@@ -0,0 +1,7 @@
+package tracer;
+
+import java.lang.String;
+
+public class Trace {
+    //@ public static ghost int index;
+}
diff --git a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/tracer/Trace.key b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/tracer/Trace.key
new file mode 100644
index 00000000000..5903fb0ee93
--- /dev/null
+++ b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/tracer/Trace.key
@@ -0,0 +1,300 @@
+
+\predicates {
+    /* use this as input */
+    traceAfter(int, java.lang.String);
+    traceBefore(int, java.lang.String);
+
+    /* used this to display current trace string */
+    traced(int, int, Seq);
+
+    /* used on the sequent */
+    traceIf(int);
+}
+
+\functions {
+    /* helper function without meaning */
+    Seq seqConcatEnd(Seq, Seq);
+}
+
+\schemaVariables {
+    \modalOperator {diamond, box, diamond_transaction, box_transaction} #allmodal;
+    \program Expression #e, #e0, #e1, #e2;
+    \program SimpleExpression #se, #se0, #se1, #se2;
+    \program SimpleJavaBooleanExpression #seBool, #seBool0, #seBool1, #seBool2;
+    \program NonSimpleExpression #nse, #nse0, #nse1, #nse2;
+    \program Statement #s0, #s1, #s2;
+    \program LeftHandSide #lhs;
+    \program Variable #v0;
+    \formula post;
+    \term int idx, idx0;
+    \term java.lang.String str;
+    \term Seq #seq;
+}
+
+\rules(programRules:Java, tracing:on) {
+
+    /*
+     * Initialization (only interactively)
+     */
+    traceIndexInit {
+       \add( tracer.Trace.index = 0 ==> )
+    };
+    traceRetraceInit {
+       \add( traced(tracer.Trace.index, tracer.Trace.index, "") ==> )
+    };
+
+
+    /*
+     * Symbolic execution rules, using (!) traceIf(int)
+     */
+    traceIf {
+        \find(
+            ==> \modality{#allmodal}{..
+                if(#se) #s0
+            ...}\endmodality (post)
+        )
+        \replacewith(
+            ==>
+            \if(traceIf(tracer.Trace.index))
+            \then(
+                {tracer.Trace.index := tracer.Trace.index+1}\modality{#allmodal}{..
+                    #s0
+                ...}\endmodality (post)
+            )
+            \else(
+                {tracer.Trace.index := tracer.Trace.index+1}\modality{#allmodal}{..
+                ...}\endmodality (post)
+            )
+        )
+        \add(
+            (#se = TRUE) <-> traceIf(tracer.Trace.index)
+            ==>
+        )
+        \heuristics(retrace)
+    };
+
+    traceIfElse {
+        \find(
+            ==> \modality{#allmodal}{..
+                if(#se) #s0 else #s1
+            ...}\endmodality (post)
+        )
+        \replacewith(
+            ==>
+            \if(traceIf(tracer.Trace.index))
+            \then(
+                {tracer.Trace.index := tracer.Trace.index+1}\modality{#allmodal}{..
+                    #s0
+                ...}\endmodality (post)
+            )
+            \else(
+                {tracer.Trace.index := tracer.Trace.index+1}\modality{#allmodal}{..
+                    #s1
+                ...}\endmodality (post)
+            )
+        )
+        \add(
+            (#se = TRUE) <-> traceIf(tracer.Trace.index)
+            ==>
+        )
+        \heuristics(retrace)
+    };
+
+
+    /*
+     * Rules to convert string traces to sets of traceIf(int) in sequent
+     */
+    traceFollowElse {
+      \find(
+          traceAfter(idx, strPool(seqConcat(seqSingleton('0'), #seq)))
+      )
+      \replacewith(
+          !traceIf(idx) & traceAfter(idx + 1, strPool(#seq))
+      )
+      \heuristics(simplify)
+    };
+
+    traceFollowElseEnd {
+      \find(
+         traceAfter(idx, strPool(seqSingleton('0')))
+      )
+      \replacewith(
+         !traceIf(idx)
+      )
+      \heuristics(simplify)
+    };
+
+    traceFollowIf {
+      \find(
+          traceAfter(idx, strPool(seqConcat(seqSingleton('1'), #seq)))
+      )
+      \replacewith(
+          traceIf(idx) & traceAfter(idx + 1, strPool(#seq))
+      )
+      \heuristics(simplify)
+    };
+
+    traceFollowIfEnd {
+      \find(
+         traceAfter(idx, strPool(seqSingleton('1')))
+      )
+      \replacewith(
+         traceIf(idx)
+      )
+      \heuristics(simplify)
+    };
+
+    traceBeforeElim {
+        \find(
+            traceBefore(idx, strPool(#seq))
+        )
+        \replacewith(
+            traceAfter(idx - seqLen(#seq), strPool(#seq))
+        )
+        \heuristics(simplify)
+    };
+
+
+    /*
+     * Rules to reconvert traceIf(int) sets for displaying the current trace
+     */
+    printTracedIf {
+      \assumes(
+          traceIf(idx) ==>
+      )
+      \find(
+          traced(idx0, idx, #seq) ==>
+      )
+      \replacewith(
+          traced(idx0, idx + 1, seqConcatEnd(#seq, seqSingleton('1'))) ==>
+      )
+      \heuristics(simplify)
+    };
+
+    printTracedElse {
+      \assumes(
+          ==> traceIf(idx)
+      )
+      \find(
+          traced(idx0, idx, #seq) ==>
+      )
+      \replacewith(
+          traced(idx0, idx + 1, seqConcatEnd(#seq, seqSingleton('0'))) ==>
+      )
+      \heuristics(simplify)
+    };
+
+    seqConcatEndNormalize {
+       \schemaVar \term Seq slit1, slit2;
+       \schemaVar \term int v;
+       \find (seqConcatEnd(seqConcat(slit1, slit2),seqSingleton(v)))
+       \replacewith( seqConcat(slit1,seqConcatEnd(slit2,seqSingleton(v))))
+       \heuristics(simplify)
+    };
+
+    seqConcatEndNormalize2 {
+       \schemaVar \term int v;
+       \find (seqConcatEnd(seqEmpty,seqSingleton(v)))
+       \replacewith( seqSingleton(v))
+       \heuristics(simplify)
+    };
+
+    seqConcatEndNormalize3 {
+       \schemaVar \term int v1, v2;
+       \find (seqConcatEnd(seqSingleton(v1),seqSingleton(v2)))
+       \replacewith(seqConcat(seqSingleton(v1),seqSingleton(v2)))
+       \heuristics(simplify)
+    };
+
+
+    /*
+     * Short circuit rules that don't interfere with if/else tracing
+     * [they don't translate to if (*) * else *, only to JavaDL \if(*) \then (*) \else (*)]
+     */
+    compound_assignment_3_nonsimple_new {
+        \find(\modality{#allmodal}{.. #lhs=#nse0 && #nse1; ...}\endmodality (post))
+
+        \varcond(\new(#v0, boolean))
+        \replacewith(\modality{#allmodal}{.. boolean #v0 = #nse0;
+                #lhs = #v0 && #nse1; ...}\endmodality (post))
+
+        \heuristics(simplify_expression)
+        \displayname "compound_assignment"
+    };
+
+    compound_assignment_3_reverse_mixed {
+        \find(\modality{#allmodal}{.. #lhs=#seBool0 && #nse1; ...}\endmodality (post))
+
+        \replacewith(
+            \if(#seBool0 = TRUE)
+            \then(\modality{#allmodal}{.. #lhs = #nse1; ...}\endmodality (post))
+            \else({#lhs := FALSE}\modality{#allmodal}{.. ...}\endmodality (post))
+        )
+
+        \heuristics(simplify_expression)
+        \displayname "assignment_and"
+    };
+
+    compound_assignment_5_nonsimple_new {
+        \find(\modality{#allmodal}{.. #lhs=#nse0 || #nse1; ...}\endmodality (post))
+
+        \varcond(\new(#v0, boolean))
+        \replacewith(\modality{#allmodal}{.. boolean #v0 = #nse0;
+                #lhs = #v0 || #nse1; ...}\endmodality (post))
+
+        \heuristics(simplify_expression)
+        \displayname "compound_assignment"
+    };
+
+    compound_assignment_5_reverse_mixed {
+        \find(\modality{#allmodal}{.. #lhs=#seBool0 || #nse1; ...}\endmodality (post))
+
+        \replacewith(
+            \if(#seBool0 = TRUE)
+            \then({#lhs := TRUE}\modality{#allmodal}{.. ...}\endmodality (post))
+            \else(\modality{#allmodal}{.. #lhs = #nse1; ...}\endmodality (post))
+        )
+
+        \heuristics(simplify_expression)
+        \displayname "assignment_or"
+    };
+
+    condition_mixed_left {
+        \find(\modality{#allmodal}{.. #lhs = #se0 ? #nse1 : #se2; ...}\endmodality (post))
+
+        \replacewith(
+            \if(#se0 = TRUE)
+            \then(\modality{#allmodal}{.. #lhs = #nse1; ...}\endmodality (post))
+            \else({#lhs := #se2}\modality{#allmodal}{.. ...}\endmodality (post))
+        )
+
+        \heuristics(simplify_prog)
+        \displayname "condition"
+    };
+
+    condition_mixed_right {
+        \find(\modality{#allmodal}{.. #lhs = #se0 ? #se1 : #nse2; ...}\endmodality (post))
+
+        \replacewith(
+            \if(#se0 = TRUE)
+            \then({#lhs := #se1}\modality{#allmodal}{.. ...}\endmodality (post))
+            \else(\modality{#allmodal}{.. #lhs = #nse2; ...}\endmodality (post))
+        )
+
+        \heuristics(simplify_prog)
+        \displayname "condidion"
+    };
+
+    condition_mixed {
+        \find(\modality{#allmodal}{.. #lhs = #se0 ? #nse1 : #nse2; ...}\endmodality (post))
+
+        \replacewith(
+            \if(#se0 = TRUE)
+            \then(\modality{#allmodal}{.. #lhs = #nse1; ...}\endmodality (post))
+            \else(\modality{#allmodal}{.. #lhs = #nse2; ...}\endmodality (post))
+        )
+
+        \heuristics(simplify_prog)
+        \displayname "condition"
+    };
+}
diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key
index c4317a71342..172ecb7d922 100644
--- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key
+++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key
@@ -93,6 +93,7 @@
     \term G updatedTerm1, updatedTerm2;
 }
 
+
 \rules(programRules:Java, JavaCard:on) {
 
     getJavaCardTransient {
@@ -496,7 +497,10 @@
         \replacewith(false)
         \heuristics(simplify_prog)
     };
+}
 
+// tryCatchThrow refactors to if/else which interferes with tracing
+\rules (programRules:Java, tracing:off) {
     tryCatchThrow {
         \find(\modality{#allmodal}{.. try { throw #se; #slist }
                 catch ( #t #v0 ) { #slist1 } ...}\endmodality (post))
@@ -580,7 +584,9 @@
         \heuristics(simplify_prog)
         \displayname "tryFinallyThrow"
     };
+}
 
+\rules (programRules:Java) {
     tryEmpty {
         \find(\modality{#allmodal}{.. try {} #cs ...}\endmodality (post))
         \replacewith(\modality{#allmodal}{.. ...}\endmodality (post))
@@ -1262,6 +1268,10 @@
         \displayname "ifElseUnfold"
     };
 
+
+}
+
+\rules (programRules:Java, tracing:off) {
     if {
         \find(\modality{#allmodal}{.. if(#se) #s0  ...}\endmodality (post))
         \replacewith(\if(#se = TRUE) \then(\modality{#allmodal}{.. #s0 ...}\endmodality (post))
@@ -1398,6 +1408,9 @@
         \replacewith(\modality{#allmodal}{.. #switch-to-if(#sw) ...}\endmodality (post))
         \heuristics(simplify_prog)
     };
+}
+
+\rules(programRules:Java) {
 
     // --------------- labels and blocks ------------------------------------------//
 
@@ -1528,19 +1541,23 @@
     // ------------------------------------------------------------------------
     // ------------ Rules for conditional expression
     // ------------------------------------------------------------------------
+}
 
-
+// unsound with if/else tracing (uses if (*) {*} else {*})
+\rules (programRules:Java, tracing:off) {
     condition {
         \find(\modality{#allmodal}{.. #lhs = #e0 ? #e1 : #e2; ...}\endmodality (post))
         \replacewith(\modality{#allmodal}{.. if(#e0) {#lhs = #e1;}
                 else {#lhs = #e2;} ...}\endmodality (post))
         \heuristics(simplify_prog, split_if)
     };
+}
 
+\rules (programRules:Java) {
     condition_not_simple {
-        \find(\modality{#allmodal}{.. #lhs = #nse ? #se1 : #se2; ...}\endmodality (post))
+        \find(\modality{#allmodal}{.. #lhs = #nse ? #e1 : #e2; ...}\endmodality (post))
         \varcond(\newTypeOf(#v0, #nse))
-        \replacewith(\modality{#allmodal}{.. #typeof(#nse) #v0 = #nse; #lhs = #v0 ? #se1 : #se2; ...}\endmodality (post))
+        \replacewith(\modality{#allmodal}{.. #typeof(#nse) #v0 = #nse; #lhs = #v0 ? #e1 : #e2; ...}\endmodality (post))
         \heuristics(simplify_prog)
         \displayname "condition"
     };
@@ -2668,14 +2685,19 @@
         \heuristics(simplify_expression)
         \displayname "compound_assignment"
     };
+}
 
+// the following rule refactors operator * && * to if (*) * else *, which is unsound for tracing
+\rules (programRules:Java, tracing:off) {
     compound_assignment_3_nonsimple {
         \find(\modality{#allmodal}{.. #lhs=#exBool0 && #nseBool1; ...}\endmodality (post))
         \replacewith(\modality{#allmodal}{.. if (!#exBool0) #lhs=false; else #lhs=#nseBool1; ...}\endmodality (post))
         \heuristics(simplify_expression, split_if)
-        \displayname "compound_assignment"
+        \displayname "assignment_and"
     };
+}
 
+\rules (programRules:Java) {
     compound_assignment_3_mixed {
         \find(\modality{#allmodal}{.. #lhs=#nseBool0 && #seBool1; ...}\endmodality (post))
         \varcond(\new(#v0, boolean))
@@ -2706,16 +2728,21 @@
         \replacewith({#lhs := \if(#seBool0 = TRUE) \then(\if(#seBool1 = TRUE) \then(TRUE) \else(FALSE)) \else(FALSE)}
             \modality{#allmodal}{.. ...}\endmodality (post))
         \heuristics(simplify_expression)
-        \displayname "assignment_and"
+        \displayname "bitwise_and"
     };
+}
 
+// the following rule refactors operator * || * to if (*) * else *, which unsound for tracing
+\rules (programRules:Java, tracing:off) {
     compound_assignment_5_nonsimple {
         \find(\modality{#allmodal}{.. #lhs=#exBool0 || #nseBool1; ...}\endmodality (post))
         \replacewith(\modality{#allmodal}{.. if (#exBool0) #lhs=true; else #lhs=#nseBool1; ...}\endmodality (post))
         \heuristics(simplify_expression, split_if)
-        \displayname "compound_assignment"
+        \displayname "assignment_or"
     };
+}
 
+\rules (programRules:Java) {
     compound_assignment_5_mixed {
         \find(\modality{#allmodal}{.. #lhs=#nseBool0 || #seBool1; ...}\endmodality (post))
         \varcond(\new(#v0, boolean))
@@ -2746,7 +2773,7 @@
         \replacewith({#lhs := \if(#seBool0 = TRUE) \then(TRUE) \else(\if(#seBool1 = TRUE) \then(TRUE) \else(FALSE))}
             \modality{#allmodal}{.. ...}\endmodality (post))
         \heuristics(simplify_expression)
-        \displayname "assignment_or"
+        \displayname "bitwise_or"
     };
 
     compound_assignment_xor_nonsimple {
diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/optionsDeclarations.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/optionsDeclarations.key
index aac46391232..5570d0bf720 100644
--- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/optionsDeclarations.key
+++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/optionsDeclarations.key
@@ -146,6 +146,8 @@
     moreSeqRules: {off, on};
     /*! Loading rules dealing with reachability can be disabled. */
     reach: {on, off};
+    /*! Tracing or retracing rules (currently only if/else). */
+    tracing: {off, on};
     /*!
     Loading less commonly used rules for (mathematical) integers,
     such as rules for bounded sums and products, modulo, or polynomials,
diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ruleSetsDeclarations.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ruleSetsDeclarations.key
index 8141bd44ac4..8608203f3c8 100644
--- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ruleSetsDeclarations.key
+++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ruleSetsDeclarations.key
@@ -299,4 +299,7 @@
 
     // double
     executeDoubleAssignment;
+
+    // tracing
+    retrace;
 }
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 aa9fe04c2ee..cf352338dae 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
@@ -372,6 +372,10 @@ public static ProofCollection automaticJavaDL() throws IOException {
         g.provable("sort.key");
         g.provable("split.key");
 
+        //g = c.group("path_validation");
+        // TODO add tracing:on to the settings
+        //g.setLocalSettings("[Choice]DefaultChoices=moreSeqRules-moreSeqRules:on");
+        //g.provable("heap/pathValidation/quicksort.key");
 
         /*
          * These are simpler regression tests that show a certain feature works
diff --git a/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt b/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt
index 2e397ca646a..0153094ffcb 100644
--- a/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt
+++ b/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt
@@ -1,5 +1,5 @@
 # This files contains representation of taclets, which are accepted and revised.
-# Date: Wed Jun 26 12:45:30 CEST 2024
+# Date: Tue Aug 06 18:14:22 CEST 2024
 
 == abortJavaCardTransactionAPI (abortJavaCardTransactionAPI) =========================================
 abortJavaCardTransactionAPI {
@@ -3733,7 +3733,7 @@ compound_assignment_3_mixed {
 \heuristics(simplify_expression)
 Choices: programRules:Java}
 -----------------------------------------------------
-== compound_assignment_3_nonsimple (compound_assignment) =========================================
+== compound_assignment_3_nonsimple (assignment_and) =========================================
 compound_assignment_3_nonsimple {
 \find(#allmodal ((modal operator))|{{ ..
   #lhs = #exBool0 && #nseBool1;
@@ -3743,7 +3743,7 @@ compound_assignment_3_nonsimple {
   else #lhs = #nseBool1;
 ... }}| (post)) 
 \heuristics(split_if, simplify_expression)
-Choices: programRules:Java}
+Choices: (programRules:Java & tracing:off)}
 -----------------------------------------------------
 == compound_assignment_3_simple (assignment_and) =========================================
 compound_assignment_3_simple {
@@ -3768,7 +3768,7 @@ compound_assignment_4_nonsimple {
 \heuristics(simplify_expression)
 Choices: programRules:Java}
 -----------------------------------------------------
-== compound_assignment_4_simple (assignment_and) =========================================
+== compound_assignment_4_simple (bitwise_and) =========================================
 compound_assignment_4_simple {
 \find(#allmodal ((modal operator))|{{ ..
   #lhs = #seBool0 & #seBool1;
@@ -3790,7 +3790,7 @@ compound_assignment_5_mixed {
 \heuristics(simplify_expression)
 Choices: programRules:Java}
 -----------------------------------------------------
-== compound_assignment_5_nonsimple (compound_assignment) =========================================
+== compound_assignment_5_nonsimple (assignment_or) =========================================
 compound_assignment_5_nonsimple {
 \find(#allmodal ((modal operator))|{{ ..
   #lhs = #exBool0 || #nseBool1;
@@ -3800,7 +3800,7 @@ compound_assignment_5_nonsimple {
   else #lhs = #nseBool1;
 ... }}| (post)) 
 \heuristics(split_if, simplify_expression)
-Choices: programRules:Java}
+Choices: (programRules:Java & tracing:off)}
 -----------------------------------------------------
 == compound_assignment_5_simple (assignment_or) =========================================
 compound_assignment_5_simple {
@@ -3825,7 +3825,7 @@ compound_assignment_6_nonsimple {
 \heuristics(simplify_expression)
 Choices: programRules:Java}
 -----------------------------------------------------
-== compound_assignment_6_simple (assignment_or) =========================================
+== compound_assignment_6_simple (bitwise_or) =========================================
 compound_assignment_6_simple {
 \find(#allmodal ((modal operator))|{{ ..
   #lhs = #seBool0 | #seBool1;
@@ -5032,17 +5032,17 @@ condition {
   }
 ... }}| (post)) 
 \heuristics(split_if, simplify_prog)
-Choices: programRules:Java}
+Choices: (programRules:Java & tracing:off)}
 -----------------------------------------------------
 == condition_not_simple (condition) =========================================
 condition_not_simple {
 \find(#allmodal ((modal operator))|{{ ..
-  #lhs = #nse ? #se1 : #se2;
+  #lhs = #nse ? #e1 : #e2;
 ... }}| (post))
 \varcond(\new(#v0 (program Variable), \typeof(#nse (program NonSimpleExpression))))
 \replacewith(#allmodal ((modal operator))|{{ ..
   #typeof(#nse) #v0 = #nse;
-  #lhs = #v0 ? #se1 : #se2;
+  #lhs = #v0 ? #e1 : #e2;
 ... }}| (post)) 
 \heuristics(simplify_prog)
 Choices: programRules:Java}
@@ -9922,7 +9922,7 @@ if {
   #s0
 ... }}| (post),#allmodal(post))) 
 
-Choices: programRules:Java}
+Choices: (programRules:Java & tracing:off)}
 -----------------------------------------------------
 == ifElse (ifElse) =========================================
 ifElse {
@@ -9936,7 +9936,7 @@ ifElse {
   #s1
 ... }}| (post))) 
 
-Choices: programRules:Java}
+Choices: (programRules:Java & tracing:off)}
 -----------------------------------------------------
 == ifElseFalse (ifElseFalse) =========================================
 ifElseFalse {
@@ -9949,7 +9949,7 @@ ifElseFalse {
   #s1
 ... }}| (post)]) 
 \heuristics(simplify_prog)
-Choices: programRules:Java}
+Choices: (programRules:Java & tracing:off)}
 -----------------------------------------------------
 == ifElseSkipElse (ifElseSkipElse) =========================================
 ifElseSkipElse {
@@ -9963,7 +9963,7 @@ ifElseSkipElse {
   #s0
 ... }}| (post)) 
 \heuristics(simplify)
-Choices: programRules:Java}
+Choices: (programRules:Java & tracing:off)}
 -----------------------------------------------------
 == ifElseSkipElseConditionInBlock (ifElseSkipElse) =========================================
 ifElseSkipElseConditionInBlock {
@@ -9981,7 +9981,7 @@ ifElseSkipElseConditionInBlock {
   #s0
 ... }}| (post)) 
 \heuristics(simplify)
-Choices: programRules:Java}
+Choices: (programRules:Java & tracing:off)}
 -----------------------------------------------------
 == ifElseSkipThen (ifElseSkipThen) =========================================
 ifElseSkipThen {
@@ -9995,7 +9995,7 @@ ifElseSkipThen {
   #s1
 ... }}| (post)) 
 \heuristics(simplify)
-Choices: programRules:Java}
+Choices: (programRules:Java & tracing:off)}
 -----------------------------------------------------
 == ifElseSkipThenConditionInBlock (ifElseSkipThen) =========================================
 ifElseSkipThenConditionInBlock {
@@ -10013,7 +10013,7 @@ ifElseSkipThenConditionInBlock {
   #s1
 ... }}| (post)) 
 \heuristics(simplify)
-Choices: programRules:Java}
+Choices: (programRules:Java & tracing:off)}
 -----------------------------------------------------
 == ifElseSplit (ifElseSplit) =========================================
 ifElseSplit {
@@ -10028,7 +10028,7 @@ ifElseSplit {
   #s0
 ... }}| (post)]) 
 \heuristics(split_if)
-Choices: programRules:Java}
+Choices: (programRules:Java & tracing:off)}
 -----------------------------------------------------
 == ifElseSplitLeft (ifElseSplitLeft) =========================================
 ifElseSplitLeft {
@@ -10043,7 +10043,7 @@ ifElseSplitLeft {
   #s0
 ... }}| (post)]==>[]) 
 \heuristics(split_if)
-Choices: programRules:Java}
+Choices: (programRules:Java & tracing:off)}
 -----------------------------------------------------
 == ifElseTrue (ifElseTrue) =========================================
 ifElseTrue {
@@ -10056,7 +10056,7 @@ ifElseTrue {
   #s0
 ... }}| (post)]) 
 \heuristics(simplify_prog)
-Choices: programRules:Java}
+Choices: (programRules:Java & tracing:off)}
 -----------------------------------------------------
 == ifElseUnfold (ifElseUnfold) =========================================
 ifElseUnfold {
@@ -10087,7 +10087,7 @@ ifEnterThen {
   #s0
 ... }}| (post)) 
 \heuristics(simplify)
-Choices: programRules:Java}
+Choices: (programRules:Java & tracing:off)}
 -----------------------------------------------------
 == ifEnterThenConditionInBlock (ifEnterThen) =========================================
 ifEnterThenConditionInBlock {
@@ -10104,7 +10104,7 @@ ifEnterThenConditionInBlock {
   #s0
 ... }}| (post)) 
 \heuristics(simplify)
-Choices: programRules:Java}
+Choices: (programRules:Java & tracing:off)}
 -----------------------------------------------------
 == ifEqualsInteger (ifEqualsInteger) =========================================
 ifEqualsInteger {
@@ -10281,7 +10281,7 @@ ifFalse {
 ... }}| (post))
 \replacewith([]==>[#allmodal(post)]) 
 \heuristics(simplify_prog)
-Choices: programRules:Java}
+Choices: (programRules:Java & tracing:off)}
 -----------------------------------------------------
 == ifSkipThen (ifSkipThen) =========================================
 ifSkipThen {
@@ -10293,7 +10293,7 @@ ifSkipThen {
   #loc = false;
 ... }}| (post)) 
 \heuristics(simplify)
-Choices: programRules:Java}
+Choices: (programRules:Java & tracing:off)}
 -----------------------------------------------------
 == ifSkipThenConditionInBlock (ifSkipThen) =========================================
 ifSkipThenConditionInBlock {
@@ -10309,7 +10309,7 @@ ifSkipThenConditionInBlock {
   }
 ... }}| (post)) 
 \heuristics(simplify)
-Choices: programRules:Java}
+Choices: (programRules:Java & tracing:off)}
 -----------------------------------------------------
 == ifSplit (ifElseSplit) =========================================
 ifSplit {
@@ -10321,7 +10321,7 @@ ifSplit {
   #s0
 ... }}| (post)]) 
 \heuristics(split_if)
-Choices: programRules:Java}
+Choices: (programRules:Java & tracing:off)}
 -----------------------------------------------------
 == ifSplitLeft (ifSplitLeft) =========================================
 ifSplitLeft {
@@ -10333,7 +10333,7 @@ ifSplitLeft {
   #s0
 ... }}| (post)]==>[]) 
 \heuristics(split_if)
-Choices: programRules:Java}
+Choices: (programRules:Java & tracing:off)}
 -----------------------------------------------------
 == ifTrue (ifTrue) =========================================
 ifTrue {
@@ -10345,7 +10345,7 @@ ifTrue {
   #s0
 ... }}| (post)]) 
 \heuristics(simplify_prog)
-Choices: programRules:Java}
+Choices: (programRules:Java & tracing:off)}
 -----------------------------------------------------
 == ifUnfold (ifElseUnfold) =========================================
 ifUnfold {
@@ -17142,7 +17142,7 @@ switch {
   switch-to-if(#sw)
 ... }}| (post)) 
 \heuristics(simplify_prog)
-Choices: programRules:Java}
+Choices: (programRules:Java & tracing:off)}
 -----------------------------------------------------
 == switch_brackets (switch_brackets) =========================================
 switch_brackets {
@@ -17857,7 +17857,7 @@ tryCatchFinallyThrow {
   }
 ... }}| (post)) 
 \heuristics(simplify_prog)
-Choices: programRules:Java}
+Choices: (programRules:Java & tracing:off)}
 -----------------------------------------------------
 == tryCatchThrow (tryCatchThrow) =========================================
 tryCatchThrow {
@@ -17885,7 +17885,7 @@ tryCatchThrow {
   }
 ... }}| (post)) 
 \heuristics(simplify_prog)
-Choices: programRules:Java}
+Choices: (programRules:Java & tracing:off)}
 -----------------------------------------------------
 == tryEmpty (tryEmpty) =========================================
 tryEmpty {
@@ -18015,7 +18015,7 @@ tryFinallyThrow {
   }
 ... }}| (post)) 
 \heuristics(simplify_prog)
-Choices: programRules:Java}
+Choices: (programRules:Java & tracing:off)}
 -----------------------------------------------------
 == tryMultipleCatchThrow (tryCatchThrow) =========================================
 tryMultipleCatchThrow {
@@ -18051,7 +18051,7 @@ tryMultipleCatchThrow {
   }
 ... }}| (post)) 
 \heuristics(simplify_prog)
-Choices: programRules:Java}
+Choices: (programRules:Java & tracing:off)}
 -----------------------------------------------------
 == tryReturn (tryReturn) =========================================
 tryReturn {
diff --git a/key.ui/examples/heap/pathValidation/quicksort.key b/key.ui/examples/heap/pathValidation/quicksort.key
new file mode 100644
index 00000000000..e1e6b5d929e
--- /dev/null
+++ b/key.ui/examples/heap/pathValidation/quicksort.key
@@ -0,0 +1,85 @@
+\profile "Java Profile";
+
+\settings // Proof-Settings-Config-File
+{ 
+    "Choice" : { 
+        "JavaCard" : "JavaCard:off",
+        "Strings" : "Strings:on",
+        "assertions" : "assertions:safe",
+        "bigint" : "bigint:on",
+        "floatRules" : "floatRules:strictfpOnly",
+        "initialisation" : "initialisation:disableStaticInitialisation",
+        "intRules" : "intRules:arithmeticSemanticsIgnoringOF",
+        "integerSimplificationRules" : "integerSimplificationRules:full",
+        "javaLoopTreatment" : "javaLoopTreatment:efficient",
+        "mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off",
+        "methodExpansion" : "methodExpansion:modularOnly",
+        "modelFields" : "modelFields:treatAsAxiom",
+        "moreSeqRules" : "moreSeqRules:on",
+        "permissions" : "permissions:off",
+        "programRules" : "programRules:Java",
+        "reach" : "reach:on",
+        "runtimeExceptions" : "runtimeExceptions:ban",
+        "sequences" : "sequences:on",
+        "wdChecks" : "wdChecks:off",
+        "wdOperator" : "wdOperator:L"
+     },
+    "Labels" : { 
+        "UseOriginLabels" : true
+     },
+    "NewSMT" : { 
+        
+     },
+    "SMTSettings" : { 
+        "SelectedTaclets" : [ 
+            
+         ],
+        "UseBuiltUniqueness" : false,
+        "explicitTypeHierarchy" : false,
+        "instantiateHierarchyAssumptions" : true,
+        "integersMaximum" : 2147483645,
+        "integersMinimum" : -2147483645,
+        "invariantForall" : false,
+        "maxGenericSorts" : 2,
+        "useConstantsForBigOrSmallIntegers" : true,
+        "useUninterpretedMultiplication" : true
+     },
+    "Strategy" : { 
+        "ActiveStrategy" : "JavaCardDLStrategy",
+        "MaximumNumberOfAutomaticApplications" : 100000,
+        "Timeout" : -1,
+        "options" : { 
+            "AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF",
+            "BLOCK_OPTIONS_KEY" : "BLOCK_EXPAND",
+            "CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_FREE",
+            "DEP_OPTIONS_KEY" : "DEP_ON",
+            "INF_FLOW_CHECK_PROPERTY" : "INF_FLOW_CHECK_FALSE",
+            "LOOP_OPTIONS_KEY" : "LOOP_EXPAND",
+            "METHOD_OPTIONS_KEY" : "METHOD_EXPAND",
+            "MPS_OPTIONS_KEY" : "MPS_MERGE",
+            "NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_DEF_OPS",
+            "OSS_OPTIONS_KEY" : "OSS_ON",
+            "QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS",
+            "QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_ON",
+            "QUERY_NEW_OPTIONS_KEY" : "QUERY_OFF",
+            "SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED",
+            "STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT",
+            "SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER",
+            "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF",
+            "USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF",
+            "USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF",
+            "USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF",
+            "VBT_PHASE" : "VBT_SYM_EX"
+         }
+     }
+ } 
+
+\javaSource "quicksort";
+
+\proofObligation 
+// Proof-Obligation settings
+{ 
+    "class" : "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO",
+    "contract" : "quicksort.Quicksort[quicksort.Quicksort::sort([I)].JML normal_behavior operation contract.0",
+    "name" : "quicksort.Quicksort[quicksort.Quicksort::sort([I)].JML normal_behavior operation contract.0"
+ }
diff --git a/key.ui/examples/heap/pathValidation/quicksort/Quicksort.java b/key.ui/examples/heap/pathValidation/quicksort/Quicksort.java
new file mode 100644
index 00000000000..26ceb2d1ea7
--- /dev/null
+++ b/key.ui/examples/heap/pathValidation/quicksort/Quicksort.java
@@ -0,0 +1,111 @@
+/**
+ * This example formalizes and verifies the wellknown quicksort
+ * algorithm for int-arrays algorithm.  It shows that the array
+ * is sorted in  the end and that it contains  a permutation of
+ * the original input.
+ *
+ * The   proofs   for   the  main   method   sort(int[])   runs
+ * automatically   while   the   other  two   methods   require
+ * interaction.  You   can  load   the  files   "sort.key"  and
+ * "split.key"  from the  example's  directory  to execute  the
+ * according proof scripts.
+ *
+ * The permutation property requires some interaction: The idea
+ * is that the only actual modification on the array are swaps
+ * within the "split" method. The sort method body contains
+ * three method invocations which each maintain the permutation
+ * property. By a repeated appeal to the transitivity of the
+ * permutation property, the entire algorithm can be proved to
+ * only permute the array.
+ *
+ * To establish  monotonicity, the key  is to specify  that the
+ * currently  handled block  contains  only  numbers which  are
+ * between   the    two   pivot   values    array[from-1]   and
+ * array[to]. The first  and last block are exempt  from one of
+ * these  conditions  since  they have  only  one  neighbouring
+ * block.
+ *
+ * The  example has  been  added  to show  the  power of  proof
+ * scripts.
+ *
+ * @author Mattias Ulbrich, 2015
+ *
+ * Modified  to run fully automatically for Retrospective  Path
+ * Validation. This is a form of partial verification. We first
+ * record a control flow trace (instrumentation for a automatic
+ * recording can be done with the help of JavaParser)  and then
+ * we validate the the single recorded control flow against the
+ * specification (the method contract). No auxialliary specifi-
+ * cation needed (no loop invariants, no contracts  for  called
+ * methods, no proof scripts)!
+ *
+ * KeY Strategy Settings:
+ *   Loop Treatment: Expand (Transformation)
+ *   Method Treatment: Expand
+ *
+ * Or just load quicksort.key
+ *
+ * Lukas Gra"tz, 2023/24
+ */
+
+package quicksort;
+
+class Quicksort {
+
+    /*@ public normal_behaviour
+      @
+      @ //-- Below is the recorded control flow trace
+      @ //-- (rules for predicates trace_O() & I(), traceIndex() are included in this KeY-version)
+      @ requires tracer.Trace.index == 0;
+      @ requires \dl_traceAfter(0, "111010101000110111000110000");
+      @
+      @  ensures tracer.Trace.index == 27;
+      @
+      @  //-- the following ensures with seqPerm cannot be shown in auto mode with default options:
+      @  //ensures \dl_seqPerm(\dl_array2seq(array), \old(\dl_array2seq(array)));
+      @  //-- equivalent ensures with \num_of:
+      @  ensures (\forall int j; 0<=j && j < array.length;
+      @               (\num_of int i; 0<=i && i < array.length; \old(array[i]) == array[j])
+      @            == (\num_of int i; 0<=i && i < array.length;      array[i]  == array[j])
+      @          );
+      @
+      @  ensures (\forall int i; 0<=i && i<array.length-1; array[i] <= array[i+1]);
+      @
+      @
+      @  assignable array[*], tracer.Trace.index;
+      @*/
+    public static void sort(int[] array) {
+        if(array.length > 0) { // 0
+            sort(array, 0, array.length-1);
+        }
+    }
+
+    private static void sort(int[] array, int from, int to) {
+        if(from < to) { // 1, 12, 21
+            int splitPoint = split(array, from, to);
+            sort(array, from, splitPoint-1);
+            sort(array, splitPoint+1, to);
+        } // 11, 20, 25, 26
+    }
+
+    private static int split(int[] array, int from, int to) {
+
+        int i = from;
+        int pivot = array[to];
+
+        for(int j = from; j < to; j++) { // 2, 4, 6, 8, 13, 15, 17, 22
+            if(array[j] <= pivot) { // 16
+                int t = array[i];
+                array[i] = array[j];
+                array[j] = t;
+                i++;
+            } // 3, 5, 7, 9, 14, 18, 23
+        } // 10, 19, 24
+
+        array[to] = array[i];
+        array[i] = pivot;
+
+        return i;
+
+    }
+}