4 files changed, 95 insertions, 2 deletions
diff --git a/test/Feature/CompressedExprLogging.c b/test/Feature/CompressedExprLogging.c
new file mode 100644
index 00000000..a2a07d8b
--- /dev/null
+++ b/test/Feature/CompressedExprLogging.c
@@ -0,0 +1,42 @@
+// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t1.bc
+// We disable the cex-cache to eliminate nondeterminism across different
+// solvers, in particular when counting the number of queries in the last two
+// commands
+// RUN: rm -rf %t.klee-out %t.klee-out2
+// RUN: %klee --output-dir=%t.klee-out --use-cex-cache=false --use-query-log=all:pc %t1.bc
+// RUN: %klee --output-dir=%t.klee-out2 --use-cex-cache=false --compress-query-log --use-query-log=all:pc %t1.bc
+// RUN: gunzip -d %t.klee-out2/all-queries.pc.gz
+// RUN: diff %t.klee-out/all-queries.pc %t.klee-out/all-queries.pc
+
+#include <assert.h>
+
+int constantArr[16] = {1 << 0,  1 << 1,  1 << 2,  1 << 3, 1 << 4,  1 << 5,
+                       1 << 6,  1 << 7,  1 << 8,  1 << 9, 1 << 10, 1 << 11,
+                       1 << 12, 1 << 13, 1 << 14, 1 << 15};
+
+int main() {
+  char buf[4];
+  klee_make_symbolic(buf, sizeof buf);
+
+  buf[1] = 'a';
+
+  constantArr[klee_range(0, 16, "idx.0")] = buf[0];
+
+  // Use this to trigger an interior update list usage.
+  int y = constantArr[klee_range(0, 16, "idx.1")];
+
+  constantArr[klee_range(0, 16, "idx.2")] = buf[3];
+
+  buf[klee_range(0, 4, "idx.3")] = 0;
+  klee_assume(buf[0] == 'h');
+
+  int x = *((int *)buf);
+  klee_assume(x > 2);
+  klee_assume(x == constantArr[12]);
+
+  klee_assume(y != (1 << 5));
+
+  assert(0);
+
+  return 0;
+}
diff --git a/test/Feature/DeterministicSwitch.c b/test/Feature/DeterministicSwitch.c
new file mode 100644
index 00000000..b6c186ff
--- /dev/null
+++ b/test/Feature/DeterministicSwitch.c
@@ -0,0 +1,38 @@
+// RUN: %llvmgcc %s -emit-llvm -g -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee -debug-print-instructions=all:stderr --output-dir=%t.klee-out --allow-external-sym-calls --switch-type=internal --search=dfs %t.bc >%t.switch.log 2>&1
+// RUN: FileCheck %s -input-file=%t.switch.log -check-prefix=CHECK-DFS
+// RUN: rm -rf %t.klee-out
+// RUN: %klee -debug-print-instructions=all:stderr --output-dir=%t.klee-out --allow-external-sym-calls --switch-type=internal --search=bfs %t.bc >%t.switch.log 2>&1
+// RUN: FileCheck %s -input-file=%t.switch.log -check-prefix=CHECK-BFS
+
+#include "klee/klee.h"
+#include <stdio.h>
+
+int main(int argc, char **argv) {
+  char c;
+
+  klee_make_symbolic(&c, sizeof(c), "index");
+
+  switch (c) {
+  case '\t':
+    printf("tab\n");
+    break;
+  case ' ':
+    printf("space\n");
+    break;
+  default:
+    printf("default\n");
+    break;
+  }
+
+  // CHECK-DFS: default
+  // CHECK-DFS: space
+  // CHECK-DFS: tab
+
+  // CHECK-BFS: tab
+  // CHECK-BFS: space
+  // CHECK-BFS: default
+
+  return 0;
+}
diff --git a/test/Feature/NonSizedGlobals.c b/test/Feature/NonSizedGlobals.c
new file mode 100644
index 00000000..b98f7bf1
--- /dev/null
+++ b/test/Feature/NonSizedGlobals.c
@@ -0,0 +1,12 @@
+// RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc
+
+struct X;
+extern struct X Y;
+void *ptr = &Y;
+
+int main()
+{
+	return 0;
+}
diff --git a/test/regression/2016-04-14-sdiv-2.c_ b/test/regression/2016-04-14-sdiv-2.c
index 88a5fca3..974036ee 100644
--- a/test/regression/2016-04-14-sdiv-2.c_
+++ b/test/regression/2016-04-14-sdiv-2.c
@@ -1,10 +1,11 @@
-// XFAIL: *
 // RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out -exit-on-error -solver-optimize-divides=true %t.bc >%t1.log
 // RUN: grep "m is 2" %t1.log
-
 #include <assert.h>
+#include <stdio.h>
+
+#include "klee/klee.h"
 
 int main(void)
 {