Sorry for the delay.
On 03/04/2019 11:53, Julia Lawall wrote:
OK, sorry, I don't know. I tried it again just now, and it sent alt-ergo
to both subgoals, the children of the split and the children of thesmoke
detector. Perhaps I misinterpreted what it was doing previously.
Still running smoke detector on the whole project doesn't seem to send the
smoke detector effect to the same place as one gets when doing why3
replay. I've included a small screenshot.
It is not joint to your mail.
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 ?
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
