[Bug] Incorrect online execution result in SPARK tutorial (2/2)

Comienza con Example_08 en Courses.Intro_To_Spark.Proof_of_Functional_Correctness y compara el playground en línea con la ejecución local de array_util.adb después de mover L7-L8. Ejecuta el comando gnatprove indicado e inspecciona la salida del playground; se considera terminado cuando los resultados en línea y locales identifican de forma coherente el error semántico.

In Courses.Intro_To_Spark.Proof_of_Functional_Correctness.Example_08:

I tried moving L7-L8 in array_util.adb to the end of if-else which should be an obvious semantic error to be fixed.

However, the online playground complains:

Local execution, on the other hand, completes without any problem:

> gnatprove -P main.gpr --checks-as-errors --level=0 --no-axiom-guard --report=all
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...

main.adb:6:30: warning: array aggregate using () is an obsolescent syntax, use [] instead [-gnatwj]
    6 |   A : constant Nat_Array := (1, 1, 2);
      |                             ^~~~~~~~

main.adb:7:30: warning: array aggregate using () is an obsolescent syntax, use [] instead [-gnatwj]
    7 |   B : constant Nat_Array := (2, 1, 0);
      |                             ^~~~~~~~

main.adb:8:04: warning: constant "R" is not referenced [-gnatwu]
    8 |   R : constant Nat_Array (1..3) := Max_Array (A, B);
      |   ^ here
array_util.adb:6:07: info: range check proved
array_util.adb:6:34: info: length check proved
array_util.adb:10:24: info: index check proved
array_util.adb:13:25: info: index check proved
array_util.adb:15:33: info: loop invariant preservation proved
array_util.adb:15:33: info: loop invariant initialization proved
array_util.adb:16:40: info: index check proved
array_util.adb:16:61: info: index check proved
array_util.adb:16:68: info: index check proved
array_util.ads:9:14: info: postcondition proved
array_util.ads:10:34: info: index check proved
array_util.ads:10:55: info: index check proved
array_util.ads:10:62: info: index check proved

> gnatprove --version
SPARK Pro 23.0w (20220412)
Why3 for gnatprove version 1.4.1+git
alt-ergo: Alt-Ergo version 2.4.0
colibri: Colibri 2020.9
cvc4: This is CVC4 version 1.8
z3: Z3 version 4.8.15 - 64 bit