--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on June 2014 ---
Probably one more instance of Alt-Ergo case splitting strategy, which is obfuscated by the large constants introduced by int32 / int64 boundaries. This is a known issue with Alt-Ergo. The -wp-split option explicitly introduces more case splits before sending proof obligations to the provers. L. Le 2 juin 2014 ? 08:53, David MENTRE <dmentre at linux-france.org> a ?crit : > Hello, > > Le 27/05/2014 10:36, Christophe Garion a ?crit : >> I have some code that was proved with the Fluorine version of Frama-C >> and is no more proved using Neon. A simplified version of the code is >> available in the test_po_time_double_behavior_1.c file. > > Everything is proved with -wp-split. Don't ask me why :-) (even if I think you are on the border line of what Alt-Ergo can prove). > > Command line used: > frama-c-gui -pp-annot -wp-timeout 60 -wp -wp-split test_po_time_double_behavior_1.c > > > Best regards, > david > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss