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

int main(){
  int x;

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