/* run.config
   EXECNOW: BIN bool.sav LOG bool_sav.res LOG bool_sav.err @frama-c@ -save @PTEST_RESULT@/bool.sav -machdep x86_32 -eva @EVA_OPTIONS@ @PTEST_DIR@/bool.c > @PTEST_RESULT@/bool_sav.res 2> @PTEST_RESULT@/bool_sav.err
   STDOPT: +"-load @PTEST_RESULT@/bool.sav -out -input -deps"
   STDOPT: +"-load @PTEST_RESULT@/bool.sav -eva @EVA_OPTIONS@"
 */

#include "stdbool.h"
#include "stdio.h"

bool x;
int y;

int f() {
  int i, j;

  i = 10;
  /*@ assert (i == 10); */
  while(i--);
  j = 5;

  return 0;
}

int main() {
  f();
  x=false;
  printf("%d\n",x);
  x=2;
  printf("%d\n",x);
  y=x+1;
  printf("%d,%d\n",x,y);
  x=x+1;
  printf("%d\n",x);
  x=x+1;
  printf("%d\n",x);
  return y;
}