[Frama-C/WP] The history of internal state changes VC goal outcomes
Steps to reproduce the issue
Using Allan Blanchard's answer to exercise 3.1.3.3 (file: code/function-contract/contract/ex-3-alphabet-answer.c)...
Start frama-c-gui code/function-contract/contract/ex-3-alphabet-answer.c.
Right-click on the function prototype int alphabet_letter and select Prove function annotations by WP, the first VC (ensures) should fail.
Right-click on the function prototype int alphabet_letter a second time and select Prove function annotations by WP, the first VC (ensures) should succeed.
Expected behaviour
The order in which WP proof invocations should not change the VC goal outcomes if there is no change to the underlying code/annotations.
Actual behaviour
The history of WP proof invocations does seem to change the VC goal outcomes.
Contextual information
- Frama-C, Why3, Alt-Ergo installation mode: all via Opam
- Frama-C version: 25.0-beta (Manganese)
- Plug-in used: WP
- Why3 version: Why3 platform, version 1.5.0
- Alt-Ergo version: 2.4.1
- OS name: Ubuntu
- OS version: 21.10 (Impish)
- Number of CPU's: 2
- CPU speed: 2.80GHz
- RAM: 16Gb