So it seems the anomaly shows up in IDE but not in replay... I'm very confused...
the stack trace coming from IDE is not informative unfortunately Le 01/02/2017 à 14:30, Jean-Jacques Levy a écrit : > File "scc/../scc.mlw", line 249, characters 23-33: > warning: this expression may diverge, which is not stated in the > specification You should add the clause "diverges" in the contracts of your non-terminating functions -- Claude Marché | tel: +33 1 69 15 66 08 INRIA Saclay - Île-de-France | Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ F-91405 ORSAY Cedex | _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr http://lists.gforge.inria.fr/mailman/listinfo/why3-club
