Dafny: fallback to ShallowType (elements of IndexField arrays seem to have Type null)

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);

       }