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

[rami3l]

In Courses.Intro_To_Spark.Proof_of_Functional_Correctness.Loop_Invariant_4 (the example just above pitfalls):

Adding a Loop_Invariant (L13-L14) seems to have changed nothing:

... however everything works quite well locally with the same command:

> 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 ...
show_map.adb:10:18: info: overflow check proved
show_map.adb:10:18: info: index check proved
show_map.adb:13:13: info: loop invariant preservation proved
show_map.adb:13:13: info: loop invariant initialization proved
show_map.adb:14:41: info: overflow check proved
show_map.adb:14:41: info: index check proved
show_map.adb:14:65: info: index check proved
show_map.adb:16:13: info: loop invariant initialization proved
show_map.adb:16:13: info: loop invariant preservation proved
show_map.adb:16:44: info: index check proved
show_map.adb:16:63: info: index check proved
show_map.adb:18:22: info: assertion proved
show_map.adb:19:50: info: overflow check proved
show_map.adb:19:50: info: index check proved
show_map.adb:19:65: info: index check proved
show_map.ads:8:35: info: overflow check proved
Summary logged in Courses.Intro_To_Spark.Proof_of_Functional_Correctness.Loop_Invariant_4/gnatprove/gnatprove.out

> 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]

Thanks for reporting!

(The issue was previously reported in #581. Fixing it requires enhancements to website infrastructure.)