1 files changed, 1 insertions, 1 deletions
diff --git a/test/Feature/AliasFunctionExit.c b/test/Feature/AliasFunctionExit.c
index 4bda950a..acfa4350 100644
--- a/test/Feature/AliasFunctionExit.c
+++ b/test/Feature/AliasFunctionExit.c
@@ -13,7 +13,7 @@ void start(int x) {
     exit(1);
 }
 
-void end(int status) {
+void __attribute__ ((noinline)) end(int status) {
   klee_alias_function("exit", "exit");
   printf("END: status = %d\n", status);
   exit(status);