Dafny: fixed a crash in datatype argument resolution

1 files changed, 2 insertions, 1 deletions

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index 81d79085..04350247 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -4290,7 +4290,8 @@ namespace Microsoft.Dafny {
       } else if (expr is DatatypeValue) {

         var e = (DatatypeValue)expr;

         // check all NON-ghost arguments

-        for (int i = 0; i < e.Ctor.Formals.Count; i++) {

+        // note that if resolution is successful, then |e.Arguments| == |e.Ctor.Formals|

+        for (int i = 0; i < e.Arguments.Count; i++) {

           if (!e.Ctor.Formals[i].IsGhost) {

             CheckIsNonGhost(e.Arguments[i]);

           }