where is the verification condition?

Nov 1, 2011 at 12:27 PM

#include <vcc.h>

int main()

int x=39;

int d=10;

int lq = 0;

int lr = x; 

while (lr >= d) 

_(invariant x == d*lq + lr && x %d ==lr%d  ) 


if(x==39) break ;   


lr =lr- d; 


_( assert lr==39)

return 0;


I think I have  supplied enough information with the invariant , but the assertion 'lr==39' did not verify .Why?

And where can I find the verification condition for the _(assert lr==39)?

Verification condition in my opinion is a formula like    X>5  ==>  X>4  ( we can infer X>4 from X>5) ,


Nov 3, 2011 at 8:21 AM


you can find the generated assertions in the Boogie code, which you can dump using the /t option.

VCC/Z3 is not good with non-linear arithmetic (like the modulo operator), so that may be why VCC is not capable of showing that lr == 39 follows from the loop exit.


Nov 3, 2011 at 12:21 PM

Also your loop invariant does not mention the special case x==39 where lr equals x instead of just being equal modulo d.

As far as I understand (correct me if I'm wrong anybody) the only information VCC has after a loop is the instantiated loop invariant and from that one in deed lr == 39 cannot be deduced. However I do not know how breaking conditions go in there. Any hints?