On 03/04/2019 20:35, Julia Lawall wrote:
The smoke detector is parallel
to the splint in each case, and times out in each case. When I replay
this file with the smoke detector option, I get warnings.
Can you tell us what are the warnings you get ?
Warnings indicating problems. Like:
goal 'move_ready_current_preserves.0.9.0', prover 'Alt-Ergo 2.3.0': result
is: Valid (0.37s, 556 steps) -> Smoke detected!
This warning means that the smoke detector detected that the context of
this goal is self contradicting.
From what I understand, your remark is that the smoke detection from
the why3replay does not result in the same session as the one from the
IDE. Yes, it is the case. Smoke detection was never thought to be
launched from the IDE (even if, to some extent, it can). We'll see if it
is possible to harmonize these two usage in the future.
Thanks for your report.
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
