--- layout: fc_discuss_archives title: Message 24 from Frama-C-discuss on February 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] How to make wp to prove the invariant successfully?



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