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

[rami3l]

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

[gusthoff]

I just tried the change you proposed locally, and I got the same error as in the figure you attached. I used SPARK Community 2021, which is the version that is currently being used on the learn website:

SPARK Community 2021 (20210519)
Why3 for gnatprove version 1.4.0+git
/opt/Ada/gpl/x86_64-linux/gnat-gpl-2021-x86_64-linux-bin/libexec/spark/bin/alt-ergo: Alt-Ergo version 2.3.0+
/opt/Ada/gpl/x86_64-linux/gnat-gpl-2021-x86_64-linux-bin/libexec/spark/bin/colibri: Colibri 2020.9
/opt/Ada/gpl/x86_64-linux/gnat-gpl-2021-x86_64-linux-bin/libexec/spark/bin/cvc4: This is CVC4 version 1.8
/opt/Ada/gpl/x86_64-linux/gnat-gpl-2021-x86_64-linux-bin/libexec/spark/bin/z3: Z3 version 4.8.10 - 64 bit

Your prover version is more recent. Maybe this plays a role here?

Also, this was the associated main.adc:

pragma Profile(GNAT_Extended_Ravenscar);
pragma Partition_Elaboration_Policy(Sequential);
pragma SPARK_Mode (On);
pragma Warnings (Off, "no Global contract available");
pragma Warnings (Off, "subprogram * has no effect");
pragma Warnings (Off, "file name does not match");