WHen the input file does not include a main function the clang-fe binary hits a segmentation fault ```bash root@88a2e3099477:/code2inv# ./clang-fe/bin/clang-fe -smt ./example2.c input.cc:18:1: warning: control reaches end of non-void function [-Wreturn-type] } ^ Segmentation fault (core dumped) ``` The following code snippet could be used to reproduce the example ```c int Qmain() { // variable declarations int x; int y; // pre-conditions (x = 1); (y = 0); // loop body while ((y < 100000)) { { (x = (x + y)); (y = (y + 1)); } } // post-condition //assert( (x >= y) ); } ```