--- layout: fc_discuss_archives title: Message 53 from Frama-C-discuss on April 2013 ---
> Ok, something really weird is happening. With z3 i'm able to prove everything that i previously was not able. Either the POs always have been correct and WP was limited, or why/z3 is experiencing some strange behavior. I believe it's the latter Don't know what makes sometimes Z3 stringer than alt-ergo, but it can highly depends on the PO structure. You may also play with the -wp-depth option or other alt-ergo options. Viewing goals on altgr-ergo is also interesting. > On a side note related to the new memory model. What implications arise from using the unsafe casts option? Basically, you must verify by hand that unsafe casts are never used to *store* data through a *modification* of aliased memory data layout. For instance : { int * p = ... ; char * q1 = (char *) p ; char * q2 = (char *) p ; if ( q1== q2 ) { .... } // CORRECT if ( *q1 == *q2 ) { .... } // CORRECT q1[2] = 0xFF ; // STILL CORRECT BUT ... if ( *p == ... ) // INCORRECT, because q1 is aliased to internal representation of p ! }