Skip to content

Commit

Permalink
Update comment
Browse files Browse the repository at this point in the history
  • Loading branch information
RustanLeino committed Feb 24, 2025
1 parent 62a134b commit 8350f67
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions Source/DafnyCore/Triggers/QuantifiersCollector.cs
Original file line number Diff line number Diff line change
Expand Up @@ -45,8 +45,8 @@ protected override bool VisitOneExpr(Expression expr, ref OldExpr/*?*/ enclosing
if (expr is LetExpr { Exact: false } letExpr) {
// create a corresponding exists quantifier
Contract.Assert(letExpr.RHSs.Count == 1); // let-such-that expressions have exactly 1 RHS
// Note, trigger selection adds some attributes. These will remain in the following exists expression. So, Boogie translation needs
// to look at letExpr.SuchThatExists.Attributes (not letExpr.Attributes) to find them.
// Note, trigger selection adds some attributes. These will remain in the following exists expression. They
// make it back to the letExpr via the ActionsOnSelectedTriggers below.
var existsExpr = new ExistsExpr(letExpr.Origin, letExpr.BoundVars.ToList(), null, letExpr.RHSs[0],
new Attributes("_delayTriggerWarning", new List<Expression>(), letExpr.Attributes)) {
Type = Type.Bool
Expand Down

0 comments on commit 8350f67

Please sign in to comment.