From 5e65402ecb18292cdd44f9f96801e15abb3ec7b1 Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Fri, 27 Jun 2025 10:49:10 +0200
Subject: [PATCH 1/2] Fixes

---
 Source/Core/AST/AbsyQuant.cs | 46 ++++++++++++++++++++++--------------
 1 file changed, 28 insertions(+), 18 deletions(-)

diff --git a/Source/Core/AST/AbsyQuant.cs b/Source/Core/AST/AbsyQuant.cs
index a5ae7175e..4778485f0 100644
--- a/Source/Core/AST/AbsyQuant.cs
+++ b/Source/Core/AST/AbsyQuant.cs
@@ -245,8 +245,8 @@ public override void Resolve(ResolutionContext rc)
           kv.Resolve(rc);
         }
 
-        this.ResolveTriggers(rc);
         Body.Resolve(rc);
+        this.ResolveTriggers(rc);
         rc.PopVarContext();
 
         // establish a canonical order of the type parameters
@@ -730,27 +730,37 @@ private void ApplyNeverTriggers()
 
     protected override void ResolveTriggers(ResolutionContext rc)
     {
-      for (Trigger tr = this.Triggers; tr != null; tr = tr.Next)
+      var freeBodyVars = new Set();
+      Body.ComputeFreeVariables(freeBodyVars);
+      
+      // No idea why this copy is necessary. Why would dummies be shared?
+      Dummies = Dummies.ToList();
+      
+      for (var tr = this.Triggers; tr != null; tr = tr.Next)
       {
         int prevErrorCount = rc.ErrorCount;
         tr.Resolve(rc);
-        if (prevErrorCount == rc.ErrorCount)
-        {
-          // for positive triggers, make sure all bound variables are mentioned
-          if (tr.Pos)
-          {
-            Set /*Variable*/
-              freeVars = new Set /*Variable*/();
-            tr.ComputeFreeVariables(freeVars);
-            foreach (Variable v in Dummies)
-            {
-              Contract.Assert(v != null);
-              if (!freeVars[v])
-              {
-                rc.Error(tr, "trigger must mention all quantified variables, but does not mention: {0}", v);
-              }
-            }
+        if (prevErrorCount != rc.ErrorCount) {
+          continue;
+        }
+
+        // for positive triggers, make sure all bound variables are mentioned
+        if (!tr.Pos) {
+          continue;
+        }
+
+        var freeVars = new Set();
+        tr.ComputeFreeVariables(freeVars);
+        for (var index = 0; index < Dummies.Count; index++) {
+          var variable = Dummies[index];
+          Contract.Assert(variable != null);
+          if (freeVars[variable] || freeBodyVars.Contains(variable)) {
+            continue;
           }
+
+          Dummies.RemoveAt(index);
+          index--;
+          //rc.Error(tr, "trigger must mention all quantified variables, but does not mention: {0}", v);
         }
       }
     }

From 3ab4a7bd5abc03820008d9ca59f17007cf135084 Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Fri, 27 Jun 2025 17:17:23 +0200
Subject: [PATCH 2/2] Bring back error message

---
 Source/Core/AST/AbsyQuant.cs | 16 ++++++++++------
 1 file changed, 10 insertions(+), 6 deletions(-)

diff --git a/Source/Core/AST/AbsyQuant.cs b/Source/Core/AST/AbsyQuant.cs
index 4778485f0..a2e8594b3 100644
--- a/Source/Core/AST/AbsyQuant.cs
+++ b/Source/Core/AST/AbsyQuant.cs
@@ -749,18 +749,22 @@ protected override void ResolveTriggers(ResolutionContext rc)
           continue;
         }
 
-        var freeVars = new Set();
-        tr.ComputeFreeVariables(freeVars);
+        var freeVarsTrigger = new Set();
+        tr.ComputeFreeVariables(freeVarsTrigger);
         for (var index = 0; index < Dummies.Count; index++) {
           var variable = Dummies[index];
           Contract.Assert(variable != null);
-          if (freeVars[variable] || freeBodyVars.Contains(variable)) {
+          if (freeVarsTrigger[variable]) {
             continue;
           }
 
-          Dummies.RemoveAt(index);
-          index--;
-          //rc.Error(tr, "trigger must mention all quantified variables, but does not mention: {0}", v);
+          if (freeBodyVars.Contains(variable)) {
+            rc.Error(tr, "trigger must mention all quantified variables, but does not mention: {0}", variable);
+          } else {
+            Dummies.RemoveAt(index);
+            index--;
+          }
+
         }
       }
     }