[Why3-club] Why3 simplifying too much

Johannes Kanig kanig at adacore.com
Mon Mar 3 10:02:19 CET 2014

Hi Andrei,

On Wed, 12 Feb 2014 17:38:25 +0100, Andrei Paskevich <andrei at lri.fr> wrote:
> 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.

I was confused - we would indeed want to make the distinction you describe:

* no VC when there is no precondition,
* a VC, even if it is simply "true", when there is a precondition, and the call has a "keep_on_simp" tag.

No urgency of course, just wanted to let you know our preference.


Johannes Kanig <kanig at adacore.com>

More information about the Why3-club mailing list