From a291b866c31269ca0f2a7458a6d16fa1b6011535 Mon Sep 17 00:00:00 2001
From: Richard Bubel <bubel@cs.tu-darmstadt.de>
Date: Fri, 2 Oct 2026 10:59:50 +0200
Subject: [PATCH] Fix completeness check

Skolem constants are now first created upon execution of the taclet (not at match time)
Hence, a taclet app queried for "complete" returns false for skolem constants, instead
completeExceptSkolemConstants must be used.
---
 .../java/de/uka/ilkd/key/control/AbstractProofControl.java | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/key.core/src/main/java/de/uka/ilkd/key/control/AbstractProofControl.java b/key.core/src/main/java/de/uka/ilkd/key/control/AbstractProofControl.java
index f8d9f9156c0..2066a5e18b7 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/control/AbstractProofControl.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/control/AbstractProofControl.java
@@ -195,7 +195,7 @@ private ImmutableList<TacletApp> filterTaclet(Goal focusedGoal,
     public boolean selectedTaclet(Taclet taclet, Goal goal,
             PosInOccurrence pos) {
         ImmutableSet<TacletApp> applics = getAppsForName(goal, taclet.name().toString(), pos);
-        if (applics.size() == 0) {
+        if (applics.isEmpty()) {
             return false;
         }
         return selectedTaclet(applics, goal);
@@ -207,7 +207,7 @@ public boolean selectedTaclet(ImmutableSet<TacletApp> applics, Goal goal) {
         if (applics.size() == 1) {
             TacletApp firstApp = it.next();
             boolean ifSeqInteraction = !firstApp.taclet().assumesSequent().isEmpty();
-            if (isMinimizeInteraction() && !firstApp.complete()) {
+            if (isMinimizeInteraction() && !firstApp.completeExceptSkolemConstants()) {
                 ImmutableList<TacletApp> ifSeqCandidates =
                     firstApp.findIfFormulaInstantiations(goal.sequent(), services);
 
@@ -229,7 +229,8 @@ public boolean selectedTaclet(ImmutableSet<TacletApp> applics, Goal goal) {
                 }
 
             }
-            if (ifSeqInteraction || !firstApp.complete()) {
+            if (ifSeqInteraction || !firstApp.completeExceptSkolemConstants() ||
+                    (!isMinimizeInteraction() && !firstApp.complete())) {
                 LinkedList<TacletApp> l = new LinkedList<>();
                 l.add(firstApp);
                 TacletInstantiationModel[] models = completeAndApplyApp(l, goal);