From 616b08e28ebe78152650fa2e1e6eba2427a93b13 Mon Sep 17 00:00:00 2001
From: Alexander Weigl <weigl@kit.edu>
Date: Wed, 19 Aug 2026 18:03:24 +0200
Subject: [PATCH 1/4] add `x instanceof T y`

---
 key.core/src/main/antlr4/JavaKeYLexer.g4      |   2 +
 key.core/src/main/antlr4/JavaKeYParser.g4     |   2 +
 .../expression/operator/BinaryOperator.java   |  14 +-
 .../operator/InstanceofPattern.java           | 142 ++++++++++
 .../ilkd/key/java/loader/JP2KeYConverter.java |  45 +++-
 .../java/visitor/BindingVariableVisitor.java  | 128 +++++++++
 .../key/java/visitor/CreatingASTVisitor.java  |  11 +
 .../ilkd/key/java/visitor/JavaASTVisitor.java |   5 +
 .../de/uka/ilkd/key/java/visitor/Visitor.java |   2 +
 .../varexp/TacletBuilderManipulators.java     |  14 +-
 .../de/uka/ilkd/key/pp/PrettyPrinter.java     |  22 ++
 .../conditions/AbnormallyTerminatesCond.java  |  59 ++++
 .../AlwaysAbnormallyTerminatingAnalysis.java  | 255 ++++++++++++++++++
 .../conditions/BindingExpressionCond.java     | 102 +++++++
 .../jml/translation/JMLSpecFactory.java       |  40 ++-
 .../de/uka/ilkd/key/proof/rules/java5.key     |   4 +-
 .../de/uka/ilkd/key/proof/rules/javaRules.key |  78 +++++-
 ...waysAbnormallyTerminatingAnalysisTest.java | 127 +++++++++
 .../Java/InstanceOfPattern/README.txt         |  72 +++++
 .../Java/InstanceOfPattern/project.key        |   3 +
 .../src/InstanceOfPatternExample.java         | 149 ++++++++++
 key.ui/examples/index/samplesIndex.txt        |   1 +
 22 files changed, 1266 insertions(+), 11 deletions(-)
 create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/InstanceofPattern.java
 create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/visitor/BindingVariableVisitor.java
 create mode 100644 key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AbnormallyTerminatesCond.java
 create mode 100644 key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AlwaysAbnormallyTerminatingAnalysis.java
 create mode 100644 key.core/src/main/java/de/uka/ilkd/key/rule/conditions/BindingExpressionCond.java
 create mode 100644 key.core/src/test/java/de/uka/ilkd/key/rule/conditions/AlwaysAbnormallyTerminatingAnalysisTest.java
 create mode 100644 key.ui/examples/Java/InstanceOfPattern/README.txt
 create mode 100644 key.ui/examples/Java/InstanceOfPattern/project.key
 create mode 100644 key.ui/examples/Java/InstanceOfPattern/src/InstanceOfPatternExample.java

diff --git a/key.core/src/main/antlr4/JavaKeYLexer.g4 b/key.core/src/main/antlr4/JavaKeYLexer.g4
index 9ea0ac834ee..0a8e4f57d58 100644
--- a/key.core/src/main/antlr4/JavaKeYLexer.g4
+++ b/key.core/src/main/antlr4/JavaKeYLexer.g4
@@ -57,6 +57,8 @@ NEWLABEL : '\\newLabel';
 CONTAINS_ASSIGNMENT : '\\containsAssignment';
 // label occurs again for character `!'
 NOTFREEIN : '\\notFreeIn';
+ISBINDINGEXPR : '\\isBindingExpr';
+ALWAYS_ABNORMALLY_TERMINATES: '\\alwaysAbnormallyTerminates';
 STATIC : '\\static';
 STATICMETHODREFERENCE : '\\staticMethodReference';
 MAXEXPANDMETHOD : '\\mayExpandMethod';
diff --git a/key.core/src/main/antlr4/JavaKeYParser.g4 b/key.core/src/main/antlr4/JavaKeYParser.g4
index 48c37383526..84d79ebe253 100644
--- a/key.core/src/main/antlr4/JavaKeYParser.g4
+++ b/key.core/src/main/antlr4/JavaKeYParser.g4
@@ -247,6 +247,8 @@ varexpId: // weigl, 2021-03-12: This will be later just an arbitrary identifier.
   | STRICT ISSUBTYPE
   | DISJOINTMODULONULL
   | NOTFREEIN
+  | ISBINDINGEXPR
+  | ALWAYS_ABNORMALLY_TERMINATES
   | HASSORT
   | NEWLABEL
   | ISREFERENCE
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/BinaryOperator.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/BinaryOperator.java
index 4ae33f4fbbc..1eb895cad04 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/BinaryOperator.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/BinaryOperator.java
@@ -8,11 +8,7 @@
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.java.TypeConverter;
-import de.uka.ilkd.key.java.ast.Comment;
-import de.uka.ilkd.key.java.ast.PositionInfo;
-import de.uka.ilkd.key.java.ast.ProgramElement;
-import de.uka.ilkd.key.java.ast.ProgramElementWithKind;
-import de.uka.ilkd.key.java.ast.SourceData;
+import de.uka.ilkd.key.java.ast.*;
 import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType;
 import de.uka.ilkd.key.java.ast.expression.Expression;
 import de.uka.ilkd.key.java.ast.expression.Operator;
@@ -110,4 +106,12 @@ public boolean equals(Object o) {
     protected int computeHashCode() {
         return 0x01000193 * super.computeHashCode() + kind.hashCode();
     }
+
+    public Expression getLeft() {
+        return this.getExpressionAt(0);
+    }
+
+    public Expression getRight() {
+        return this.getExpressionAt(1);
+    }
 }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/InstanceofPattern.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/InstanceofPattern.java
new file mode 100644
index 00000000000..8e3166edcd6
--- /dev/null
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/InstanceofPattern.java
@@ -0,0 +1,142 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package de.uka.ilkd.key.java.ast.expression.operator;
+
+import java.util.List;
+import java.util.Objects;
+
+import de.uka.ilkd.key.java.Services;
+import de.uka.ilkd.key.java.ast.*;
+import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType;
+import de.uka.ilkd.key.java.ast.abstraction.PrimitiveType;
+import de.uka.ilkd.key.java.ast.declaration.VariableSpecification;
+import de.uka.ilkd.key.java.ast.expression.Expression;
+import de.uka.ilkd.key.java.ast.reference.ExecutionContext;
+import de.uka.ilkd.key.java.ast.reference.TypeReference;
+import de.uka.ilkd.key.java.visitor.Visitor;
+
+import org.key_project.util.ExtList;
+import org.key_project.util.collection.ImmutableArray;
+
+import org.jspecify.annotations.NullMarked;
+
+/**
+ * Instanceof with pattern matching (Java 16+).
+ * Supports syntax: expr instanceof Type varName
+ * where varName is bound as a local variable in the true branch.
+ */
+@NullMarked
+public class InstanceofPattern extends TypeOperator {
+    protected final VariableSpecification patternVariable;
+
+    public InstanceofPattern(ExtList children) {
+        super(children);
+        this.patternVariable =
+            Objects.requireNonNull(children.get(VariableSpecification.class));
+    }
+
+    public InstanceofPattern(Expression lhs, TypeReference type, VariableSpecification patternVar) {
+        super(lhs, type);
+        this.patternVariable = Objects.requireNonNull(patternVar);
+    }
+
+    public InstanceofPattern(PositionInfo pi, List<Comment> c, Expression lhs, TypeReference type,
+            VariableSpecification patternVar) {
+        super(pi, c, new ImmutableArray<>(lhs), type);
+        this.patternVariable = Objects.requireNonNull(patternVar);
+    }
+
+    /**
+     * Returns the number of children of this node.
+     *
+     * @return an int giving the number of children of this node
+     */
+    public int getChildCount() {
+        int result = 0;
+        if (children != null) {
+            result += children.size();
+        }
+        if (typeReference != null) {
+            result++;
+        }
+
+        result++;
+        assert result == 3;
+        return result;
+    }
+
+    public SourceElement getLastElement() {
+        return patternVariable;
+    }
+
+    /**
+     * Returns the child at the specified index in this node's "virtual" child array
+     *
+     * @param index an index into this node's "virtual" child array
+     * @return the program element at the given position
+     * @throws ArrayIndexOutOfBoundsException if <tt>index</tt> is out of bounds
+     */
+    public ProgramElement getChildAt(int index) {
+        return switch (index) {
+            case 0 -> children.get(0);
+            case 1 -> typeReference;
+            case 2 -> patternVariable;
+            default -> throw new IllegalStateException("Unexpected value: " + index);
+        };
+    }
+
+    /**
+     * Get arity.
+     *
+     * @return the int value.
+     */
+    public int getArity() {
+        return 1;
+    }
+
+    /**
+     * Get precedence.
+     *
+     * @return the int value.
+     */
+    public int getPrecedence() {
+        return 5;
+    }
+
+    /**
+     * Get notation.
+     *
+     * @return the int value.
+     */
+    public int getNotation() {
+        return POSTFIX;
+    }
+
+    /**
+     * Get the pattern variable bound by this instanceof expression.
+     *
+     * @return the VariableSpecification for the pattern variable, or null if no pattern
+     */
+    public VariableSpecification getPatternVariable() {
+        return patternVariable;
+    }
+
+    /**
+     * calls the corresponding method of a visitor in order to perform some action/transformation on
+     * this element
+     *
+     * @param v the Visitor
+     */
+    public void visit(Visitor v) {
+        v.performActionOnInstanceofPattern(this);
+    }
+
+    public KeYJavaType getKeYJavaType(Services javaServ) {
+        return javaServ.getJavaInfo().getKeYJavaType(PrimitiveType.JAVA_BOOLEAN);
+    }
+
+    public KeYJavaType getKeYJavaType(Services javaServ, ExecutionContext ec) {
+        return getKeYJavaType(javaServ);
+    }
+}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java b/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java
index 773c8bcbb0b..20b7066e6f5 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java
@@ -924,6 +924,31 @@ public Object visit(InstanceOfExpr n, Void arg) {
         List<Comment> c = createComments(n);
         Expression lhs = accept(n.getExpression());
         TypeReference type = requireTypeReference(n.getType());
+
+        if (n.getName().isPresent()) {
+            final SimpleName nName = n.getName().get();
+            var name = nName.getIdentifier();
+
+            PositionInfo piVar = createPositionInfo(nName);
+            List<Comment> cVar = createComments(nName);
+
+            IProgramVariable pvar;
+            if (!name.startsWith("#")) {
+                pvar = new LocationVariable(
+                    new ProgramElementName(name), type.getKeYJavaType());
+            } else {
+                pvar = (ProgramSV) lookupSchemaVariable(nName);
+            }
+
+            final var vs =
+                new VariableSpecification(piVar, cVar, null, pvar, 0, type.getKeYJavaType());
+            return new InstanceofPattern(pi, c, lhs, type, vs);
+        }
+
+        if (n.getPattern().isPresent()) {
+            reportUnsupportedElement(n);
+        }
+
         return new Instanceof(pi, c, lhs, type);
     }
 
@@ -2178,7 +2203,25 @@ public Object visit(RecordPatternExpr n, Void arg) {
 
     @Override
     public Object visit(TypePatternExpr n, Void arg) {
-        return reportUnsupportedElement(n);
+        // weigl: This is somehow crude and called by a type resolution in NameExpr, expecting a
+        // VariableDeclaration
+        var nName = n.getName();
+        TypeRef type = accept(n.getType());
+        var name = nName.getIdentifier();
+
+        PositionInfo piVar = createPositionInfo(nName);
+        List<Comment> cVar = createComments(nName);
+
+        IProgramVariable pvar;
+        if (!name.startsWith("#")) {
+            pvar = new LocationVariable(
+                new ProgramElementName(name), type.getKeYJavaType());
+        } else {
+            pvar = (ProgramSV) lookupSchemaVariable(nName);
+        }
+
+        ImmutableArray<de.uka.ilkd.key.java.ast.declaration.Modifier> mods = map(n.getModifiers());
+        return new LocalVariableDeclaration(mods, type, new VariableSpecification(pvar));
     }
 
     @Override
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/BindingVariableVisitor.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/BindingVariableVisitor.java
new file mode 100644
index 00000000000..cd0fe5bee21
--- /dev/null
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/BindingVariableVisitor.java
@@ -0,0 +1,128 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package de.uka.ilkd.key.java.visitor;
+
+import java.util.*;
+
+import de.uka.ilkd.key.java.ast.expression.Expression;
+import de.uka.ilkd.key.java.ast.expression.ParenthesizedExpression;
+import de.uka.ilkd.key.java.ast.expression.operator.*;
+import de.uka.ilkd.key.logic.op.LocationVariable;
+
+/**
+ *
+ * @author Alexander Weigl
+ * @version 1 (20.08.26)
+ */
+public class BindingVariableVisitor {
+    public record Bindings(Map<LocationVariable, Expression> whenTrue,
+            Map<LocationVariable, Expression> whenFalse) {
+        public Bindings(Map<LocationVariable, Expression> whenTrue,
+                Map<LocationVariable, Expression> whenFalse) {
+            this.whenTrue = Collections.unmodifiableMap(whenTrue);
+            this.whenFalse = Collections.unmodifiableMap(whenFalse);
+        }
+
+        static Bindings empty() {
+            return new Bindings(Map.of(), Map.of());
+        }
+
+        @Override
+        public String toString() {
+            return "Bindings{whenTrue=" + whenTrue + ", whenFalse=" + whenFalse + "}";
+        }
+    }
+
+    public static Bindings analyze(Expression e) {
+        if (e instanceof InstanceofPattern io) {
+            // §6.3.1.5 — a instanceof p
+            // "when true" = variables declared by p. No "when false" rule:
+            // it can't be determined at compile time that the match failed
+            // in a way that still binds anything.
+            var name = (LocationVariable) io.getPatternVariable().getProgramVariable();
+            var expr = io.getExpressionAt(0);
+            return new Bindings(Map.of(name, expr), Map.of());
+        } else if (e instanceof BinaryOperator bo) {
+            if (bo.getKind() == BinaryOperatorKind.LOGICAL_AND) {
+                // §6.3.1.1 — a && b
+                Bindings a = analyze(bo.getExpressionAt(0));
+                Bindings b = analyze(bo.getExpressionAt(1));
+
+                requireDisjoint(a.whenTrue, b.whenTrue,
+                    "both operands of && declare pattern variable when true");
+                requireDisjoint(a.whenFalse, b.whenFalse,
+                    "both operands of && declare pattern variable when false");
+
+                // a's "when true" set is definitely matched at b (scope flows rightward).
+                var whenTrue = union(a.whenTrue, b.whenTrue);
+                // No rule for a && b when false: can't tell at compile time which
+                // operand caused the false result.
+                return new Bindings(whenTrue, Map.of());
+            } else if (bo.getKind() == BinaryOperatorKind.LOGICAL_OR) {
+                // §6.3.1.2 — a || b (mirror image of &&)
+                Bindings a = analyze(bo.getExpressionAt(0));
+                Bindings b = analyze(bo.getExpressionAt(1));
+
+                requireDisjoint(a.whenTrue, b.whenTrue,
+                    "both operands of || declare pattern variable when true");
+                requireDisjoint(a.whenFalse, b.whenFalse,
+                    "both operands of || declare pattern variable when false");
+                // a's "when false" set is definitely matched at b.
+                var whenFalse = union(a.whenFalse, b.whenFalse);
+                // No rule for a || b when true.
+                return new Bindings(Map.of(), whenFalse);
+            }
+        } else if (e instanceof UnaryOperator not && not.kind == UnaryOperatorKind.LOGICAL_NOT) {
+            // §6.3.1.3 — !a: true/false swap.
+            Bindings a = analyze(not.getExpressionAt(0));
+            return new Bindings(a.whenFalse, a.whenTrue);
+        } else if (e instanceof Conditional c) {
+            // §6.3.1.4 — a ? b : c
+            Bindings condB = analyze(c.getExpressionAt(0));
+            Bindings thenB = analyze(c.getExpressionAt(1));
+            Bindings elseB = analyze(c.getExpressionAt(2));
+            // (condB.whenTrue is definitely matched at b; condB.whenFalse at c —
+            // see DefinitelyMatchedAt below if you need those sets directly.)
+
+            requireDisjoint(condB.whenTrue, elseB.whenTrue,
+                "cond(true) and else-branch(true) both declare pattern variable");
+            requireDisjoint(condB.whenTrue, elseB.whenFalse,
+                "cond(true) and else-branch(false) both declare pattern variable");
+            requireDisjoint(condB.whenFalse, thenB.whenTrue,
+                "cond(false) and then-branch(true) both declare pattern variable");
+            requireDisjoint(condB.whenFalse, thenB.whenFalse,
+                "cond(false) and then-branch(false) both declare pattern variable");
+            requireDisjoint(thenB.whenTrue, elseB.whenTrue,
+                "then-branch(true) and else-branch(true) both declare pattern variable");
+            requireDisjoint(thenB.whenFalse, elseB.whenFalse,
+                "then-branch(false) and else-branch(false) both declare pattern variable");
+
+
+            // No rule for introducing bindings from a ? b : c itself, in either
+            // direction: it can't be known at compile time whether a is true.
+            return Bindings.empty();
+        } else if (e instanceof ParenthesizedExpression p) {
+            // §6.3.1.7 — (a): pass through unchanged.
+            return analyze(p.getExpressionAt(0));
+
+        }
+        return Bindings.empty();
+    }
+
+    private static Map<LocationVariable, Expression> union(Map<LocationVariable, Expression> a,
+            Map<LocationVariable, Expression> b) {
+        var result = new LinkedHashMap<>(a);
+        result.putAll(b);
+        return result;
+    }
+
+    private static void requireDisjoint(Map<LocationVariable, Expression> a,
+            Map<LocationVariable, Expression> b, String message) {
+        for (LocationVariable name : a.keySet()) {
+            if (b.containsKey(name)) {
+                throw new IllegalStateException(message + ": '" + name + "'");
+            }
+        }
+    }
+}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java
index 8a7e73b6849..bd61369a845 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java
@@ -469,6 +469,17 @@ ProgramElement createNewElement(ExtList changeList) {
         def.doAction(x);
     }
 
+    @Override
+    public void performActionOnInstanceofPattern(InstanceofPattern x) {
+        DefaultAction def = new DefaultAction(x) {
+            @Override
+            ProgramElement createNewElement(ExtList changeList) {
+                return new InstanceofPattern(changeList);
+            }
+        };
+        def.doAction(x);
+    }
+
     @Override
     public void performActionOnBreak(Break x) {
         DefaultAction def = new DefaultAction(x) {
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTVisitor.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTVisitor.java
index 10619d18977..7dea53d312e 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTVisitor.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTVisitor.java
@@ -248,6 +248,11 @@ public void performActionOnExactInstanceof(ExactInstanceof x) {
         doDefaultAction(x);
     }
 
+    @Override
+    public void performActionOnInstanceofPattern(InstanceofPattern x) {
+        doDefaultAction(x);
+    }
+
     @Override
     public void performActionOnExecutionContext(ExecutionContext x) {
         doDefaultAction(x);
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java
index 4cc400fdb05..cb47e524200 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java
@@ -157,6 +157,8 @@ public interface Visitor {
 
     void performActionOnExactInstanceof(ExactInstanceof x);
 
+    void performActionOnInstanceofPattern(InstanceofPattern x);
+
     void performActionOnNew(New x);
 
     void performActionOnTypeCast(TypeCast x);
diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java
index 67065ce497c..47e35ab0051 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java
@@ -167,6 +167,17 @@ public void apply(TacletBuilder<?> tacletBuilder, Object[] arguments,
     public static final TacletBuilderCommand NEW_LOCAL_VARS = new ConstructorBasedBuilder(
         "newLocalVars", NewLocalVarsCondition.class, SV, SV, SV, SV);
 
+    public static final TacletBuilderCommand BINDING_EXPRESSION_FULL = new ConstructorBasedBuilder(
+        "isBindingExpr", BindingExpressionCond.class, SV, SV, SV);
+
+    public static final TacletBuilderCommand ABNORMALLY_TERMINATE = new ConstructorBasedBuilder(
+        "alwaysAbnormallyTerminates", BindingExpressionCond.class, SV);
+
+
+    public static final TacletBuilderCommand BINDING_EXPRESSION_SIMPLE =
+        new ConstructorBasedBuilder(
+            "isBindingExpr", BindingExpressionCond.class, SV);
+
     static class NotFreeInTacletBuilderCommand extends AbstractTacletBuilderCommand {
         public NotFreeInTacletBuilderCommand(@NonNull ArgumentType... argumentsTypes) {
             super("notFreeIn", argumentsTypes);
@@ -382,7 +393,8 @@ public IsLabeledCondition build(Object[] arguments, List<String> parameters,
             applyUpdateOnRigid, DROP_EFFECTLESS_ELEMENTARIES, SIMPLIFY_ITE_UPDATE, SUBFORMULAS,
             STATIC_FIELD, MODEL_FIELD, SUBFORMULA, DROP_EFFECTLESS_STORES, EQUAL_UNIQUE,
             META_DISJOINT,
-            IS_OBSERVER, CONSTANT, HAS_SORT, LABEL, NEW_LABEL, HAS_ELEM_SORT, IS_IN_STRICTFP);
+            IS_OBSERVER, CONSTANT, HAS_SORT, LABEL, NEW_LABEL, HAS_ELEM_SORT, IS_IN_STRICTFP,
+            BINDING_EXPRESSION_FULL, BINDING_EXPRESSION_SIMPLE, ABNORMALLY_TERMINATE);
         register(STORE_TERM_IN, STORE_STMT_IN, HAS_INVARIANT, GET_INVARIANT, GET_FREE_INVARIANT,
             GET_VARIANT, IS_LABELED);
         loadWithServiceLoader();
diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java b/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java
index 09348df07c7..9108e6dbb35 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java
@@ -1310,6 +1310,28 @@ public void performActionOnExactInstanceof(ExactInstanceof x) {
         printInstanceOfLike(x, "exactInstanceof");
     }
 
+    @Override
+    public void performActionOnInstanceofPattern(InstanceofPattern x) {
+        boolean addParentheses = x.isToBeParenthesized();
+        if (addParentheses) {
+            layouter.print("(");
+        }
+        if (x.getArguments() != null) {
+            x.getExpressionAt(0).visit(this);
+        }
+        layouter.print(" instanceof ");
+        if (x.getTypeReference() != null) {
+            x.getTypeReference().visit(this);
+        }
+        if (x.getPatternVariable() != null) {
+            layouter.print(" ");
+            x.getPatternVariable().visit(this);
+        }
+        if (addParentheses) {
+            layouter.print(")");
+        }
+    }
+
     @Override
     public void performActionOnNew(New x) {
         boolean addParentheses = x.isToBeParenthesized();
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AbnormallyTerminatesCond.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AbnormallyTerminatesCond.java
new file mode 100644
index 00000000000..75f718058a7
--- /dev/null
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AbnormallyTerminatesCond.java
@@ -0,0 +1,59 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package de.uka.ilkd.key.rule.conditions;
+
+import de.uka.ilkd.key.java.Services;
+import de.uka.ilkd.key.java.ast.Statement;
+
+import org.key_project.logic.LogicServices;
+import org.key_project.logic.SyntaxElement;
+import org.key_project.logic.op.sv.SchemaVariable;
+import org.key_project.prover.rules.VariableCondition;
+import org.key_project.prover.rules.instantiation.MatchResultInfo;
+import org.key_project.util.collection.ImmutableArray;
+
+import org.jspecify.annotations.NonNull;
+import org.jspecify.annotations.Nullable;
+
+/// This is a variable condition, that checks if a given variable binds new variables.
+///
+/// @author Alexander Weigl
+/// @version 1 (20.08.26)
+public class AbnormallyTerminatesCond implements VariableCondition {
+    /// Is negated
+    private final boolean negated;
+
+    /// A schema variable representing a Java Expression.
+    private final SchemaVariable svStmts;
+
+    public AbnormallyTerminatesCond(SchemaVariable svStmts, boolean negated) {
+        this.svStmts = svStmts;
+        this.negated = negated;
+    }
+
+    @Override
+    public @Nullable MatchResultInfo check(
+            @Nullable SchemaVariable var, @Nullable SyntaxElement instCandidate,
+            @NonNull MatchResultInfo matchCond, @NonNull LogicServices services) {
+        var svInst = (de.uka.ilkd.key.rule.inst.SVInstantiations) matchCond.getInstantiations();
+        var s = svInst.getInstantiation(svStmts);
+        boolean isAbnormallyTerminating = false;
+
+        var analysis = new AlwaysAbnormallyTerminatingAnalysis(null, (Services) services);
+        if (s instanceof ImmutableArray<?> stmts) {
+
+        } else if (s instanceof Statement stmts) {
+
+        } else {
+            matchCond = null;
+        }
+
+
+        if (negated) {
+            return isAbnormallyTerminating ? null : matchCond;
+        } else {
+            return isAbnormallyTerminating ? matchCond : null;
+        }
+    }
+}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AlwaysAbnormallyTerminatingAnalysis.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AlwaysAbnormallyTerminatingAnalysis.java
new file mode 100644
index 00000000000..da45e54af4f
--- /dev/null
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AlwaysAbnormallyTerminatingAnalysis.java
@@ -0,0 +1,255 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package de.uka.ilkd.key.rule.conditions;
+
+import java.util.HashSet;
+import java.util.LinkedList;
+import java.util.Set;
+
+import de.uka.ilkd.key.java.Services;
+import de.uka.ilkd.key.java.ast.Label;
+import de.uka.ilkd.key.java.ast.Statement;
+import de.uka.ilkd.key.java.ast.StatementBlock;
+import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType;
+import de.uka.ilkd.key.java.ast.expression.Expression;
+import de.uka.ilkd.key.java.ast.expression.literal.BooleanLiteral;
+import de.uka.ilkd.key.java.ast.expression.operator.BinaryOperator;
+import de.uka.ilkd.key.java.ast.expression.operator.BinaryOperatorKind;
+import de.uka.ilkd.key.java.ast.reference.ExecutionContext;
+import de.uka.ilkd.key.java.ast.statement.*;
+
+import org.key_project.util.collection.ImmutableArray;
+
+import org.jspecify.annotations.Nullable;
+
+/// This analysis returns true iff a statement has the possibility to terminate normally
+/// iff not every run terminates abnormally.
+///
+class AlwaysAbnormallyTerminatingAnalysis {
+
+    record TerminationReason(boolean isReturn, Set<KeYJavaType> isThrow, String breakTo,
+            String continueTo) {
+        public TerminationReason(boolean isReturn) {
+            this(isReturn, Set.of(), null, null);
+        }
+
+        public TerminationReason(KeYJavaType keYJavaType) {
+            this(false, Set.of(keYJavaType), null, null);
+        }
+
+        public boolean isAbnormallTerminating() {
+            return isReturn || !isThrow.isEmpty() || breakTo != null && continueTo != null;
+        }
+    }
+
+    private final KeYJavaType assertionException;
+    private final LinkedList<Label> labelStack = new LinkedList<>();
+    private final ExecutionContext ec;
+    private final Services services;
+
+    AlwaysAbnormallyTerminatingAnalysis(ExecutionContext ec, Services services) {
+        this.ec = ec;
+        this.services = services;
+
+        assertionException = services.getJavaInfo().getKeYJavaType("java.lang.AssertionError");
+    }
+
+    public @Nullable TerminationReason abnormallyTerminating(Statement stmt) {
+        return switch (stmt) {
+            case EnhancedFor forStmt -> abnormallyTerminating(forStmt.getBody());
+            case Do doStmt -> abnormallyTerminating(doStmt.getBody());
+            case For forStmt -> abnormallyTerminating(forStmt.getBody());
+            case Switch switchStmt -> {
+                if (hasDefaultBranch(switchStmt)) {
+                    yield allAbnormallyTerminating(switchStmt.getBranchList());
+                }
+                yield null;
+            }
+            case If ifStmt -> //
+                alwaysTrue(ifStmt.getExpression())
+                        ? abnormallyTerminating(ifStmt.getThen())
+                        : alwaysFalse(ifStmt.getExpression())
+                                ? abnormallyTerminating(ifStmt.getElse())
+                                : and(abnormallyTerminating(ifStmt.getThen()),
+                                    abnormallyTerminating(ifStmt.getElse()));
+
+            case Try tStmt -> {
+                var s1 = abnormallyTerminating(tStmt.getBody());
+                var s2 = removeCatchClauses(s1, tStmt.getBranchList());
+                yield isAbnormallTerminating(s2) ? s2 : null;
+            }
+            case While wStmt -> abnormallyTerminating(wStmt.getBody());
+            case Assert aStmt ->
+                alwaysFalse(aStmt.getCondition()) ? new TerminationReason(assertionException)
+                        : null;
+            case StatementBlock b -> abnormallyTerminating(b.getBody());
+            case Continue cStmt ->
+                new TerminationReason(false, Set.of(), null,
+                    cStmt.getLabel() == null ? "" : cStmt.getLabel().toString());
+            case Break bStmt ->
+                new TerminationReason(false, Set.of(),
+                    bStmt.getLabel() == null ? "" : bStmt.getLabel().toString(), null);
+            case Return ret -> new TerminationReason(true);
+            case Throw thr -> {
+                yield new TerminationReason(thr.getExpression().getKeYJavaType(services, ec));
+            }
+            case LabeledStatement ignored1 -> {
+                labelStack.addLast(ignored1.getLabel());
+                var b = abnormallyTerminating(ignored1.getBody());
+                labelStack.removeLast();
+                yield b;
+            }
+            case SynchronizedBlock s -> abnormallyTerminating(s.getBody());
+            case LoopScopeBlock s -> abnormallyTerminating(s.getBody());
+            default -> null;
+        };
+    }
+
+    private boolean hasDefaultBranch(Switch switchStmt) {
+        return switchStmt.getBranchList().stream().anyMatch(it -> it instanceof Default);
+    }
+
+    private TerminationReason removeCatchClauses(@Nullable TerminationReason s1,
+            ImmutableArray<Branch> branchList) {
+        var exc = new HashSet<>(s1 == null ? Set.of() : s1.isThrow);
+        var newExcCatch = new HashSet<KeYJavaType>();
+        final var isReturn = s1 != null && s1.isReturn;
+
+        var catchReturns = true;
+
+        boolean finallyReturn = false;
+        for (var branch : branchList) {
+            if (branch instanceof Catch c) {
+                var t =
+                    (KeYJavaType) c.getParameterDeclaration().getVariableSpecification().getType();
+                exc.remove(t);
+                var q = abnormallyTerminating(c);
+                if (q != null) {
+                    newExcCatch.addAll(q.isThrow);
+                    catchReturns = catchReturns && q.isReturn;
+                } else {
+                    catchReturns = false;
+                }
+            }
+            if (branch instanceof Finally f) {
+                var q = abnormallyTerminating(f);
+                if (q != null) {
+                    newExcCatch.addAll(q.isThrow);
+                    finallyReturn = q.isReturn;
+                } else {
+                    finallyReturn = false;
+                }
+            }
+        }
+
+        exc.addAll(newExcCatch);
+        var ret = finallyReturn || isReturn && (!s1.isThrow().isEmpty() && catchReturns);
+        return new TerminationReason(ret, exc, s1 == null ? null : s1.breakTo,
+            s1 == null ? null : s1.continueTo);
+    }
+
+    private boolean isAbnormallTerminatingOnlyException(TerminationReason s1) {
+        return s1 != null && !s1.isThrow.isEmpty() && s1.isReturn;
+    }
+
+    private boolean isAbnormallTerminating(TerminationReason b) {
+        return b != null && b.isAbnormallTerminating();
+    }
+
+    private @Nullable TerminationReason or(@Nullable TerminationReason a, TerminationReason b) {
+        final var a1 = isAbnormallTerminating(a);
+        final var b1 = isAbnormallTerminating(b);
+        if (a1 && b1) {
+            var s = new HashSet<>(a.isThrow);
+            s.addAll(b.isThrow);
+            return new TerminationReason(a.isReturn || b.isReturn, s, a.breakTo, a.continueTo);
+        } else if (a1) {
+            return a;
+        } else if (b1) {
+            return b;
+        }
+        return null;
+    }
+
+    private @Nullable TerminationReason and(@Nullable TerminationReason a,
+            @Nullable TerminationReason b) {
+        if (a != null && a.isAbnormallTerminating()
+                && b != null && b.isAbnormallTerminating()) {
+            var s = new HashSet<>(a.isThrow);
+            s.addAll(b.isThrow);
+            return new TerminationReason(a.isReturn || b.isReturn, s, a.breakTo, a.continueTo);
+        }
+        return null;
+    }
+
+    private TerminationReason abnormallyTerminatingFinally(ImmutableArray<Branch> branchList) {
+        for (var branch : branchList) {
+            if (branch instanceof Finally) {
+                return abnormallyTerminating(branch);
+            }
+        }
+        return null;
+    }
+
+
+    private boolean alwaysTrue(@Nullable Expression guardExpression) {
+        if (guardExpression == null)
+            return false;
+        if (guardExpression instanceof BooleanLiteral bl) {
+            return bl.getValue();
+        } else if (guardExpression instanceof BinaryOperator bo) {
+            if (bo.getKind() == BinaryOperatorKind.LOGICAL_AND) {
+                return alwaysTrue(bo.getLeft()) && alwaysTrue(bo.getRight());
+            } else if (bo.getKind() == BinaryOperatorKind.LOGICAL_OR) {
+                return alwaysTrue(bo.getLeft()) || alwaysTrue(bo.getRight());
+            }
+        }
+        return false;
+    }
+
+    private boolean alwaysFalse(@Nullable Expression guardExpression) {
+        if (guardExpression == null)
+            return false;
+        if (guardExpression instanceof BooleanLiteral bl) {
+            return !bl.getValue();
+        } else if (guardExpression instanceof BinaryOperator bo) {
+            if (bo.getKind() == BinaryOperatorKind.LOGICAL_AND) {
+                return alwaysFalse(bo.getLeft()) && alwaysFalse(bo.getRight());
+            } else if (bo.getKind() == BinaryOperatorKind.LOGICAL_OR) {
+                return alwaysFalse(bo.getLeft()) || alwaysFalse(bo.getRight());
+            }
+        }
+        return false;
+    }
+
+    private TerminationReason allAbnormallyTerminating(ImmutableArray<Branch> branchList) {
+        return branchList.stream().map(this::abnormallyTerminating)
+                .reduce(this::and).orElse(null);
+    }
+
+    private TerminationReason abnormallyTerminating(ImmutableArray<? extends Statement> body) {
+        for (var statement : body) {
+            final var terminationReason = abnormallyTerminating(statement);
+            if (terminationReason != null && terminationReason.isAbnormallTerminating())
+                return terminationReason;
+        }
+        return null;
+    }
+
+    private @Nullable TerminationReason abnormallyTerminating(@Nullable Branch it) {
+        if (it == null)
+            return null;
+        return switch (it) {
+            case Finally f -> abnormallyTerminating(f.getBody());
+            case Case f -> abnormallyTerminating(f.getBody());
+            case Default f -> abnormallyTerminating(f.getBody());
+            case Ccatch f -> abnormallyTerminating(f.getBody());
+            case Then f -> abnormallyTerminating(f.getBody());
+            case Else f -> abnormallyTerminating(f.getBody());
+            case Catch f -> abnormallyTerminating(f.getBody());
+            default -> null;
+        };
+    }
+
+}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/BindingExpressionCond.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/BindingExpressionCond.java
new file mode 100644
index 00000000000..fd477fb7059
--- /dev/null
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/BindingExpressionCond.java
@@ -0,0 +1,102 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package de.uka.ilkd.key.rule.conditions;
+
+import java.util.Map;
+
+import de.uka.ilkd.key.java.ast.Statement;
+import de.uka.ilkd.key.java.ast.declaration.LocalVariableDeclaration;
+import de.uka.ilkd.key.java.ast.declaration.VariableSpecification;
+import de.uka.ilkd.key.java.ast.expression.Expression;
+import de.uka.ilkd.key.java.ast.reference.TypeRef;
+import de.uka.ilkd.key.java.visitor.BindingVariableVisitor;
+import de.uka.ilkd.key.logic.op.LocationVariable;
+
+import org.key_project.logic.LogicServices;
+import org.key_project.logic.SyntaxElement;
+import org.key_project.logic.op.sv.SchemaVariable;
+import org.key_project.prover.rules.VariableCondition;
+import org.key_project.prover.rules.instantiation.MatchResultInfo;
+import org.key_project.util.collection.ImmutableArray;
+
+import org.jspecify.annotations.NonNull;
+import org.jspecify.annotations.Nullable;
+
+/// This is a variable condition, that checks if a given variable binds new variables.
+///
+/// @author Alexander Weigl
+/// @version 1 (20.08.26)
+public class BindingExpressionCond implements VariableCondition {
+    /// Is negated
+    private final boolean negated;
+
+    /// A schema variable representing a Java Expression.
+    private final SchemaVariable svExpr;
+    /// A schema variable representing a program that binds variable under positive polarity of
+    /// `svExpr`
+    private final @Nullable SchemaVariable svPosBinding;
+    /// Will store the update `{...||i := i_before||...}`.
+    private final @Nullable SchemaVariable svNegBinding;
+
+    public BindingExpressionCond(SchemaVariable svExpr, boolean negated) {
+        this(svExpr, null, null, negated);
+    }
+
+    public BindingExpressionCond(SchemaVariable svExpr, @Nullable SchemaVariable svPosBinding,
+            @Nullable SchemaVariable svNegBinding,
+            boolean negated) {
+        this.svExpr = svExpr;
+        this.svPosBinding = svPosBinding;
+        this.svNegBinding = svNegBinding;
+        this.negated = negated;
+    }
+
+    @Override
+    public @Nullable MatchResultInfo check(
+            @Nullable SchemaVariable var, @Nullable SyntaxElement instCandidate,
+            @NonNull MatchResultInfo matchCond, @NonNull LogicServices services) {
+        var newMatchCondition = matchCond;
+        var svInst = (de.uka.ilkd.key.rule.inst.SVInstantiations) matchCond.getInstantiations();
+        var condition = svInst.getInstantiation(svExpr);
+
+        boolean isBindingExpr = false;
+
+        if (condition instanceof Expression e) {
+            var v = BindingVariableVisitor.analyze(e);
+            isBindingExpr = !(v.whenFalse().isEmpty() && v.whenTrue().isEmpty());
+            // b ? v.whenTrue() : v.whenFalse()
+
+            if (isBindingExpr && svPosBinding != null && svNegBinding != null) {
+                svInst = svInst
+                        .add(svPosBinding, createBinders(v.whenTrue()), Statement.class, services)
+                        .add(svNegBinding, createBinders(v.whenFalse()), Statement.class, services);
+                newMatchCondition = newMatchCondition.setInstantiations(svInst);
+            }
+        } else {
+            newMatchCondition = null;
+        }
+
+
+        if (negated) {
+            return isBindingExpr ? null : newMatchCondition;
+        } else {
+            return isBindingExpr ? newMatchCondition : null;
+        }
+    }
+
+    private ImmutableArray<Statement> createBinders(Map<LocationVariable, Expression> variables) {
+
+        var seq = variables.entrySet().stream().map(
+            it -> {
+                final var key = it.getKey();
+                final var value = it.getValue();
+                return new LocalVariableDeclaration(
+                    new TypeRef(key.getKeYJavaType()),
+                    new VariableSpecification(key, value, key.getKeYJavaType()));
+            })
+                .toArray(Statement[]::new);
+        return new ImmutableArray<>(seq);
+        // return new StatementBlock(new ImmutableArray<>(seq));
+    }
+}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java
index 16748c266ee..f92055c6780 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java
@@ -15,7 +15,9 @@
 import de.uka.ilkd.key.java.ast.declaration.ModifierKind;
 import de.uka.ilkd.key.java.ast.declaration.ParameterDeclaration;
 import de.uka.ilkd.key.java.ast.declaration.VariableSpecification;
+import de.uka.ilkd.key.java.ast.expression.Expression;
 import de.uka.ilkd.key.java.ast.statement.*;
+import de.uka.ilkd.key.java.visitor.BindingVariableVisitor;
 import de.uka.ilkd.key.ldt.HeapLDT;
 import de.uka.ilkd.key.ldt.HeapLDT.SplitFieldName;
 import de.uka.ilkd.key.ldt.JavaDLTheory;
@@ -1697,6 +1699,34 @@ private ImmutableList<LocationVariable> collectLocalVariablesVisibleTo(Statement
                     result = result.prepend(visibleLocalVariables);
                     return result;
                 }
+            } else if (s instanceof If ifStmt) {
+                final int branchCount = ifStmt.getBranchCount();
+                final var condition = ifStmt.getExpression();
+                if (branchCount == 1) {
+                    var thenBranch = ifStmt.getBranchAt(0);
+                    final ImmutableList<LocationVariable> visibleLocalVariables =
+                        collectLocalVariablesVisibleTo(statement, thenBranch);
+                    if (visibleLocalVariables != null) {
+                        result = result.prepend(visibleLocalVariables);
+                        ImmutableList<LocationVariable> pattern =
+                            collectPatternVariables(true, condition);
+                        result = result.prepend(pattern);
+                        return result;
+                    }
+                }
+
+                if (branchCount == 2) { // also consider else-branch
+                    var elseBranch = ifStmt.getBranchAt(1);
+                    final ImmutableList<LocationVariable> visibleLocalVariables =
+                        collectLocalVariablesVisibleTo(statement, elseBranch);
+                    if (visibleLocalVariables != null) {
+                        result = result.prepend(visibleLocalVariables);
+                        ImmutableList<LocationVariable> pattern =
+                            collectPatternVariables(false, condition);
+                        result = result.prepend(pattern);
+                        return result;
+                    }
+                }
             } else if (s instanceof BranchStatement branch) {
                 final int branchCount = branch.getBranchCount();
                 for (int j = 0; j < branchCount; j++) {
@@ -1874,7 +1904,7 @@ public LoopSpecification createJMLLoopInvariant(IProgramMethod pm, LoopStatement
     public FunctionalOperationContract initiallyClauseToContract(InitiallyClause ini,
             IProgramMethod pm) throws SLTranslationException {
         final ImmutableList<JMLModifier> modifiers =
-            ImmutableList.<JMLModifier>singleton(JMLModifier.PRIVATE);
+            ImmutableList.singleton(JMLModifier.PRIVATE);
         final TextualJMLSpecCase specCase = new TextualJMLSpecCase(modifiers, Behavior.NONE);
         specCase.addName(ini.getName());
         for (LabeledParserRuleContext context : createPrecond(pm, ini.getOriginalSpec())) {
@@ -1917,4 +1947,12 @@ private ImmutableList<LabeledParserRuleContext> createPrecond(IProgramMethod pm,
         }
         return res;
     }
+
+
+    private ImmutableList<LocationVariable> collectPatternVariables(boolean b,
+            Expression condition) {
+        var v = BindingVariableVisitor.analyze(condition);
+        return ImmutableList.fromList(b ? v.whenTrue().keySet() : v.whenFalse().keySet());
+    }
+
 }
diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/java5.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/java5.key
index 31f6af27de6..40832a239da 100644
--- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/java5.key
+++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/java5.key
@@ -13,7 +13,7 @@
     \program SimpleExpression #se;
     \program NonSimpleExpression #nse;
     \program Expression #e;
-    \program Variable #v0;
+    \program Variable #v0, #fresh;
     \program Variable #id;
     \program Variable #a;
     \program Statement #stm;
@@ -26,6 +26,8 @@
     \formula post, inv;
 
     \term E e;
+
+    \program [list] Statement #then, #else;
 }
 
 /***
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 1c29b1ee2cd..10a38e4384f 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
@@ -36,7 +36,7 @@
     \program Variable #v, #v0, #v1, #v2, #boolv, #a, #a0, #a1;
 
     \program ConstantPrimitiveTypeVariable #cv; // variables that are compile-time constants
-    \program Variable #b0, #ar1;
+    \program Variable #b0, #ar1, #id;
     \program VariableInitializer #vi;
     \program SimpleJavaBooleanExpression #seBool, #seBool0, #seBool1, #seBool2;
     \program JavaBooleanExpression #exBool, #exBool0, #exBool1, #exBool2;
@@ -53,7 +53,7 @@
 
     \program ClassReference #cr;
 
-    \program [list] Statement #slist, #slist1, #slist2, #slist3;
+    \program [list] Statement #slist, #slist1, #slist2, #slist3, #posBinding, #negBinding;
     \program [list] Expression #elist;
     \program [list] SimpleExpression #selist;
     \program [list] Catch #cs;
@@ -1274,6 +1274,69 @@
         \displayname "ifElseUnfold"
     };
 
+    // --- instanceof pattern matching binding (Java 16+) ----------------------
+		// These rules handle the variable binding semantics of pattern matching instanceof
+    // Syntax: if(expr instanceof Type varName) { /* varName is bound to expr */ }
+
+		ifUnfoldPattern {
+			\find(\modality{#allmodal}{.. if( #nse ) {#slist} ...}\endmodality (post))
+      \varcond(\new(#boolv, boolean))
+      \varcond(\isBindingExpr(#nse, #posBinding, #negBinding))
+      \replacewith(
+        \modality{#allmodal}{..
+          boolean #boolv;
+          { #boolv = #nse; }
+          if(#boolv) {
+            #posBinding;
+            #slist
+          }
+        ...}\endmodality (post))
+
+      \heuristics(simplify_autoname)
+      \displayname "ifElseUnfoldPattern"
+    };
+
+		ifUnfoldPatternUnreachable {
+			\find(\modality{#allmodal}{.. if( #nse ) {#slist} ...}\endmodality (post))
+      \varcond(\new(#boolv, boolean))
+      \varcond(\isBindingExpr(#nse, #posBinding, #negBinding))
+      \varcond(\alwaysAbnormallyTerminates(#slist))
+      \replacewith(
+        \modality{#allmodal}{..
+          boolean #boolv;
+          { #boolv = #nse; }
+          if(#boolv) {
+            #posBinding;
+            #slist
+          }
+          #negBinding
+        ...}\endmodality (post))
+
+      \heuristics(simplify_autoname)
+      \displayname "ifElseUnfoldPatternUnrechable"
+    };
+
+    ifElseUnfoldPattern {
+				\find(\modality{#allmodal}{.. if( #nse ) {#slist} else { #slist1 } ...}\endmodality (post))
+	      \varcond(\new(#boolv, boolean))
+	      \varcond(\isBindingExpr(#nse, #posBinding, #negBinding))
+				\replacewith(
+		      \modality{#allmodal}{..
+		        boolean #boolv;
+            { #boolv = #nse; }
+		        if(#boolv) {
+		          #posBinding;
+		          #slist
+		        } else {
+		          #negBinding;
+		          #slist1
+		        }
+		      ...}\endmodality (post))
+
+        \heuristics(simplify_autoname)
+        \displayname "ifElseUnfoldPattern"
+    };
+
     ifElseUnfold {
         \find(\modality{#allmodal}{.. if(#nse) #s0 else #s1 ...}\endmodality (post))
         \varcond(\new(#boolv, boolean))
@@ -1528,6 +1591,17 @@
     // -----------                  instanceof                -----------
     // ----------------------------------------------------------------------------
 
+		instanceof_eval_id {
+        \find(\modality{#allmodal}{.. #v = #nse instanceof #t #id; ...}\endmodality (post))
+        \varcond(\newTypeOf(#v0, #nse))
+        \replacewith(\modality{#allmodal}{..
+	            #typeof(#nse) #v0=#nse;
+	            #v=#v0 instanceof #t;
+	            #t #id = (#t) #v;
+            ...}\endmodality (post))
+        \heuristics(simplify_autoname)
+    };
+
     instanceof_eval {
         \find(\modality{#allmodal}{.. #v = #nse instanceof #t; ...}\endmodality (post))
         \varcond(\newTypeOf(#v0, #nse))
diff --git a/key.core/src/test/java/de/uka/ilkd/key/rule/conditions/AlwaysAbnormallyTerminatingAnalysisTest.java b/key.core/src/test/java/de/uka/ilkd/key/rule/conditions/AlwaysAbnormallyTerminatingAnalysisTest.java
new file mode 100644
index 00000000000..58b2ab8959d
--- /dev/null
+++ b/key.core/src/test/java/de/uka/ilkd/key/rule/conditions/AlwaysAbnormallyTerminatingAnalysisTest.java
@@ -0,0 +1,127 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package de.uka.ilkd.key.rule.conditions;
+
+import de.uka.ilkd.key.java.Services;
+import de.uka.ilkd.key.java.ast.JPContext;
+import de.uka.ilkd.key.java.ast.Statement;
+import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType;
+import de.uka.ilkd.key.java.ast.abstraction.PrimitiveType;
+import de.uka.ilkd.key.java.ast.reference.ExecutionContext;
+import de.uka.ilkd.key.java.ast.reference.TypeRef;
+import de.uka.ilkd.key.java.loader.JP2KeYConverter;
+import de.uka.ilkd.key.logic.ProgramElementName;
+import de.uka.ilkd.key.logic.op.LocationVariable;
+import de.uka.ilkd.key.logic.op.SchemaVariableFactory;
+import de.uka.ilkd.key.logic.sort.ProgramSVSort;
+import de.uka.ilkd.key.logic.sort.SortImpl;
+import de.uka.ilkd.key.nparser.NamespaceBuilder;
+import de.uka.ilkd.key.proof.init.JavaProfile;
+
+import org.key_project.logic.Name;
+import org.key_project.logic.Namespace;
+import org.key_project.logic.op.sv.SchemaVariable;
+
+import com.github.javaparser.JavaParser;
+import com.github.javaparser.StaticJavaParser;
+import com.github.javaparser.ast.body.ClassOrInterfaceDeclaration;
+import org.junit.jupiter.api.TestInstance;
+import org.junit.jupiter.params.ParameterizedTest;
+import org.junit.jupiter.params.provider.CsvSource;
+
+import static org.junit.jupiter.api.Assertions.assertEquals;
+
+/**
+ * NOTE ON PACKAGE PLACEMENT: put this file in the same package as
+ * AlwaysAbnormallyTerminatingAnalysis (it relies on package-private / private
+ * access to the record and to the and()/or() helpers via reflection, so it
+ * doesn't need any source changes to the class under test).
+ * <p>
+ * NOTE ON TIER B (statement-level tests): those need a real Services +
+ * parsed Statement, which is project-specific plumbing I don't have visibility
+ * into. `parseStatement(String)` below is a stub — wire it up to however your
+ * test suite already builds a Services/ExecutionContext and parses a method
+ * body (KeY 3.x parses via JavaParser under the hood). Everything else in
+ * this file works standalone.
+ */
+@TestInstance(TestInstance.Lifecycle.PER_CLASS)
+class AlwaysAbnormallyTerminatingAnalysisTest {
+    private final Services services = new Services(JavaProfile.getDefaultProfile());
+    private final JPContext context;
+    private final JP2KeYConverter converter;
+    private final JavaParser javaParser;
+    private final ExecutionContext executionContext;
+
+
+    // --- plumbing you need to fill in for your project -----------------
+
+    private AlwaysAbnormallyTerminatingAnalysis newAnalysis() {
+        return new AlwaysAbnormallyTerminatingAnalysis(executionContext, services);
+    }
+
+    private Statement parseStatement(String javaStatementSource) {
+        return (Statement) services.getJavaService()
+                .readBlock("{" + javaStatementSource + "}", context, null).program();
+    }
+
+    public AlwaysAbnormallyTerminatingAnalysisTest() {
+        System.out.println("TEST INIT");
+        var nss = services.getNamespaces();
+        NamespaceBuilder nb = new NamespaceBuilder(nss);
+        nb.addSort("boolean").addSort("int").addSort("Seq").addSort("LocSet").addSort("double")
+                .addSort("float");
+
+        Namespace<SchemaVariable> nsSchema = new Namespace<>();
+        nsSchema.add(SchemaVariableFactory.createProgramSV(
+            new ProgramElementName("#a"), ProgramSVSort.EXPRESSION, false));
+        nsSchema.add(SchemaVariableFactory.createProgramSV(
+            new ProgramElementName("#b"), ProgramSVSort.EXPRESSION, false));
+        nsSchema.add(SchemaVariableFactory.createProgramSV(
+            new ProgramElementName("#c"), ProgramSVSort.EXPRESSION, false));
+
+        services.activateJava(null);
+
+
+        var cu = StaticJavaParser.parse("""
+                public class Context {
+                    boolean x, y, z;
+                }
+                """);
+        services.getJavaService().getSymbolResolver().inject(cu);
+        context = new JPContext((ClassOrInterfaceDeclaration) cu.types().getFirst(), cu);
+        services.getJavaService().parseSpecialClasses();
+        converter = services.getJavaService().getConverter(nsSchema);
+        javaParser = services.getJavaService().getProgramFactory().createJavaParser();
+
+        executionContext = new ExecutionContext(
+            new TypeRef(new KeYJavaType(PrimitiveType.JAVA_BYTE, new SortImpl(new Name("byte")))),
+            null, new LocationVariable(new ProgramElementName("testVar"),
+                new SortImpl(new Name("testSort"))));
+    }
+
+    @ParameterizedTest(name = "[{index}] {1}")
+    @CsvSource(delimiterString = "|", value = {
+        // expectedAlwaysAbnormal | description | source
+        "true  | if/else both return                   | if (x) { return 1; } else { return 2; }",
+        "true | if/else only then returns              | if (true) { return 1; } else { doStuff(); }",
+        "false | if/else only then returns             | if (x) { return 1; } else { doStuff(); }",
+        "false | if with no else                       | if (x) { return 1; }",
+        "true | while(true) with a break              | while (true) { if (x) { break; } return 1; }",
+        "false | while(true) with no break at all      | while (true) { doStuff(); }",
+        "false | switch without default                | switch (x) { case 1: return 1; }",
+        "true  | switch with default, all cases return | switch (x) { case 1: return 1; default: throw new RuntimeException(); }",
+        "false | try/catch that recovers                  | try { throw new RuntimeException(); } catch (RuntimeException e) { doStuff(); }",
+        "true  | try/finally where finally always returns | try { doStuff(); } finally { return 1; }",
+        "true  | assert with a constant-false condition   | assert false;",
+        "false | assert with a constant-true condition    | assert true;",
+    })
+    void statementAlwaysAbnormal(boolean expected, String description, String source) {
+        Statement stmt = parseStatement(source);
+        AlwaysAbnormallyTerminatingAnalysis analysis = newAnalysis();
+        Object result = analysis.abnormallyTerminating(stmt);
+        boolean actual = result != null; // TerminationReason#isAbnormallTerminating() should also
+                                         // be checked once record fields are trustworthy
+        assertEquals(expected, actual, description);
+    }
+}
diff --git a/key.ui/examples/Java/InstanceOfPattern/README.txt b/key.ui/examples/Java/InstanceOfPattern/README.txt
new file mode 100644
index 00000000000..38f279cae75
--- /dev/null
+++ b/key.ui/examples/Java/InstanceOfPattern/README.txt
@@ -0,0 +1,72 @@
+example.name = Binding InstanceOf
+example.path = Java 25
+example.file = project.key
+example.additionalFile.1 = src/InstanceOfPatternExample.java
+
+
+Java 16+ Instanceof Pattern Matching Example
+=============================================
+
+This example demonstrates KeY's support for Java 16+ instanceof pattern matching,
+which allows type checking and variable binding in a single expression.
+
+Feature Overview
+----------------
+Traditional instanceof (pre-Java 16):
+    if (obj instanceof String) {
+        String s = (String) obj;
+        return s.length();
+    }
+
+Pattern matching instanceof (Java 16+):
+    if (obj instanceof String s) {
+        // 's' is automatically bound as a String
+        return s.length();
+    }
+
+What This Example Shows
+-----------------------
+1. Basic pattern matching (getStringLength method)
+   - The pattern variable 's' is bound in the true branch
+   
+2. Negated instanceof (checkNotString method)
+   - Pattern binding happens in the else branch, not the if branch
+   - Demonstrates: if(!(x instanceof T e)) { ... } else { ... }
+   
+3. Multiple instanceof patterns (processNumber method)
+   - Chained instanceof checks with different types
+   
+4. Pattern variables in complex expressions (compareIfBothStrings)
+   - Multiple pattern variables bound in the same branch
+   - Combined with && operator
+   
+5. Traditional vs pattern matching comparison (traditionalVsPattern)
+   - Shows both styles work correctly together
+
+Key Taclets
+-----------
+The following taclets in genericRules.key handle pattern matching:
+
+- instanceof_pattern_if_split: Splits if-statements and binds the pattern variable
+- instanceof_pattern_negated_if: Handles negated instanceof by swapping branches  
+- instanceof_pattern_cast_elimination: Eliminates redundant casts after instanceof
+
+Loading This Example
+--------------------
+1. Open KeY
+2. Load the project.key file from this directory
+3. Select a method to verify
+4. Start symbolic execution
+
+The instanceof pattern matching will be automatically handled during proof search.
+
+Requirements
+------------
+- Java 16 or later (for compilation)
+- KeY with instanceof pattern matching support
+
+See Also
+--------
+- Java 16 Release Notes: https://openjdk.java.net/projects/jdk/16/
+- JEP 394: Pattern Matching for instanceof
+  https://openjdk.java.net/jeps/394
diff --git a/key.ui/examples/Java/InstanceOfPattern/project.key b/key.ui/examples/Java/InstanceOfPattern/project.key
new file mode 100644
index 00000000000..e55dd42651e
--- /dev/null
+++ b/key.ui/examples/Java/InstanceOfPattern/project.key
@@ -0,0 +1,3 @@
+\javaSource "src";
+
+\chooseContract
diff --git a/key.ui/examples/Java/InstanceOfPattern/src/InstanceOfPatternExample.java b/key.ui/examples/Java/InstanceOfPattern/src/InstanceOfPatternExample.java
new file mode 100644
index 00000000000..c7d5282d439
--- /dev/null
+++ b/key.ui/examples/Java/InstanceOfPattern/src/InstanceOfPatternExample.java
@@ -0,0 +1,149 @@
+/**
+ * Example demonstrating Java 16+ instanceof pattern matching support in KeY.
+ * 
+ * This feature allows you to write:
+ *   if (obj instanceof String s) {
+ *       // s is automatically bound and can be used here
+ *       return s.length();
+ *   }
+ * 
+ * Instead of the traditional:
+ *   if (obj instanceof String) {
+ *       String s = (String) obj;
+ *       return s.length();
+ *   }
+ */
+public class InstanceOfPatternExample {
+    
+    /**
+     * Basic instanceof pattern matching example.
+     * The variable 's' is bound in the true branch of the instanceof check.
+     */
+    /*@ normal_behavior
+      @ requires obj != null;
+      @ ensures \result >= 0;
+      @*/
+    public static int getStringLength(Object obj) {
+        if (obj instanceof String s) {
+            // Pattern variable 's' is bound and has type String here
+            // @ assert s != null;
+            return s.length();
+        }
+        return -1;
+    }
+    
+    /**
+     * Negated instanceof pattern - note that the binding only happens
+     * in the else branch, not the if branch.
+     */
+    /*@ normal_behavior
+      @ requires true;
+      @ ensures \result >= 0;
+      @*/
+    public static int checkNotString(Object obj) {
+        Object a = new Object();
+        //@ assert a != null;
+        if (!(obj instanceof String s)) {
+            // 's' is NOT bound here
+            return 0;
+        } else {
+            // 's' IS bound here (in the else branch)
+            // @ assert s != null;
+            return s.length();
+        }
+    }
+    
+    /**
+     * Multiple instanceof patterns in sequence.
+     */
+    /*@ normal_behavior
+      @ requires true;
+      @ ensures \result >= 0;
+      @*/
+    public static int processNumber(Object obj) {
+        if (obj instanceof Integer i) {
+            return i.intValue();
+        } else if (obj instanceof Double d) {
+            return d.intValue();
+        } else if (obj instanceof Long l) {
+            return l.intValue();
+        }
+        return -1;
+    }
+    
+    /**
+     * Pattern matching with method calls.
+     */
+    /*@ normal_behavior
+      @ requires true;
+      @ ensures \result >= -1;
+      @*/
+    public static int getToStringLength(Object obj) {
+        if (obj instanceof String s) {
+            // Can call methods on the pattern variable
+            return s.toString().length();
+        }
+        return -1;
+    }
+    
+//    /**
+//     * Pattern matching in complex expressions.
+//     */
+//    /*@ normal_behavior
+//      @ requires obj1 != null && obj2 != null;
+//      @ ensures \result == 0 || \result > 0;
+//      @*/
+//    public static int compareIfBothStrings(Object obj1, Object obj2) {
+//        if (obj1 instanceof String s1 && obj2 instanceof String s2) {
+//            // Both s1 and s2 are bound in this branch
+//            //@ assert s1 != null && s2 != null;
+//            return s1.compareTo(s2);
+//        }
+//        return 0;
+//    }
+    
+    /**
+     * Traditional instanceof vs pattern matching.
+     * This shows both styles for comparison.
+     */
+    /*@ normal_behavior
+      @ requires true;
+      @ ensures \result >= -1;
+      @*/
+    public static int traditionalVsPattern(Object obj) {
+        // Traditional style (still supported)
+        if (obj instanceof String) {
+            String s = (String) obj;
+            int traditional = s.length();
+            
+            // Pattern matching style (more concise)
+            if (obj instanceof String pattern) {
+                int patternStyle = pattern.length();
+                //@ assert traditional == patternStyle;
+            }
+            
+            return traditional;
+        }
+        return -1;
+    }
+    
+    /**
+     * Main method for testing.
+     */
+    public static void main(String[] args) {
+        System.out.println(getStringLength("Hello"));  // 5
+        System.out.println(getStringLength(42));       // -1
+        
+        System.out.println(checkNotString(42));        // 0
+        System.out.println(checkNotString("World"));   // 5
+        
+        System.out.println(processNumber(42));         // 42
+        System.out.println(processNumber(3.14));       // 3
+        System.out.println(processNumber(100L));       // 100
+        
+        System.out.println(getToStringLength("Test")); // 4
+        
+        System.out.println(compareIfBothStrings("A", "B")); // -1
+        System.out.println(compareIfBothStrings("A", 42));  // 0
+    }
+}
diff --git a/key.ui/examples/index/samplesIndex.txt b/key.ui/examples/index/samplesIndex.txt
index 666003ded24..f38d3278d8c 100644
--- a/key.ui/examples/index/samplesIndex.txt
+++ b/key.ui/examples/index/samplesIndex.txt
@@ -30,6 +30,7 @@ Java/Records/README.txt
 Java/Records+CompactConstructor/README.txt
 Java/TextBlockLiterals/README.txt
 Java/TryWithResources/README.txt
+Java/InstanceOfPattern/README.txt
 
 # The KeY Book (note: the comments here are only for maintainability, if you want to move an entry to a different section, look into the individual txt file!)
 ## Chapter 15 - Using the KeY Prover

From e9f69988dcdf69722eb50e0bee6a88995949c78e Mon Sep 17 00:00:00 2001
From: Alexander Weigl <weigl@kit.edu>
Date: Thu, 20 Aug 2026 05:37:15 +0200
Subject: [PATCH 2/4] add a first matching debugging tool

---
 AGENT.md                                      | 217 +++++++++++++++
 .../key/rule/match/vm/VMTacletMatcher.java    | 120 +++++++-
 .../impl/TacletMatchDebuggerExtension.java    | 262 ++++++++++++++++++
 ...ilkd.key.gui.extension.api.KeYGuiExtension |   3 +-
 4 files changed, 599 insertions(+), 3 deletions(-)
 create mode 100644 AGENT.md
 create mode 100644 key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/TacletMatchDebuggerExtension.java

diff --git a/AGENT.md b/AGENT.md
new file mode 100644
index 00000000000..f1065315eea
--- /dev/null
+++ b/AGENT.md
@@ -0,0 +1,217 @@
+# Agent Guidelines for KeY Project
+
+This document provides guidelines and rules for AI agents working on the KeY deductive Java program verifier project.
+
+## Project Overview
+
+**KeY** is an interactive theorem prover for formal verification and analysis of Java programs. It supports:
+- Formal verification of Java programs with Java Modeling Language specifications
+- Symbolic program execution
+- First-order reasoning
+- Test case generation
+
+**License**: GPL v2 (all contributions must be compatible)
+
+## Technical Stack
+
+### Build System
+- **Gradle** with Groovy DSL (`build.gradle`)
+- Multi-module project structure
+- Java 21 compatibility required
+
+```bash
+# Common build commands
+./gradlew classes                   # Compile all classes
+./gradlew testClasses               # Compile all test classes
+./gradlew test                      # Run full test suite (hours)
+./gradlew testFast                  # Run lightweight tests (minutes)
+./gradlew spotlessApply             # Reformat source code
+./gradlew :key.<subproject>:test --tests "<class>.<method>"  # Specific test
+./gradlew :key.ui:run               # Run KeY UI
+./gradlew :key.ui:run --args='--experimental'  # With experimental features
+./gradlew :key.ui:shadowJar         # Create fat jar
+```
+
+### Key Technologies
+- **Java 21** (source/target compatibility)
+- **JUnit 6** (Jupiter) for testing
+- **AssertJ** for assertions
+- **SLF4J** with Logback for logging
+- **Spotless** for code formatting
+- **ANTLR 4** for parser generation
+
+### Dependencies Management
+- Version Catalog (`libs.*` notation in build files)
+- All dependencies must be on Maven Central repository
+- Use JSpecify for nullability annotations
+
+## Project Structure
+
+### Core Modules
+```
+key.util          - Base utilities
+key.core          - Core verification engine
+key.ui            - GUI application
+key.ncore         - Logic layer
+key.ncore.*       - Calculus layers
+```
+Extension Modules are marked by name `keyext.*`
+
+### Module Naming Convention
+- Base components: `key.*`
+- Extensions/plugins: `keyext.*`
+- Follow Maven standard directory layout
+
+## Coding Conventions
+
+### Java Code Style
+- Follow [Java Code Conventions](https://keyproject.github.io/key-docs/devel/CodingConventions/)
+- Use Spotless plugin for automatic formatting
+- Indentation: 4 spaces (no tabs)
+- Line length: Reasonable limits (typically 120 chars)
+- Braces: Always use braces for control structures
+
+### Package Structure
+- Root packages: `de.uka.ilkd.key.*`, `org.key_project.*`
+- Keep related classes in same package
+- Avoid circular dependencies between modules
+
+### Documentation
+- JavaDoc for public APIs
+- Inline comments for complex logic
+- Reference official docs: https://keyproject.github.io/key-docs/devel/
+
+## Testing Guidelines
+
+### Test Organization
+- Tests in `src/test/java` mirroring source structure
+- Test fixtures in `src/testFixtures/java`
+- Use JUnit 5 Jupiter API
+- Prefer AssertJ for fluent assertions
+
+### Writing Tests
+```java
+// Example pattern
+@Test
+void shouldVerifyExpectedBehavior() {
+    // Given
+    // When  
+    // Then - use AssertJ
+    assertThat(result).isEqualTo(expected);
+}
+```
+
+### Running Tests
+- Use `testFast` for quick feedback during development
+- Use `test` before committing (comprehensive but slow)
+- Debug with: `./gradlew test --debug-jvm` (attach at localhost:5005)
+
+## Quality Assurance
+
+### Automated Checks
+All PRs are automatically checked via GitHub Actions:
+- Unit tests execution
+- Code formatting (Spotless)
+- Static analysis (Checker Framework, SonarQube)
+- License compliance
+
+### Pre-commit Checklist
+1. Code compiles: `./gradlew classes`
+2. Tests pass: `./gradlew testFast`
+3. Reformatting: `./gradlew spotlessApply`
+4. No new warnings introduced
+5. GPL v2 license compatibility verified
+
+## Development Workflow
+
+### Branch Strategy
+- Feature branches from main
+- Descriptive branch names (e.g., `lastname/xxx`, `feature/xxx`, `fix/yyy`)
+- Releases are in `releases/` and pre-releases in `prerelease/`
+- Rebase before merging to keep history clean
+
+### Commit Messages
+- Clear, descriptive messages
+- Reference issues when applicable
+- Follow conventional commits pattern
+
+### Pull Requests
+1. Fork and create feature branch
+2. Implement changes with tests
+3. Ensure all CI checks pass
+4. Open PR with clear description
+5. Address review feedback
+6. Squash/rebase as requested
+
+## Architecture Principles
+
+### Core Design
+- Separation of concerns between layers
+- Immutable data structures where possible
+- Thread-safety considerations documented
+- Performance-critical code profiled
+
+### Key Components
+- **Proof Engine**: Sequent calculus-based theorem proving
+- **SMT Integration**: Z3, cvc5, Princess solvers
+- **GUI**: Java Swing with FlatLaf look-and-feel
+
+## Tools & Resources
+
+### Essential Links
+- Homepage: https://key-project.org
+- Developer Docs: https://keyproject.github.io/key-docs/devel/
+- Issue Tracker: https://github.com/KeYProject/key/issues
+- Mailing List: key-all@lists.informatik.kit.edu
+
+### IDE Setup
+- IntelliJ IDEA recommended (project includes `.idea` configs)
+- Eclipse supported via gradle eclipse plugin
+- Enable annotation processing for Checker Framework
+
+## Agent-Specific Rules
+
+### When Making Changes
+1. **Understand context first**: Read existing code, tests, and documentation
+2. **Follow patterns**: Match existing code style and architecture
+3. **Test incrementally**: Verify each change compiles and tests pass
+4. **Document decisions**: Add comments explaining non-obvious choices
+5. **Respect licensing**: All code must be GPL v2 compatible
+
+### Communication
+- Be explicit about assumptions and limitations
+- Provide complete, functional code (no placeholders)
+- Include usage examples when adding new features
+- Reference relevant documentation or prior art
+
+### Code Review Expectations
+- Manual review by core team required
+- Automated checks must pass first
+- Be prepared to iterate based on feedback
+- Maintain backward compatibility when possible
+
+## Common Tasks Reference
+
+### Adding a New Module
+1. Create directory following pattern: `key.module.name/`
+2. Add to `settings.gradle`
+3. Configure `build.gradle` with dependencies
+4. Apply standard plugins (java, spotless, checkerframework)
+
+### Modifying Build Configuration
+1. Edit root `build.gradle` for global changes
+2. Edit subproject `build.gradle` for module-specific changes
+3. Update version catalog if adding dependencies
+4. Test build locally before committing
+
+### Debugging Issues
+1. Check existing issues/PRs for similar problems
+2. Enable debug logging
+3. Use debugger attachment (localhost:5005)
+4. Consult developer documentation
+5. Ask on mailing list if stuck
+
+---
+
+*Last updated: August 2026*
+*For questions, refer to the [KeY Developer Documentation](https://keyproject.github.io/key-docs/devel/)*
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/VMTacletMatcher.java b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/VMTacletMatcher.java
index a0a1afb91ed..3f9655f26da 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/VMTacletMatcher.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/VMTacletMatcher.java
@@ -3,6 +3,7 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.rule.match.vm;
 
+import java.io.PrintWriter;
 import java.util.HashMap;
 import java.util.Iterator;
 
@@ -108,10 +109,22 @@ public class VMTacletMatcher implements TacletMatcher {
      */
     private final JTerm findExp;
 
+    /**
+     * optional sink for human readable explanations of the matching decisions taken by this
+     * matcher; {@code null} disables logging entirely, in which case {@link #logDecision} is a
+     * no-op.
+     */
+    private final @Nullable PrintWriter out;
+
     /**
      * @param taclet the Taclet matched by this matcher
      */
     public VMTacletMatcher(Taclet taclet) {
+        this(taclet, null);
+    }
+
+    public VMTacletMatcher(Taclet taclet, @Nullable PrintWriter out) {
+        this.out = out;
         varconditions = taclet.getVariableConditions();
         assumesSequent = taclet.assumesSequent();
         boundVars = taclet.getBoundVariables();
@@ -122,25 +135,46 @@ public VMTacletMatcher(Taclet taclet) {
         // interpreter is used only when explicitly selected (property) or as the automatic
         // fallback for a pattern the compiler does not handle
         final boolean useInterpreter = Boolean.getBoolean(INTERPRETER_MATCHER_PROPERTY);
+        logDecision(
+            "Building matcher for taclet '%s' using the %s back-end (system property %s=%s).",
+            taclet.name(), useInterpreter ? "interpreter" : "compiled",
+            INTERPRETER_MATCHER_PROPERTY, useInterpreter);
 
         if (taclet instanceof final FindTaclet findTaclet) {
             findExp = findTaclet.find();
             ignoreTopLevelUpdates = taclet.ignoreTopLevelUpdates()
                     && !(findExp.op() instanceof UpdateApplication);
             findMatchProgram = matchProgramFor(findExp, useInterpreter);
+            logDecision(
+                "Taclet '%s' is a find taclet with find expression '%s'; top-level updates %s ignored.",
+                taclet.name(), findExp, ignoreTopLevelUpdates ? "will be" : "will not be");
         } else {
             ignoreTopLevelUpdates = false;
             findExp = null;
             findMatchProgram = null;
+            logDecision("Taclet '%s' has no \\find expression; no find matcher is built.",
+                taclet.name());
         }
 
         // The taclet's \assumes formulas use the same back-end as the find, chosen by the one
         // switch above: with the compiled matcher they are compiled too (cursor-free, including
         // the Java program of a modality), with the interpreter they are interpreted.
+        int assumesCount = 0;
         for (final SequentFormula sf : assumesSequent) {
             assumesMatchPrograms.put(sf.formula(),
                 matchProgramFor((JTerm) sf.formula(), useInterpreter));
-            assumesKeySources.put(sf.formula(), keySourceFor((JTerm) sf.formula()));
+            final PatternKeySource keySource = keySourceFor((JTerm) sf.formula());
+            assumesKeySources.put(sf.formula(), keySource);
+            logDecision("Built \\assumes matcher #%d for formula '%s' with key source %s.",
+                ++assumesCount, sf.formula(), keySource);
+        }
+    }
+
+    private void logDecision(String message, Object... args) {
+        if (out != null) {
+            out.format(message, args);
+            out.println();
+            out.flush();
         }
     }
 
@@ -204,6 +238,9 @@ private static MatchProgram matchProgramFor(JTerm pattern, boolean interpreter)
             @NonNull LogicServices p_services) {
         final MatchProgram program = assumesMatchPrograms.get(p_template);
         if (program == null) {
+            logDecision(
+                "Failed to match \\assumes template '%s': it is not an assumes formula of this taclet.",
+                p_template);
             throw new IllegalArgumentException(
                 "template is not an assumes formula of this taclet: " + p_template);
         }
@@ -218,6 +255,10 @@ private static MatchProgram matchProgramFor(JTerm pattern, boolean interpreter)
 
         if (updateContextPresent) {
             context = mc.getInstantiations().getUpdateContext();
+            logDecision(
+                "Matching \\assumes template '%s' against candidates with a non-empty update context; "
+                    + "each candidate's own update prefix must match the context first.",
+                p_template);
         }
 
         for (var cf : p_toMatch) {
@@ -231,11 +272,26 @@ private static MatchProgram matchProgramFor(JTerm pattern, boolean interpreter)
                     checkConditions(program.match(formula, mc, p_services), p_services);
 
                 if (newMC != null) {
+                    logDecision(
+                        "Candidate formula '%s' matches \\assumes template '%s' (variable conditions satisfied).",
+                        cf.getSequentFormula().formula(), p_template);
                     resFormulas = resFormulas.prepend(cf);
                     resMC = resMC.prepend(newMC);
+                } else {
+                    logDecision(
+                        "Candidate formula '%s' rejected for \\assumes template '%s': "
+                            + "term match or variable conditions failed.",
+                        cf.getSequentFormula().formula(), p_template);
                 }
+            } else {
+                logDecision(
+                    "Candidate formula '%s' rejected for \\assumes template '%s': "
+                        + "its update prefix does not match the current update context.",
+                    cf.getSequentFormula().formula(), p_template);
             }
         }
+        logDecision("\\assumes matching for template '%s' found %d matching candidate(s).",
+            p_template, resFormulas.size());
         return new AssumesMatchResult(resFormulas, resMC);
     }
 
@@ -264,8 +320,15 @@ private JTerm matchUpdateContext(ImmutableList<UpdateLabelPair> context, JTerm f
                 }
             }
             // update context does not match update prefix of formula
+            logDecision(
+                "Update context mismatch at position %d/%d: expected update '%s', "
+                    + "but candidate's update prefix does not agree (or candidate has none left).",
+                i + 1, size, curContext.head().update());
             return null;
         }
+        logDecision(
+            "Update context of %d update(s) fully matched; continuing with the stripped formula '%s'.",
+            context.size(), formula);
         return formula;
     }
 
@@ -301,11 +364,17 @@ private JTerm matchUpdateContext(ImmutableList<UpdateLabelPair> context, JTerm f
 
             assert assumesSequentIterator.hasNext()
                     : "p_toMatch and assumes sequent must have same number of elements";
+            logDecision(
+                "Matching candidate instantiation '%s' against the next %s \\assumes template.",
+                candidateInst, candidateInAntec ? "antecedent" : "succedent");
             newMC = matchAssumes(
                 ImmutableList.singleton(candidateInst),
                 assumesSequentIterator.next().formula(), p_matchCond, p_services).matchConditions();
 
             if (newMC.isEmpty()) {
+                logDecision(
+                    "Sequential \\assumes matching aborted: candidate '%s' did not match its template.",
+                    candidateInst);
                 return null;
             }
 
@@ -314,6 +383,7 @@ private JTerm matchUpdateContext(ImmutableList<UpdateLabelPair> context, JTerm f
         assert !anteIterator.hasNext() && !succIterator.hasNext()
                 : "p_toMatch and assumes sequent must have same number of elements";
 
+        logDecision("Sequential \\assumes matching succeeded for all candidates.");
         return p_matchCond;
     }
 
@@ -332,6 +402,9 @@ private JTerm matchUpdateContext(ImmutableList<UpdateLabelPair> context, JTerm f
                 // for example SimplifyIfThenElseUpdateCondition
                 // rewrite these conditions and avoid null; conditions that do not involve matched
                 // variables
+                logDecision(
+                    "No schema variables are instantiated yet; delegating directly to the "
+                        + "taclet's variable conditions (e.g. conditions not tied to a matched variable).");
                 return checkVariableConditions(null, null, cond, services);// XXX
             }
 
@@ -342,8 +415,11 @@ private JTerm matchUpdateContext(ImmutableList<UpdateLabelPair> context, JTerm f
                     result = (MatchConditions) checkVariableConditions(sv, se, result, services);
                 }
             }
+        } else {
+            logDecision("Skipping variable condition checks: the term match already failed.");
         }
 
+        logDecision("checkConditions %s.", result != null ? "succeeded" : "failed");
         return result;
     }
 
@@ -381,24 +457,38 @@ private boolean varIsBound(SchemaVariable v) {
             @Nullable SyntaxElement instantiationCandidate,
             @Nullable MatchResultInfo matchCond,
             @NonNull LogicServices services) {
+        logDecision("check variable conditions for %s, %s, %s", var, instantiationCandidate,
+            matchCond);
         if (matchCond != null) {
             if (instantiationCandidate instanceof JTerm term) {
                 if (!(term.op() instanceof QuantifiableVariable)) {
                     if (varIsBound(var) || varDeclaredNotFree(var)) {
                         // match(x) is not a variable, but the corresponding template variable is
                         // bound or declared non free (so it has to be matched to a variable)
+                        logDecision(
+                            "check variable conditions failed: schema variable %s is bound/declared "
+                                + "not-free but was instantiated with the non-variable term '%s'.",
+                            var, term);
                         return null; // FAILED
                     }
                 }
             }
             // check generic conditions
             for (final VariableCondition vc : varconditions) {
+                final MatchResultInfo before = matchCond;
                 matchCond = vc.check(var, instantiationCandidate, matchCond, services);
                 if (matchCond == null) {
+                    logDecision(
+                        "check variable conditions failed: generic variable condition '%s' rejected "
+                            + "instantiation of %s with '%s'.",
+                        vc, var, instantiationCandidate);
                     return null; // FAILED
                 }
+                logDecision("generic variable condition '%s' accepted the instantiation (was: %s).",
+                    vc, before);
             }
         }
+        logDecision("check variable conditions succeeded for %s.", var);
         return matchCond;
     }
 
@@ -413,14 +503,21 @@ private boolean varIsBound(SchemaVariable v) {
      */
     private Pair<JTerm, MatchResultInfo> matchAndIgnoreUpdatePrefix(
             JTerm source, final MatchResultInfo matchResult) {
+        logDecision("Try to match w/o update-prefix.");
         final MatchConditions matchCond = (MatchConditions) matchResult;
         final var instantiations = matchCond.getInstantiations();
         ImmutableList<UpdateLabelPair> updateLabel = instantiations.getUpdateContext();
+        int strippedUpdates = 0;
         while (source.op() instanceof UpdateApplication) {
             final JTerm update = UpdateApplication.getUpdate(source);
             updateLabel = updateLabel.append(new UpdateLabelPair(update, source.getLabels()));
             source = UpdateApplication.getTarget(source);
+            strippedUpdates++;
         }
+        logDecision(
+            "Stripped %d leading update(s) from the term to be matched; remaining term is '%s' "
+                + "and the stripped updates were pushed onto the update context.",
+            strippedUpdates, source);
         return new Pair<>(source,
             matchCond.setInstantiations(instantiations.addUpdateList(updateLabel)));
     }
@@ -434,6 +531,7 @@ private Pair<JTerm, MatchResultInfo> matchAndIgnoreUpdatePrefix(
             @NonNull MatchResultInfo p_matchCond,
             @NonNull LogicServices services) {
         if (findMatchProgram == null) {
+            logDecision("No matching program for \\find was found.");
             return null;
         }
         JTerm source = (JTerm) term;
@@ -444,7 +542,15 @@ private Pair<JTerm, MatchResultInfo> matchAndIgnoreUpdatePrefix(
             p_matchCond = resultUpdateMatch.second;
         }
         final MatchResultInfo matchResult = findMatchProgram.match(source, p_matchCond, services);
-        return matchResult == null ? null : checkConditions(matchResult, services);
+        if (matchResult == null) {
+            logDecision("\\find matching failed: term '%s' does not match the find pattern '%s'.",
+                source, findExp);
+            return null;
+        }
+        final MatchResultInfo checked = checkConditions(matchResult, services);
+        logDecision("\\find matching of term '%s' against pattern '%s' %s.",
+            source, findExp, checked != null ? "succeeded" : "failed its variable conditions");
+        return checked;
     }
 
 
@@ -460,13 +566,23 @@ private Pair<JTerm, MatchResultInfo> matchAndIgnoreUpdatePrefix(
         final MatchSchemaVariableInstruction instr =
             JavaDLMatchVMInstructionSet.getMatchInstructionForSV(sv);
 
+        logDecision("Matching schema variable %s against '%s' using instruction '%s'.",
+            sv, syntaxElement, instr);
+
         // the instruction routes the candidate by kind (term or program element) itself
         matchCond = instr.match(syntaxElement, matchCond, services);
+        if (matchCond == null) {
+            logDecision("Matching schema variable %s against '%s' failed at the instruction level.",
+                sv, syntaxElement);
+            return null;
+        }
         if (syntaxElement instanceof JTerm) {
             matchCond = checkVariableConditions(sv, syntaxElement, matchCond, services);
         } else if (syntaxElement instanceof ProgramElement) {
             matchCond = checkConditions(matchCond, services);
         }
+        logDecision("Matching schema variable %s against '%s' %s.",
+            sv, syntaxElement, matchCond != null ? "succeeded" : "failed");
         return matchCond;
     }
 
diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/TacletMatchDebuggerExtension.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/TacletMatchDebuggerExtension.java
new file mode 100644
index 00000000000..870e8ea938c
--- /dev/null
+++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/TacletMatchDebuggerExtension.java
@@ -0,0 +1,262 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package de.uka.ilkd.key.gui.extension.impl;
+
+import java.awt.*;
+import java.awt.event.ActionEvent;
+import java.io.PrintWriter;
+import java.io.StringWriter;
+import java.util.ArrayList;
+import java.util.Collections;
+import java.util.Comparator;
+import java.util.List;
+import javax.swing.*;
+
+import de.uka.ilkd.key.core.KeYMediator;
+import de.uka.ilkd.key.gui.MainWindow;
+import de.uka.ilkd.key.gui.actions.KeyAction;
+import de.uka.ilkd.key.gui.extension.api.ContextMenuAdapter;
+import de.uka.ilkd.key.gui.extension.api.ContextMenuKind;
+import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension;
+import de.uka.ilkd.key.pp.PosInSequent;
+import de.uka.ilkd.key.proof.Goal;
+import de.uka.ilkd.key.rule.MatchConditions;
+import de.uka.ilkd.key.rule.NoPosTacletApp;
+import de.uka.ilkd.key.rule.Taclet;
+import de.uka.ilkd.key.rule.match.vm.VMTacletMatcher;
+import de.uka.ilkd.key.util.MiscTools;
+
+import org.key_project.logic.Term;
+import org.key_project.prover.rules.TacletMatcher;
+import org.key_project.prover.rules.instantiation.MatchResultInfo;
+import org.key_project.prover.rules.instantiation.SVInstantiations;
+
+import org.jspecify.annotations.NullMarked;
+import org.jspecify.annotations.Nullable;
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
+
+/**
+ * Extension that provides a context menu action for debugging taclet matching on terms.
+ * When clicking on a term in the sequent view, users can select a taclet from a combo box
+ * and see whether it matches the selected term.
+ *
+ * @author Alexander Weigl
+ */
+@KeYGuiExtension.Info(name = "Taclet Match Debugger",
+    description = "Debug taclet matching by selecting a term and testing which taclets match.\n"
+        + "Developer: Alexander Weigl",
+    experimental = false, optional = true, priority = 50)
+@NullMarked
+public class TacletMatchDebuggerExtension implements KeYGuiExtension, KeYGuiExtension.ContextMenu {
+    private static final Logger LOGGER =
+        LoggerFactory.getLogger(TacletMatchDebuggerExtension.class);
+
+    private final ContextMenuAdapter adapter = new ContextMenuAdapter() {
+        @Override
+        public <T> List<Action> getContextActions(KeYMediator mediator, ContextMenuKind<T> kind,
+                @Nullable T underlyingObject) {
+            if (kind != ContextMenuKind.SEQUENT_VIEW
+                    || !(underlyingObject instanceof PosInSequent pos)) {
+                return Collections.emptyList();
+            }
+
+            // Check if we have a valid proof and goal
+            Goal goal = mediator.getSelectedGoal();
+            if (goal == null) {
+                return Collections.emptyList();
+            }
+
+            // Check if the position has a valid term
+            if (pos.getPosInOccurrence() == null) {
+                return Collections.emptyList();
+            }
+
+            var selectedTerm = pos.getPosInOccurrence().subTerm();
+            if (selectedTerm == null) {
+                return Collections.emptyList();
+            }
+
+            return Collections.singletonList(new MatchTacletAction(mediator, pos, selectedTerm));
+        }
+    };
+
+    @Override
+    public <T> List<Action> getContextActions(KeYMediator mediator, ContextMenuKind<T> kind,
+            @Nullable T underlyingObject) {
+        return adapter.getContextActions(mediator, kind, underlyingObject);
+    }
+
+    /**
+     * Action that opens a dialog to select a taclet and test matching.
+     */
+    private static class MatchTacletAction extends KeyAction {
+        private final KeYMediator mediator;
+        private final PosInSequent pos;
+        private final Term selectedTerm;
+
+        public MatchTacletAction(KeYMediator mediator, PosInSequent pos, Term selectedTerm) {
+            this.mediator = mediator;
+            this.pos = pos;
+            this.selectedTerm = selectedTerm;
+            setName("Match Taclets...");
+        }
+
+        @Override
+        public void actionPerformed(ActionEvent e) {
+            MainWindow mainWindow = MainWindow.getInstance();
+
+            // Get all available taclets from the current goal
+            Goal goal = mediator.getSelectedGoal();
+            if (goal == null) {
+                JOptionPane.showMessageDialog(mainWindow,
+                    "No active proof goal available.",
+                    "Error",
+                    JOptionPane.ERROR_MESSAGE);
+                return;
+            }
+
+            // Collect all taclets
+            List<NoPosTacletApp> tacletApps = new ArrayList<>(
+                goal.ruleAppIndex().tacletIndex().allNoPosTacletApps());
+
+            // Add taclets from OneStepSimplifier if available
+            var simplifier = MiscTools.findOneStepSimplifier(goal.proof());
+            if (simplifier != null && !simplifier.isShutdown()) {
+                tacletApps.addAll(simplifier.getCapturedTaclets());
+            }
+
+            if (tacletApps.isEmpty()) {
+                JOptionPane.showMessageDialog(mainWindow,
+                    "No taclets available for matching.",
+                    "Information",
+                    JOptionPane.INFORMATION_MESSAGE);
+                return;
+            }
+
+            // Sort taclets by name for easier selection
+            tacletApps.sort(Comparator.comparing(app -> app.rule().name().toString()));
+
+            // Create array of taclet names for the combo box
+            String[] tacletNames = tacletApps.stream()
+                    .map(app -> app.rule().name().toString())
+                    .toArray(String[]::new);
+
+            // Show dialog with combo box for taclet selection
+            JComboBox<String> tacletComboBox = new JComboBox<>(tacletNames);
+            tacletComboBox.setEditable(false);
+            tacletComboBox.setMaximumRowCount(25);
+
+            JPanel panel = new JPanel(new BorderLayout());
+            panel.add(new JLabel("Select a taclet to match against the term:"), BorderLayout.NORTH);
+            panel.add(tacletComboBox, BorderLayout.CENTER);
+            panel.setBorder(BorderFactory.createEmptyBorder(10, 10, 10, 10));
+
+            int result = JOptionPane.showConfirmDialog(
+                mainWindow,
+                panel,
+                "Match Taclet",
+                JOptionPane.OK_CANCEL_OPTION,
+                JOptionPane.PLAIN_MESSAGE);
+
+            if (result == JOptionPane.OK_OPTION) {
+                int selectedIndex = tacletComboBox.getSelectedIndex();
+                if (selectedIndex >= 0 && selectedIndex < tacletApps.size()) {
+                    NoPosTacletApp selectedTacletApp = tacletApps.get(selectedIndex);
+                    Taclet selectedTaclet = selectedTacletApp.rule();
+
+                    performMatching(selectedTaclet, selectedTerm, goal);
+                }
+            }
+        }
+
+        /**
+         * Performs the actual taclet matching and displays the results.
+         */
+        private void performMatching(Taclet taclet, Term term, Goal goal) {
+            StringWriter out = new StringWriter();
+            PrintWriter output = new PrintWriter(out);
+            var services = goal.proof().getServices();
+            TacletMatcher matcher = new VMTacletMatcher(taclet, output);
+
+            output.printf("=== Taclet Match Debug ===\n\n");
+            output.printf("Selected Term: %s\n\n", term);
+            output.printf("Selected Taclet: %s\n\n", taclet.name());
+
+            // Print taclet definition
+            output.printf("Taclet Definition:\n");
+            output.printf("----------------------------------------\n");
+            try {
+                var lp = de.uka.ilkd.key.pp.LogicPrinter.purePrinter(
+                    new de.uka.ilkd.key.pp.NotationInfo(), null);
+                lp.printTaclet(taclet);
+                output.println(lp.result());
+            } catch (Exception ex) {
+                output.printf("Could not print taclet: %s\n", ex.getMessage());
+            }
+            output.printf("----------------------------------------\n\n");
+
+            // Try to match
+            output.printf("Matching Result:\n");
+            output.printf("----------------------------------------\n");
+
+            try {
+                // Create initial match conditions
+                MatchResultInfo initialMatchCond = MatchConditions.EMPTY_MATCHCONDITIONS;
+
+                MatchResultInfo matchResult = matcher.matchFind(term, initialMatchCond, services);
+
+                if (matchResult != null) {
+                    output.printf("✓ MATCH SUCCESSFUL!\n\n");
+
+                    // Print variable instantiations
+                    SVInstantiations instantiations = matchResult.getInstantiations();
+                    var instMap = instantiations.getInstantiationMap();
+                    if (instMap != null && !instMap.isEmpty()) {
+                        output.printf("Variable Instantiations:\n");
+                        for (var entry : instMap) {
+                            output.printf("  %s := %s\n", entry.key().name(),
+                                entry.value().getInstantiation());
+                        }
+                    } else {
+                        output.printf("No variable instantiations needed.\n");
+                    }
+
+                    // Check additional conditions
+                    MatchResultInfo checkedResult = matcher.checkConditions(matchResult, services);
+                    if (checkedResult != null) {
+                        output.printf("\n✓ All taclet conditions satisfied!\n");
+                    } else {
+                        output.printf("\n✗ Taclet conditions NOT satisfied!\n");
+                    }
+                } else {
+                    output.printf("✗ NO MATCH - The taclet does not match the selected term.\n");
+                }
+            } catch (Exception ex) {
+                output.printf("✗ ERROR during matching: ").printf(ex.getMessage()).printf("\n");
+                LOGGER.error("Error during taclet matching", ex);
+            }
+
+            output.printf("----------------------------------------\n");
+
+            // Output to console
+            LOGGER.info("Taclet matching performed for taclet: {}, {}", taclet.name(), out);
+
+            // Also show in a dialog
+            JTextArea textArea = new JTextArea(out.toString());
+            textArea.setEditable(false);
+            textArea.setCaretPosition(0);
+            textArea.setFont(new Font(Font.MONOSPACED, Font.PLAIN, 12));
+
+            JScrollPane scrollPane = new JScrollPane(textArea);
+            scrollPane.setPreferredSize(new Dimension(700, 500));
+
+            JOptionPane.showMessageDialog(
+                MainWindow.getInstance(),
+                scrollPane,
+                "Taclet Match Result",
+                JOptionPane.INFORMATION_MESSAGE);
+        }
+    }
+}
diff --git a/key.ui/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension b/key.ui/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension
index 5c590ebaca9..915df3d286e 100644
--- a/key.ui/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension
+++ b/key.ui/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension
@@ -11,4 +11,5 @@ de.uka.ilkd.key.gui.JmlEnabledKeysIndicator
 de.uka.ilkd.key.gui.extension.impl.ProfileNameInStatusBar
 de.uka.ilkd.key.gui.extension.impl.ParallelProverStatusIndicator
 de.uka.ilkd.key.gui.profileloading.WDLoadDialogOptionPanel
-de.uka.ilkd.key.gui.extension.impl.SoundinessExtension
\ No newline at end of file
+de.uka.ilkd.key.gui.extension.impl.SoundinessExtension
+de.uka.ilkd.key.gui.extension.impl.TacletMatchDebuggerExtension
\ No newline at end of file

From 32ef0544597e2f6b91727430db633d97b203ebe8 Mon Sep 17 00:00:00 2001
From: Richard Bubel <bubel@cs.tu-darmstadt.de>
Date: Fri, 21 Aug 2026 07:13:52 +0200
Subject: [PATCH 3/4] Fix in replacewith of "instance_eval_id" taclet and added
 small example

---
 .../de/uka/ilkd/key/proof/rules/javaRules.key |  4 +--
 .../src/InstanceOfPatternExample.java         | 28 +++++++++++++++++--
 2 files changed, 27 insertions(+), 5 deletions(-)

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 10a38e4384f..61da8c0360e 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
@@ -1591,13 +1591,13 @@
     // -----------                  instanceof                -----------
     // ----------------------------------------------------------------------------
 
-		instanceof_eval_id {
+	instanceof_eval_id {
         \find(\modality{#allmodal}{.. #v = #nse instanceof #t #id; ...}\endmodality (post))
         \varcond(\newTypeOf(#v0, #nse))
         \replacewith(\modality{#allmodal}{..
 	            #typeof(#nse) #v0=#nse;
 	            #v=#v0 instanceof #t;
-	            #t #id = (#t) #v;
+	            #t #id = (#t) #v0;
             ...}\endmodality (post))
         \heuristics(simplify_autoname)
     };
diff --git a/key.ui/examples/Java/InstanceOfPattern/src/InstanceOfPatternExample.java b/key.ui/examples/Java/InstanceOfPattern/src/InstanceOfPatternExample.java
index c7d5282d439..3a7ed766223 100644
--- a/key.ui/examples/Java/InstanceOfPattern/src/InstanceOfPatternExample.java
+++ b/key.ui/examples/Java/InstanceOfPattern/src/InstanceOfPatternExample.java
@@ -14,11 +14,33 @@
  *   }
  */
 public class InstanceOfPatternExample {
-    
+
     /**
-     * Basic instanceof pattern matching example.
-     * The variable 's' is bound in the true branch of the instanceof check.
+     *
      */
+
+    /*@ normal_behavior
+      @ requires obj != null;
+      @ ensures \result instanceof String;
+      @*/
+    public static Object getString(Object obj) {
+        return "ha";
+    }
+
+    /*@ normal_behavior
+      @ requires obj != null;
+      @ ensures \result;
+      @*/
+    public static boolean isString(Object obj) {
+        boolean result = getString(obj) instanceof String id;
+        return result;
+    }
+
+
+        /**
+         * Basic instanceof pattern matching example.
+         * The variable 's' is bound in the true branch of the instanceof check.
+         */
     /*@ normal_behavior
       @ requires obj != null;
       @ ensures \result >= 0;

From 73183af8f9b82211496e47d5c89da0c437367d0b Mon Sep 17 00:00:00 2001
From: Alexander Weigl <weigl@kit.edu>
Date: Sat, 22 Aug 2026 17:40:58 +0200
Subject: [PATCH 4/4] add cast in pos/negBinding, more rules

---
 .../java/visitor/BindingVariableVisitor.java  |  6 +++-
 .../de/uka/ilkd/key/proof/rules/javaRules.key | 36 ++++++++++++++++++-
 .../src/InstanceOfPatternExample.java         | 15 ++------
 3 files changed, 43 insertions(+), 14 deletions(-)

diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/BindingVariableVisitor.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/BindingVariableVisitor.java
index cd0fe5bee21..4c114dfd693 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/BindingVariableVisitor.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/BindingVariableVisitor.java
@@ -41,7 +41,11 @@ public static Bindings analyze(Expression e) {
             // it can't be determined at compile time that the match failed
             // in a way that still binds anything.
             var name = (LocationVariable) io.getPatternVariable().getProgramVariable();
-            var expr = io.getExpressionAt(0);
+            Expression expr = io.getExpressionAt(0);
+
+            // add a cast
+            expr = new TypeCast(expr, io.getTypeReference());
+
             return new Bindings(Map.of(name, expr), Map.of());
         } else if (e instanceof BinaryOperator bo) {
             if (bo.getKind() == BinaryOperatorKind.LOGICAL_AND) {
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 61da8c0360e..79b72e9cb99 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
@@ -1597,7 +1597,41 @@
         \replacewith(\modality{#allmodal}{..
 	            #typeof(#nse) #v0=#nse;
 	            #v=#v0 instanceof #t;
-	            #t #id = (#t) #v0;
+	            // not needed #t #id = (#t) #v0;
+            ...}\endmodality (post))
+        \heuristics(simplify_autoname)
+    };
+
+		instanceof_eval_id_and {
+        \find(\modality{#allmodal}{.. #v = #b0 instanceof #t #id && #nse; ...}\endmodality (post))
+        \replacewith(\modality{#allmodal}{..
+	            #v = #b0 instanceof #t;
+	            if(#v) {
+	              #t #id = (#t) #b0;
+	              #v = /*true&&*/ #nse;
+	            }
+            ...}\endmodality (post))
+        \heuristics(simplify_autoname)
+    };
+
+    instanceof_eval_id_or {
+        \find(\modality{#allmodal}{.. #v = !(#b0 instanceof #t #id) || #nse; ...}\endmodality (post))
+        \replacewith(\modality{#allmodal}{..
+              #v = #b0 instanceof #t;
+              if(!#v) {
+                #t #id = (#t) #b0;
+                #v = /*false || */ #nse;
+              }
+            ...}\endmodality (post))
+        \heuristics(simplify_autoname)
+    };
+
+
+		instanceof_eval_id_simple {
+        \find(\modality{#allmodal}{.. #v = #b0 instanceof #t #id; ...}\endmodality (post))
+        \replacewith(\modality{#allmodal}{..
+	            #v=#b0 instanceof #t;
+	            // not needed #t #id = (#t) #v0;
             ...}\endmodality (post))
         \heuristics(simplify_autoname)
     };
diff --git a/key.ui/examples/Java/InstanceOfPattern/src/InstanceOfPatternExample.java b/key.ui/examples/Java/InstanceOfPattern/src/InstanceOfPatternExample.java
index 3a7ed766223..caa282c51fd 100644
--- a/key.ui/examples/Java/InstanceOfPattern/src/InstanceOfPatternExample.java
+++ b/key.ui/examples/Java/InstanceOfPattern/src/InstanceOfPatternExample.java
@@ -14,10 +14,7 @@
  *   }
  */
 public class InstanceOfPatternExample {
-
-    /**
-     *
-     */
+    //@ static invariant_free (\forall String s; true; s.length() >= 0);
 
     /*@ normal_behavior
       @ requires obj != null;
@@ -32,17 +29,11 @@ public static Object getString(Object obj) {
       @ ensures \result;
       @*/
     public static boolean isString(Object obj) {
-        boolean result = getString(obj) instanceof String id;
-        return result;
+        return getString(obj) instanceof String id && id.length() >= 0;
     }
 
-
-        /**
-         * Basic instanceof pattern matching example.
-         * The variable 's' is bound in the true branch of the instanceof check.
-         */
     /*@ normal_behavior
-      @ requires obj != null;
+      @ requires obj instanceof String;
       @ ensures \result >= 0;
       @*/
     public static int getStringLength(Object obj) {