clear debug info

Author: CatarinaGamboa

liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java

@@ -50,9 +50,15 @@ public static boolean smtEnabled() {
      * Set by {@link #smtStart} (the structured / flat VC printers) and consumed by {@link #smtRawQuery}. Lets the
      * low-level Z3 boundary trace skip a query that a higher layer already printed in full, so {@code -a} shows every
      * query exactly once. Single-threaded: each {@code smtStart} is immediately followed by one {@code solver.check()}.
+     * Callers that may abort a structured check before {@code solver.check()} (e.g. a translation failure) must clear
+     * the flag via {@link #clearStructuredQueryPending} so suppression cannot leak onto the next, unrelated query.
      */
     private static boolean structuredQueryPending = false;
 
+    public static void clearStructuredQueryPending() {
+        structuredQueryPending = false;
+    }
+
     /**
      * Catch-all trace emitted at the actual {@code solver.check()} boundary so {@code -a} / {@code -d} show EVERY query
      * sent to Z3 — including those that bypass the structured {@link #smtStart} path (the simplifier's implication

liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java

@@ -65,6 +65,8 @@ public SMTResult verifySubtype(Predicate subRef, Predicate supRef, Context conte
             e.printStackTrace();
         } catch (Z3Exception e) {
             throw new Z3Exception(e.getLocalizedMessage());
+        } finally {
+            DebugLog.clearStructuredQueryPending();
         }
         return SMTResult.ok();
     }