summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Dafny/Translator.cs3
1 files changed, 2 insertions, 1 deletions
diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index bdb436ce..cd084ca1 100644
--- a/Dafny/Translator.cs
+++ b/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);
}