On Thu, 26 Mar 2020, Guillaume Melquiond wrote:
> Le 26/03/2020 à 13:08, Julia Lawall a écrit :
>
> > Are there any other possibilities, or other ways to solve the problem of
> > finding useless asserts?
>
> I don't have any good solution. But here are a few ideas that might make
> it easier for you.
>
> Rather than removing the assertions, make them trivial (e.g., "false ->
> ..."). That way, you can reuse your old session without much trouble, as
> the proof tree should then be mostly the same as before. (It mostly
> depends on the transformations you have applied to the assertions
> themselves. If none, it should be identical.)
>
> I also suggest that you delete why3shapes.gz before running why3replay
> or why3ide on your new sources to force a trivial reassociation.
>
> A completely different approach would be to run a bisection in why3ide
> on some goals you consider heavily dependent on assertions. Then take a
> look at the hypotheses Why3 has flagged as useless. It should give some
> clues on which assertions can be safely removed.
Thanks! Bisect is indeed something that I have not yet tried.
julia
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
