Hello,
If you're using Why3's development version, there was a bug in session
reloading in Why3's master branch for a few weeks that had the effects
you mention. It was fixed a few days ago by commit 9f03b008
<https://gitlab.inria.fr/why3/why3/-/commit/9f03b008cf02091fec21c19d49145ee2b36c80e3>.
Hope this helps,
Raphaël
On 17/03/2020 09:31, Julia Lawall wrote:
Hello,
I wonder if there is some easy room for improvement in the process of
reloading a session when things have changed. For example, I have at
least the illusion that when I remove a lemma at the end of a large module
and then reload it, the proofs don't all end up in the right places.
For example, I may get a "index in array bounds" associated with an
inline_goal or a formula where the main operator is /\ that is put with an
inline_goal, when it is actually only provable with a split.
Are proofs at least associated with the kind of goal they are being used
for? It's unlikely that a formula would switch from being eg a
precondition to a postcondition.
thanks,
julia
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
