diff --git a/Source/DafnyCore/AST/Statements/Statements.cs b/Source/DafnyCore/AST/Statements/Statements.cs index 7ad30da2913..7b31c85914f 100644 --- a/Source/DafnyCore/AST/Statements/Statements.cs +++ b/Source/DafnyCore/AST/Statements/Statements.cs @@ -483,7 +483,7 @@ public TypeRhs(Cloner cloner, TypeRhs original) if (original.ArrayDimensions != null) { if (original.InitDisplay != null) { Contract.Assert(original.ArrayDimensions.Count == 1); - ArrayDimensions = new List { original.ArrayDimensions[0] }; + ArrayDimensions = new List { cloner.CloneExpr(original.ArrayDimensions[0]) }; InitDisplay = original.InitDisplay.ConvertAll(cloner.CloneExpr); } else { ArrayDimensions = original.ArrayDimensions.Select(cloner.CloneExpr).ToList(); diff --git a/Test/git-issues/github-issue-3343.dfy b/Test/git-issues/github-issue-3343.dfy new file mode 100644 index 00000000000..517a11d7fc1 --- /dev/null +++ b/Test/git-issues/github-issue-3343.dfy @@ -0,0 +1,6 @@ +// RUN: %baredafny run "%s" -t:java > "%t" +// RUN: %diff "%s.expect" "%t" +method Bug() { + var zero := 0; + var a := new int[zero] []; +} diff --git a/Test/git-issues/github-issue-3343.dfy.expect b/Test/git-issues/github-issue-3343.dfy.expect new file mode 100644 index 00000000000..823a60a105c --- /dev/null +++ b/Test/git-issues/github-issue-3343.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 1 verified, 0 errors