lustrec/optim/clocks7/wp3.script @ 6a93d814
| 1 |
(* Generated by Frama-C WP *) |
|---|---|
| 2 |
|
| 3 |
Goal typed_toto_step_assert_20. |
| 4 |
Hint property,toto_step. |
| 5 |
Proof. |
| 6 |
Require Import Why3. |
| 7 |
intuition. |
| 8 |
repeat (split || exists 0); why3 "Z3". |
| 9 |
Qed. |
| 10 |
|
| 11 |
|