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.cs3
1 files changed, 2 insertions, 1 deletions
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index bdb436ce..cd084ca1 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -3946,8 +3946,9 @@ Contract.Requires(tok != null);
args.Add(heap);
args.Add(r);
args.Add(f);
+ Bpl.Type t = (f.Type != null) ? f.Type : f.ShallowType;
return new Bpl.NAryExpr(tok,
- new Bpl.FunctionCall(new Bpl.IdentifierExpr(tok, "read", f.Type.AsCtor.Arguments[0])),
+ new Bpl.FunctionCall(new Bpl.IdentifierExpr(tok, "read", t.AsCtor.Arguments[0])),
args);
}