Hi Johannes,
I commited a patch that keeps trivially true subgoals during
goal_split if they carry "keep_on_simp", which fixes the problem in
your example. There is a catch, however. Internally, Why3 keeps a
single formula for a precondition, not a list of formulas. That is,
"requires { true }" is the same as no "requires" at all. I can imagine
that you wouldn't want to see a subgoal "true" in your example if f2
didn't have preconditions, which means that you want to distinguish
the two cases. Is that right? It would be a somewhat invasive
modification throughout src/whyml — but that's also something that I
reluctantly wanted to do for other reasons.
Best,
Andrei
On 10 February 2014 17:27, Johannes Kanig <ka...@adacore.com> wrote:
> Recent versions (git) of Why3 seem to be more aggressive in throwing away
> simplified VCs ... On the attached file, the following command generates
> only one VC file in subfolder tmp, while older versions generated two (one
> for each VC, even if trivial):
>
> $ why3 -a split_goal -C why3.conf -P altergo-gp -o tmp test_iterable.mlw
>
> Note the usage of the "keep_on_simp" label.
>
> The previous behavior was that goals with "keep_on_simp" were never
> simplified - that's what we want, we would like to have a VC per goal,
> whether it's trivial or not.
>
> Note that I also don't like that label, and if we find a better solution,
> that would be very welcome.
>
> For example, what *seems* to work right now is to introduce a dummy
> predicate "true_", whose definition is "true" and use that instead of "true"
> everywhere. If that (or something similar) was guaranteed to work and not
> suppress VCs, we could get rid of "keep_on_simp".
>
> What do you think?
>
> --
> Johannes Kanig <ka...@adacore.com>
> _______________________________________________
> Why3-club mailing list
> Why3-club@lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
>
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
