diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala index a232b93dad0a624ee9d5e3663027948f4b8e783b..24ecca501029604f25dc9c285e797be4562c5a01 100644 --- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala +++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala @@ -1200,11 +1200,11 @@ trait CodeExtraction extends ASTExtractors { } getOwner(lhsRec) match { - case Some(Some(fd)) if fd != currentFunDef => - outOfSubsetError(tr, "cannot update an array that is not defined locally") + // case Some(Some(fd)) if fd != currentFunDef => + // outOfSubsetError(tr, "cannot update an array that is not defined locally") - case Some(None) => - outOfSubsetError(tr, "cannot update an array that is not defined locally") + // case Some(None) => + // outOfSubsetError(tr, "cannot update an array that is not defined locally") case Some(_) => diff --git a/src/test/resources/regression/verification/xlang/valid/ArrayNested1.scala b/src/test/resources/regression/verification/xlang/valid/ArrayNested1.scala new file mode 100644 index 0000000000000000000000000000000000000000..196a6442bd544a3981e6a7de7e923e040cadd32d --- /dev/null +++ b/src/test/resources/regression/verification/xlang/valid/ArrayNested1.scala @@ -0,0 +1,19 @@ +import leon.lang._ + +object ArrayNested1 { + + def test(): Int = { + + var a = Array(1, 2, 0) + + def nested(): Unit = { + require(a.length == 3) + a = a.updated(1, 5) + } + + nested() + a(1) + + } ensuring(_ == 5) + +} diff --git a/src/test/resources/regression/verification/xlang/valid/ArrayNested2.scala b/src/test/resources/regression/verification/xlang/valid/ArrayNested2.scala new file mode 100644 index 0000000000000000000000000000000000000000..fb1a778b8922be1ad8bd5836c5a56740af930374 --- /dev/null +++ b/src/test/resources/regression/verification/xlang/valid/ArrayNested2.scala @@ -0,0 +1,19 @@ +import leon.lang._ + +object ArrayNested2 { + + def test(): Int = { + + var a = Array(1, 2, 0) + + def nested(): Unit = { + require(a.length == 3) + a(2) = 5 + } + + nested() + a(2) + + } ensuring(_ == 5) + +}