int a;

/*@
  assigns a;
  ensures a = 3;
*/
void foo()
{
    a = 3;
}