Le 16/05/2019 à 14:48, Guillaume Melquiond a écrit :
Le 16/05/2019 à 13:38, Jean-Jacques Levy a écrit :
1- assertions around ‘if-statement’ keep the conditional in the logic.
In previous 0.88.3, they were splitted around the two branches of the
if-statement. Now the provers have to go through the predicate of the
if-statement. In command-line, I tried to use a ‘case’ command, but
did not seem to help the provers. Same with various ‘split’.. I miss a
‘simplify’ command which would normalize (ie erase) the condition in
the two branches?
I cannot think of a good solution. I would have thought that
"eliminate_if" would do the trick, but the formula it produces is not
suitable for splitting. (It is basically the same formula as the one
obtained by "split_all_full".)
After discussing with Andrei, it appears that the "case_split" attribute
might help. Assuming that the structure of your code is similar to the
following one
```
let f (b:bool) (x:int)
ensures { x = 3 }
=
assert { [@case_split] if b then x = 1 else x = 2 };
()
```
then calling "split_vc" twice produces two goals, the first one being
```
axiom H1 : b = True
axiom H : x = 1
goal VC f : x = 3
```
Best regards,
Guillaume
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
