With the last commit, it depends on whether you have "keep_on_simp" on
top of the function call. If it's there, there will be a subgoal for
it. If it's not, there will be none.
A.
On 12 February 2014 18:43, Yannick Moy wrote:
> -- Johannes Kanig (2014-02-12)
>>
>>
>>> your example. There is a ca
-- Johannes Kanig (2014-02-12)
>
>
>> 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
On Wed, 12 Feb 2014 17:38:25 +0100, Andrei Paskevich wrote:
I commited a patch
Thank you very much, Andrei, for this patch and the other one. I will try that
out tomorrow most probably.
your example. There is a catch, however. Internally, Why3 keeps a
single formula for a precondition, not
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
Fixed in git, thanks for the report.
A.
On 11 February 2014 18:36, Johannes Kanig wrote:
> Dear Why3 team,
>
> I get a warning on the following code (with Why3 on git):
>
> module M
> use import "int".Int
> use import "ref".Ref
>
> type vol_rec_t = { rec__x : int }
>
> val vol : ref vol_re
