/* Generated by Goblint-CIL v. 2.0.6-15-gfaeb7be */
/* print_CIL_Input is true */

#line 1 "cilcode.tmp/ex13.c"
int x  =    5;
#line 2 "cilcode.tmp/ex13.c"
int main(void) 
{ 
  int x___0 ;
  int x___1 ;

  {
#line 3
  x___0 = 6;
#line 5
  x___1 = 7;
#line 6
  return (x___1);
#line 8
  return (x___0);
}
}