The atexit imlementation of the KLEE-libc does not work, when exit is called "explicitely".
Note that at an explicit exit call, the functions registered with atexit ought to be called.

So, the following CHECK does fail when running with the KLEE libc (but it works fine with uclibc).
fwc@aebd8f83 shows the complete test.

void foo() { printf("called foo\n"); }
int main() {
  atexit(foo);
  exit(0);
  // CHECK: called foo          <-- fails
}

The bug occurs since the functions registered via atexit are called by RunAtExit which is marked with __attribute__((destructur)). The destructor is called after exiting main. The "explicit" exit-call is handled by the SpecialFunctionHandler, which directly terminates the state, which thus does not exit main, thus not calling the destructor.