diff --git a/Source/Dafny/Compiler-java.cs b/Source/Dafny/Compiler-java.cs index a66c534fed0..76e10486182 100644 --- a/Source/Dafny/Compiler-java.cs +++ b/Source/Dafny/Compiler-java.cs @@ -1465,7 +1465,7 @@ public void EmitRead(ConcreteSyntaxTree wr) { public ConcreteSyntaxTree EmitWrite(ConcreteSyntaxTree wr) { ConcreteSyntaxTree w; if (Indices.Count == 1) { - wr.Write($"{FormatTypeDescriptorVariable(ElmtTypeParameter)}.setArrayElement({Array}, {Indices[0]}.intValue(),"); + wr.Write($"{FormatTypeDescriptorVariable(ElmtTypeParameter)}.setArrayElement({Array}, {Indices[0]},"); w = wr.Fork(); wr.Write(")"); } else { @@ -1473,6 +1473,7 @@ public ConcreteSyntaxTree EmitWrite(ConcreteSyntaxTree wr) { w = wr.Fork(); wr.Write(")"); } + Compiler.EndStmt(wr); return w; } } diff --git a/Test/comp/Arrays.dfy b/Test/comp/Arrays.dfy index 971eccbd645..d4651343d99 100644 --- a/Test/comp/Arrays.dfy +++ b/Test/comp/Arrays.dfy @@ -314,6 +314,13 @@ class Cell { { x, y := arr, arr; } + method UArray(x: T) + modifies arr + { + if arr.Length > 0 { + arr[0] := x; + } + } } type ychar = ch | '\0' <= ch <= 'z' diff --git a/Test/comp/Arrays.dfy.expect b/Test/comp/Arrays.dfy.expect index ce8dbb84b27..6af6e3e356e 100644 --- a/Test/comp/Arrays.dfy.expect +++ b/Test/comp/Arrays.dfy.expect @@ -1,5 +1,5 @@ -Dafny program verifier finished with 41 verified, 0 errors +Dafny program verifier finished with 42 verified, 0 errors Dafny program verifier did not attempt verification 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22