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.cs2
1 files changed, 2 insertions, 0 deletions
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 55dd637c..50324002 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -13126,6 +13126,8 @@ namespace Microsoft.Dafny {
visitor.Visit(f.Body);
foreach (var expr in f.Ens) { visitor.Visit(expr); }
foreach (var expr in f.Req) { visitor.Visit(expr); }
+ foreach (var expr in f.Reads) { visitor.Visit(expr); }
+ foreach (var expr in f.Decreases.Expressions) { visitor.Visit(expr); }
return f.Formals.Zip(fexp.Args).All(formal_concrete => CanSafelySubstitute(visitor.TriggerVariables, formal_concrete.Item1, formal_concrete.Item2));
}