@@ -29,6 +29,7 @@ public final class DebugLog {
     private static final String SMT_TAG = Colors.BLUE + "[SMT]" + Colors.RESET;
     private static final String SMT_CHECK = Colors.SALMON + "[SMT CHECK]" + Colors.RESET;
     private static final String SMP_TAG = Colors.YELLOW + "[SMP]" + Colors.RESET;
+    private static final String WARN_TAG = Colors.SALMON + "[WARN]" + Colors.RESET;
 
     private DebugLog() {
     }
@@ -37,6 +38,17 @@ public static boolean enabled() {
         return CommandLineLauncher.cmdArgs.debugMode;
     }
 
+    /**
+     * A non-fatal problem the verifier worked around (e.g. a supertype it could not resolve), which may explain a
+     * missing or unexpected result.
+     */
+    public static void warn(String message) {
+        if (!enabled()) {
+            return;
+        }
+        System.out.println(WARN_TAG + " " + message);
+    }
+
     /**
      * One-line header for a verification check: emits the absolute file path + line so terminals (iTerm2, VS Code,
      * WezTerm, …) make it ⌘/Ctrl-clickable. Replaces the older two-line {@code info()} prints.
 
@@ -1,10 +1,11 @@
 package liquidjava.processor.context;
 
-import java.util.ArrayDeque;
 import java.util.ArrayList;
 import java.util.Deque;
+import java.util.LinkedList;
 import java.util.List;
 import java.util.Set;
+import liquidjava.diagnostics.DebugLog;
 import liquidjava.rj_language.Predicate;
 import spoon.reflect.declaration.CtElement;
 import spoon.reflect.reference.CtTypeReference;
@@ -35,26 +36,21 @@ public List<CtTypeReference<?>> getSuperTypes() {
      * direct superclass is {@code Exception}).
      */
     public void addSuperTypes(CtTypeReference<?> ts, Set<CtTypeReference<?>> sts) {
-        Deque<CtTypeReference<?>> todo = new ArrayDeque<>();
-        if (ts != null)
-            todo.add(ts);
-        for (CtTypeReference<?> ct : sts)
-            if (ct != null)
-                todo.add(ct);
+        // LinkedList, unlike ArrayDeque, accepts the nulls of a missing superclass, skipped when polled
+        Deque<CtTypeReference<?>> todo = new LinkedList<>(sts);
+        todo.addFirst(ts);
         while (!todo.isEmpty()) {
             CtTypeReference<?> t = todo.poll();
-            if (supertypes.contains(t))
+            if (t == null || supertypes.contains(t))
                 continue;
             supertypes.add(t);
             try {
-                CtTypeReference<?> sup = t.getSuperclass();
-                if (sup != null)
-                    todo.add(sup);
-                for (CtTypeReference<?> i : t.getSuperInterfaces())
-                    if (i != null)
-                        todo.add(i);
-            } catch (RuntimeException | LinkageError ignored) {
+                todo.add(t.getSuperclass());
+                todo.addAll(t.getSuperInterfaces());
+            } catch (RuntimeException | LinkageError e) {
                 // a supertype that cannot be resolved (no source, not on the classpath) ends the walk on that branch
+                DebugLog.warn("Could not resolve the supertypes of " + t.getQualifiedName()
+                        + "; specs declared above it will not apply to " + getName() + " (" + e + ")");
             }
         }
     }
 
@@ -49,14 +49,6 @@ public static void handleConstructorState(CtConstructor<?> c, RefinedFunction f,
         }
     }
 
-    /**
-     * An unannotated constructor whose body starts with {@code super(...)} leaves the object in the state that the
-     * called superclass constructor's specification gives it (e.g. {@code MyException(String m, Throwable c) { super(m,
-     * c); }} with the {@code Throwable(String, Throwable)} spec: {@code withThrowable(this)}). The super constructor's
-     * parameters are renamed to the arguments passed, which must be parameters of this constructor or literals.
-     *
-     * @return whether a state was inherited (otherwise the caller falls back to the default state)
-     */
     /**
      * JDK classes whose constructors all pass their arguments unchanged to the superclass constructor with the same
      * parameter types (documented in their Javadoc), so a spec on that superclass constructor describes them too. Only
@@ -66,6 +58,43 @@ public static void handleConstructorState(CtConstructor<?> c, RefinedFunction f,
     private static final Set<String> DELEGATING_JDK_CLASSES = Set.of("java.lang.Exception",
             "java.lang.RuntimeException", "java.lang.Error");
 
+    /**
+     * An unannotated constructor whose body starts with {@code super(...)} leaves the object in the state that the
+     * called superclass constructor's specification gives it (e.g. {@code MyException(String m, Throwable c) { super(m,
+     * c); }} with the {@code Throwable(String, Throwable)} spec: {@code withThrowable(this)}). The super constructor's
+     * parameters are renamed to the arguments passed, which must be parameters of this constructor or literals.
+     *
+     * @return whether a state was inherited (otherwise the caller falls back to the default state)
+     */
+    private static boolean inheritSuperConstructorState(CtConstructor<?> c, RefinedFunction f, TypeChecker tc) {
+        CtInvocation<?> call = superConstructorCall(c);
+        if (call == null)
+            return false;
+        var exe = call.getExecutable();
+        RefinedFunction superF = specifiedConstructor(tc, exe.getSimpleName(), exe.getDeclaringType(),
+                exe.getParameters());
+        if (superF == null || superF.getToStates().isEmpty()
+                || superF.getArguments().size() != call.getArguments().size())
+            return false;
+        List<ObjectState> states = renameStates(superF.getToStates(), superParamsToArguments(superF, call));
+        if (states == null)
+            return false;
+        f.setAllStates(states);
+        return true;
+    }
+
+    /** The {@code super(...)} call that starts the body of {@code c}, or null if it does not start with one. */
+    private static CtInvocation<?> superConstructorCall(CtConstructor<?> c) {
+        if (c.getBody() == null || c.getBody().getStatements().isEmpty()
+                || !(c.getBody().getStatement(0)instanceof CtInvocation<?> call))
+            return null;
+        var exe = call.getExecutable();
+        if (exe == null || !exe.isConstructor() || exe.getDeclaringType() == null || c.getDeclaringType() == null
+                || exe.getDeclaringType().equals(c.getDeclaringType().getReference()))
+            return null; // not a super(...) call (this(...) delegates within the class)
+        return call;
+    }
+
     /** The specified constructor that {@code name(params)} of {@code type} ends up running, if one is known. */
     private static RefinedFunction specifiedConstructor(TypeChecker tc, String name, CtTypeReference<?> type,
             List<CtTypeReference<?>> params) {
@@ -82,19 +111,11 @@ private static RefinedFunction specifiedConstructor(TypeChecker tc, String name,
         return null;
     }
 
-    private static boolean inheritSuperConstructorState(CtConstructor<?> c, RefinedFunction f, TypeChecker tc) {
-        if (c.getBody() == null || c.getBody().getStatements().isEmpty()
-                || !(c.getBody().getStatement(0)instanceof CtInvocation<?> call))
-            return false;
-        var exe = call.getExecutable();
-        if (exe == null || !exe.isConstructor() || exe.getDeclaringType() == null || c.getDeclaringType() == null
-                || exe.getDeclaringType().equals(c.getDeclaringType().getReference()))
-            return false; // not a super(...) call (this(...) delegates within the class)
-        RefinedFunction superF = specifiedConstructor(tc, exe.getSimpleName(), exe.getDeclaringType(),
-                exe.getParameters());
-        if (superF == null || superF.getToStates().isEmpty()
-                || superF.getArguments().size() != call.getArguments().size())
-            return false;
+    /**
+     * Maps each parameter of the super constructor to the name of the argument {@code call} passes for it: a parameter
+     * of the calling constructor or a non-string literal, or null for any other expression.
+     */
+    private static Map<String, String> superParamsToArguments(RefinedFunction superF, CtInvocation<?> call) {
         Map<String, String> rename = new HashMap<>();
         for (int i = 0; i < call.getArguments().size(); i++) {
             CtExpression<?> arg = call.getArguments().get(i);
@@ -107,12 +128,20 @@ else if (arg instanceof CtLiteral<?> lit && lit.getValue() != null && !(lit.getV
             else
                 rename.put(param, null); // an argument we cannot name: usable only if the state ignores it
         }
+        return rename;
+    }
+
+    /**
+     * The given states with the super constructor's parameters renamed, or null if one of them mentions a parameter
+     * whose argument has no name.
+     */
+    private static List<ObjectState> renameStates(List<Predicate> toStates, Map<String, String> rename) {
         List<ObjectState> states = new ArrayList<>();
-        for (Predicate to : superF.getToStates()) {
+        for (Predicate to : toStates) {
             for (Map.Entry<String, String> r : rename.entrySet()) {
                 if (r.getValue() == null) {
                     if (to.getVariableNames().contains(r.getKey()))
-                        return false;
+                        return null;
                 } else {
                     to = to.substituteVariable(r.getKey(), r.getValue());
                 }
@@ -121,8 +150,7 @@ else if (arg instanceof CtLiteral<?> lit && lit.getValue() != null && !(lit.getV
             os.setTo(to);
             states.add(os);
         }
-        f.setAllStates(states);
-        return true;
+        return states;
     }
 
     /**