1 files changed, 10 insertions, 0 deletions
diff --git a/test/Feature/EntryPoint.c b/test/Feature/EntryPoint.c
index 8a10d36f..48442659 100644
--- a/test/Feature/EntryPoint.c
+++ b/test/Feature/EntryPoint.c
@@ -3,6 +3,10 @@
 // RUN: %klee --output-dir=%t.klee-out --entry-point=other_main %t.bc | FileCheck -check-prefix=CHECK-OTHER_MAIN %s
 
 // RUN: rm -rf %t.klee-out
+// RUN: %clang -emit-llvm -g -c -DMAIN %s -o %t.bc
+// RUN: %klee --output-dir=%t.klee-out --entry-point=other_main %t.bc | FileCheck -check-prefix=CHECK-OTHER_MAIN %s
+
+// RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --entry-point="" %t.bc 2>%t.stderr.log || echo "Exit status must be 0"
 // RUN: FileCheck -check-prefix=CHECK-EMPTY --input-file=%t.stderr.log %s
 
@@ -14,4 +18,10 @@ int other_main() {
   return 0;
 }
 
+#ifdef MAIN
+int main() {
+  return 0;
+}
+#endif
+
 // CHECK-EMPTY: KLEE: ERROR: entry-point cannot be empty