Vanished invariant "expl" attribute
Hello all,
I searched a little bit in the list of issues but did not find any that is relative to my problem.
The problem is that, in some cases "expl" attributes on invariants terms are lost when seeing the associated verifications conditions in the IDE, or when getting them back from the API via Termcode.goal_expl_task
.
For example, in the following code:
module Pb_invariant_attribute
use export ref.Ref
use export bool.Bool
val a : ref bool
val b : ref bool
val c : ref bool
let test ()
diverges
=
while (true)
do
invariant { [@expl:foo] (!a) }
invariant { [@expl:bar] (not (!b)) }
invariant { [@expl:bla] (not (not (!c))) }
done
end
After a split, VCs concerning a
are labelled "Loop invariant init" and "Loop invariant preservation", while the ones concerning b
and c
are respectively labelled "bar" and "bla".