#include<civlc.cvh>
#include<stdio.h>

int main(){
  int x,y,z;

  $havoc(&x);
  printf("x=%d\n", x);
  for(int i=0; i<5; i++){
    $havoc(&y);
    printf("x=%d\n", y);
  }
  $havoc(&z);
}