Taking the first model element matching an id and a loc is inaccurate
This ticket comes from investigating a "bad counterexample" classification on a simple test file in SPARK: main.adb
This SPARK test contains on a single line X := 0; SetX(2);
. The model returned by the prover contains two different values for X
at this line: X = 0
for the first part, and X = 4
for the second part which is a "good" value to show the assertion failure (since X = 4
satisfies the postcondition of SetX
).
But the giant-step RAC takes the value X = 0
when trying to evaluate the postcondition of SetX
.
This problem does not happen if the affectation and the call to SetX
are split in 2 different lines.
The bug seems to come from Model_parser.search_model_element_for_id
, which assumes that an id and a loc are enough to find the correct value for the oracle.
I have minimized the .mlw
generated by SPARK to reproduce the above problem with Why3:
- reproducer file: same_loc.mlw
- Why3 command:
why3 prove -P "CVC5,1.0.0,counterexamples" --check-ce --rac-prover="CVC5,1.0.0" ~/Work/WIP/same_loc.mlw --debug=vc_sp
This is not urgent for SPARK since there is a workaround (splitting in different lines). @marche it reminds me of what we discussed this week about filtering duplicated elements in models, so I guess it is worth having a look at it.