summaryrefslogtreecommitdiff
path: root/Source/Dafny/Translator.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Dafny/Translator.cs')
-rw-r--r--Source/Dafny/Translator.cs4
1 files changed, 3 insertions, 1 deletions
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index b5d89abd..14fca463 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -13107,8 +13107,10 @@ namespace Microsoft.Dafny {
return f.Formals.Zip(fexp.Args).All(formal_concrete => CanSafelySubstitute(visitor.TriggerVariables, formal_concrete.Item1, formal_concrete.Item2));
}
+ Triggers.TriggersCollector triggersCollector = new Triggers.TriggersCollector();
+
private bool CanSafelySubstitute(ISet<IVariable> protectedVariables, IVariable variable, Expression substitution) {
- return !(protectedVariables.Contains(variable) && Dafny.Triggers.TriggersCollector.IsTriggerKiller(substitution));
+ return !(protectedVariables.Contains(variable) && triggersCollector.IsTriggerKiller(substitution));
}
private class VariablesCollector: BottomUpVisitor {