// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t2.bc
// RUN: %klee --libc=klee %t2.bc > %t3.log
// RUN: echo "good" > %t3.good
// RUN: diff %t3.log %t3.good

int main() {
  char buf[4];
  char *s = "foo";

  klee_make_symbolic(buf, sizeof buf);
  buf[3] = 0;

  if (strcmp(buf, s)==0) {
    if (buf[0]=='f' && buf[1]=='o' && buf[2]=='o' && buf[3]==0) {
      printf("good\n");
    } else {
      printf("bad\n");
    }
  }
  
  return 0;
}