1 files changed, 30 insertions, 0 deletions
diff --git a/test/Feature/LowerSwitch.c b/test/Feature/LowerSwitch.c
new file mode 100644
index 00000000..c4d9644a
--- /dev/null
+++ b/test/Feature/LowerSwitch.c
@@ -0,0 +1,30 @@
+// RUN: %llvmgcc %s -emit-llvm -g -c -o %t.bc
+// RUN: %klee --exit-on-error --allow-external-sym-calls --switch-type=internal %t.bc
+// RUN: not test -f klee-last/test000010.bout
+// RUN: %klee --exit-on-error --allow-external-sym-calls --switch-type=simple %t.bc
+// RUN: test -f klee-last/test000010.bout
+
+#include <stdio.h>
+
+int main(int argc, char **argv) {
+  int c = klee_range(0, 256, "range");
+  
+  switch(c) {
+  case 0: printf("0\n"); break;
+  case 10: printf("10\n"); break;
+  case 16: printf("16\n"); break;
+  case 17: printf("17\n"); break;
+  case 18: printf("18\n"); break;
+  case 19: printf("19\n"); break;
+#define C(x) case x: case x+1: case x+2: case x+3
+#define C2(x) C(x): C(x+4): C(x+8): C(x+12)
+#define C3(x) C2(x): C2(x+16): C2(x+32): C2(x+48)
+  C3(128):
+    printf("bignums: %d\n", c); break;
+  default: 
+    printf("default\n");
+    break;
+  }
+
+  return 0;
+}