--- layout: fc_discuss_archives title: Message 24 from Frama-C-discuss on February 2012 ---
Le 7 f?vr. 12 ? 14:26, Henry a ?crit : > Yes, I don't understand the \forall quantifier properly. It is the standard logical quantifier. > But if the invariant is changed to be 0 <= x <= (z+1.0), then the > status is unknown. Is the type of the constant very important? Which > type it should be if the type of x and z is different? By using 1.0 instead of 1, your specification is promoted to real world, where SMT solvers are far less efficient than in integer world. Similar to using C-float 1.0 instead of C-int 1. L. > Henry > _______________________________________________ > 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