diff --git a/sledge/test/analyze/FA_dynamic_size_array.c b/sledge/test/analyze/FA_dynamic_size_array.c
new file mode 100644
index 000000000..46160f804
--- /dev/null
+++ b/sledge/test/analyze/FA_dynamic_size_array.c
@@ -0,0 +1,20 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+void main() {
+  size_t n = __llair_choice();
+  n = (n < 0 ? -n : n) + 1;
+  int* a = __llair_alloc(n * sizeof(int));
+
+  for (int i = 0; i < n; i++) {
+    a[i] = i;
+  }
+
+  free(a);
+
+  return;
+}
diff --git a/sledge/test/analyze/FA_mallctl_thread_allocatedp.cpp b/sledge/test/analyze/FA_mallctl_thread_allocatedp.cpp
new file mode 100644
index 000000000..61ed3b4b6
--- /dev/null
+++ b/sledge/test/analyze/FA_mallctl_thread_allocatedp.cpp
@@ -0,0 +1,32 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+#include <cstddef>
+#include <cstdint>
+
+extern "C" int mallctl(const char* name, void* oldp, size_t* oldlenp,
+                       void* newp, size_t newlen) __attribute__((__weak__));
+
+int main() {
+  volatile uint64_t* counter;
+  size_t counterLen = sizeof(uint64_t*);
+
+  if (mallctl("thread.allocatedp", static_cast<void*>(&counter), &counterLen,
+              nullptr, 0) != 0) {
+    return 1;
+  }
+
+  if (counterLen != sizeof(uint64_t*)) {
+    return 1;
+  }
+
+  // false alarm: the spec of mallctl does not special case
+  // thread.allocatedp and set counter to a valid pointer
+  uint64_t origAllocated = *counter;
+
+  return 0;
+}
diff --git a/sledge/test/analyze/FN_ptr_arith_bad.cpp b/sledge/test/analyze/FN_ptr_arith_bad.cpp
new file mode 100644
index 000000000..2c8762a34
--- /dev/null
+++ b/sledge/test/analyze/FN_ptr_arith_bad.cpp
@@ -0,0 +1,16 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+int main() {
+  auto x = new int[8];
+  auto y = new int[8];
+  y[0] = 42;
+  auto x_ptr = x + 8; // one past the end
+  if (x_ptr == &y[0]) // valid
+    *x_ptr = 23;      // UB
+  return y[0];
+}
diff --git a/sledge/test/analyze/addr_of_global_struct.c b/sledge/test/analyze/addr_of_global_struct.c
new file mode 100644
index 000000000..1521e6043
--- /dev/null
+++ b/sledge/test/analyze/addr_of_global_struct.c
@@ -0,0 +1,25 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+typedef struct _ {
+  int x;
+  int y;
+} S;
+
+S s;
+
+void main() {
+  int x, y, z;
+  S* p;
+
+  x = (&s)->x;
+  p = &s;
+  y = p->x;
+  z = s.x;
+
+  return;
+}
diff --git a/sledge/test/analyze/address_arith.c b/sledge/test/analyze/address_arith.c
new file mode 100644
index 000000000..eaaa40c1b
--- /dev/null
+++ b/sledge/test/analyze/address_arith.c
@@ -0,0 +1,22 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+typedef struct _ {
+  int* f;
+  int* g;
+} S;
+
+void main() {
+  S x;
+  int** p;
+  int y;
+
+  /* safe */
+  x.f = &y;
+  p = &x.f;
+  p++;
+}
diff --git a/sledge/test/analyze/address_arith_unsafe.c b/sledge/test/analyze/address_arith_unsafe.c
new file mode 100644
index 000000000..677260aa3
--- /dev/null
+++ b/sledge/test/analyze/address_arith_unsafe.c
@@ -0,0 +1,25 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+typedef struct _ {
+  int* f;
+  int* g;
+} S;
+
+void main() {
+  S x;
+  int** p;
+  int y;
+
+  /* safe */
+  x.f = &y;
+  p = &x.f;
+  p++;
+  /* unsafe */
+  *p = 0;
+  *x.g = 0;
+}
diff --git a/sledge/test/analyze/arithmetic.c b/sledge/test/analyze/arithmetic.c
index 86a6cb5da..2b4eb2dbb 100644
--- a/sledge/test/analyze/arithmetic.c
+++ b/sledge/test/analyze/arithmetic.c
@@ -9,6 +9,7 @@ float f(int x, float y) { // 8, 3.0
   int z = x * x;          // 64
   return y + z;           // 67.0
 }
+
 int g(int y) { // 8
   if (y) {
     return 1;
diff --git a/sledge/test/analyze/arithmetic_loop.c b/sledge/test/analyze/arithmetic_loop.c
index ddbb10643..b3728c23a 100644
--- a/sledge/test/analyze/arithmetic_loop.c
+++ b/sledge/test/analyze/arithmetic_loop.c
@@ -5,17 +5,16 @@
  * LICENSE file in the root directory of this source tree.
  */
 
-#include <stdlib.h> // for exit
-
 int f(int x);
 int g(int x);
 
 int f(int x) { // x= 0, 1, 2, ...
   return g(x + 2);
 }
+
 int g(int y) { // y= 2, 3, 4, ...
-  if (y > 5) { // catch this crash only when depth bound > 2
-    exit(42);
+  if (y > 5) {
+    return y;
   }
   return f(y - 1); // Back edge!
 }
diff --git a/sledge/test/analyze/arithmetic_loop_unsafe.c b/sledge/test/analyze/arithmetic_loop_unsafe.c
new file mode 100644
index 000000000..59cf0a4f8
--- /dev/null
+++ b/sledge/test/analyze/arithmetic_loop_unsafe.c
@@ -0,0 +1,25 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+int f(int x);
+int g(int x);
+
+int f(int x) { // x= 0, 1, 2, ...
+  return g(x + 2);
+}
+
+int g(int y) { // y= 2, 3, 4, ...
+  if (y > 5) { // catch this crash only when depth bound >= 4
+    abort();
+  }
+  return f(y - 1); // Back edge!
+}
+
+int main() {
+  f(0);
+  return 0;
+}
diff --git a/sledge/test/analyze/array_access.c b/sledge/test/analyze/array_access.c
new file mode 100644
index 000000000..49064dae9
--- /dev/null
+++ b/sledge/test/analyze/array_access.c
@@ -0,0 +1,18 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+int x;
+
+void main() {
+  int n = 4;
+  int* A = (int*)__llair_alloc(n * sizeof(int));
+  /* safe */
+  x = A[0];
+  x = A[1];
+  x = A[2];
+  x = A[3];
+}
diff --git a/sledge/test/analyze/array_access_unsafe.c b/sledge/test/analyze/array_access_unsafe.c
new file mode 100644
index 000000000..54698b61d
--- /dev/null
+++ b/sledge/test/analyze/array_access_unsafe.c
@@ -0,0 +1,21 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+int x;
+
+void main() {
+  int n = 4;
+  int* A = (int*)__llair_alloc(n * sizeof(int));
+  /* safe */
+  x = A[0];
+  x = A[1];
+  x = A[2];
+  x = A[3];
+  /* unsafe */
+  x = A[-2];
+  x = A[n + 2];
+}
diff --git a/sledge/test/analyze/bool_to_int.c b/sledge/test/analyze/bool_to_int.c
new file mode 100644
index 000000000..59ebd6c88
--- /dev/null
+++ b/sledge/test/analyze/bool_to_int.c
@@ -0,0 +1,17 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+#include <assert.h>
+
+int main() {
+  int two;
+  int equals_two;
+  two = 2;
+  equals_two = (two == 2);
+  assert((equals_two != 0));
+  assert((equals_two == 1));
+}
diff --git a/sledge/test/analyze/copy_struct_on_stack.c b/sledge/test/analyze/copy_struct_on_stack.c
new file mode 100644
index 000000000..3db979fae
--- /dev/null
+++ b/sledge/test/analyze/copy_struct_on_stack.c
@@ -0,0 +1,19 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+typedef struct _ {
+  int i;
+  int j;
+  char c;
+} S;
+
+void main() {
+  S x = {1, 2, '3'};
+  S y = {4, 5, '6'};
+
+  x = y;
+}
diff --git a/sledge/test/analyze/free_free.c b/sledge/test/analyze/free_free.c
new file mode 100644
index 000000000..1ac73fa3d
--- /dev/null
+++ b/sledge/test/analyze/free_free.c
@@ -0,0 +1,12 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+int main() {
+  int* p = (int*)malloc(sizeof(int));
+  free(p);
+  free(p);
+}
diff --git a/sledge/test/analyze/free_local.c b/sledge/test/analyze/free_local.c
new file mode 100644
index 000000000..6a069ed2b
--- /dev/null
+++ b/sledge/test/analyze/free_local.c
@@ -0,0 +1,11 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+int main() {
+  int i;
+  free(&i);
+}
diff --git a/sledge/test/analyze/global_vars.c b/sledge/test/analyze/global_vars.c
index ba5211ff5..85ce0abd2 100644
--- a/sledge/test/analyze/global_vars.c
+++ b/sledge/test/analyze/global_vars.c
@@ -5,24 +5,13 @@
  * LICENSE file in the root directory of this source tree.
  */
 
-/* The symbolic heap for this example should look like:
-  ^ %.str --> <13,{}> * %c1 --> <8,%.str> * %retval --> <4,0>
-  instead of
-      ^ %.str --> <13,{}>
-      * %a_string --> <8,%.str>
-      * %an_int --> <4,0>
-      * %c1 --> <8,%.str>
-      * %retval --> <4,0>
-  Which has an_int and a_string indirections. There can be obtained by
-  sledge.dbg llvm analyze -trace Domain.call global_vars.bc */
-
 const char* a_string = "I'm a string";
 int an_int = 0;
 
-int c() { return an_int; }
+int idx() { return an_int; }
 
 int main() {
-  const char* c1 = a_string;
+  const char* str = a_string;
 
-  return c();
+  return str[idx()];
 }
diff --git a/sledge/test/analyze/int_bool_assign.c b/sledge/test/analyze/int_bool_assign.c
new file mode 100644
index 000000000..7952fac43
--- /dev/null
+++ b/sledge/test/analyze/int_bool_assign.c
@@ -0,0 +1,23 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+int main() {
+  int c = __llair_choice() % 5;
+  int* p;
+
+  if (c) {
+    p = (int*)malloc(sizeof(int));
+  }
+  for (int i = 0; i < 4; i++) {
+    c += (__llair_choice() % 3);
+  }
+  if (c) {
+    *p = 0;
+    free(p);
+  }
+  return 0;
+}
diff --git a/sledge/test/analyze/irreducible.c b/sledge/test/analyze/irreducible.c
new file mode 100644
index 000000000..6a6f4c226
--- /dev/null
+++ b/sledge/test/analyze/irreducible.c
@@ -0,0 +1,26 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+void main() {
+  int x, y;
+
+  x++;
+  if (x / 2) {
+  L0:
+    if (x <= 0)
+      goto L3;
+    x--;
+    goto L1;
+  } else {
+  L1:
+    y++;
+    goto L0;
+  }
+L3:
+
+  return;
+}
diff --git a/sledge/test/analyze/loop.c b/sledge/test/analyze/loop.c
new file mode 100644
index 000000000..55708e7ff
--- /dev/null
+++ b/sledge/test/analyze/loop.c
@@ -0,0 +1,15 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+int main() {
+  int n = 0;
+  int b = __llair_choice();
+  for (int i = 0; i < b; i++) {
+    n += i;
+  }
+  return n;
+}
diff --git a/sledge/test/analyze/nested_loop_branch.c b/sledge/test/analyze/nested_loop_branch.c
new file mode 100644
index 000000000..0b8b45368
--- /dev/null
+++ b/sledge/test/analyze/nested_loop_branch.c
@@ -0,0 +1,23 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+int main() {
+  int x = 0;
+  while (__llair_choice()) {
+    x += 1;
+    while (__llair_choice()) {
+      x += 3;
+      if (__llair_choice()) {
+        x += 5;
+      } else {
+        x += 7;
+      }
+      x += 9;
+    }
+  }
+  return x;
+}
diff --git a/sledge/test/analyze/nested_loop_branch_break.c b/sledge/test/analyze/nested_loop_branch_break.c
new file mode 100644
index 000000000..4332dd982
--- /dev/null
+++ b/sledge/test/analyze/nested_loop_branch_break.c
@@ -0,0 +1,24 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+int main() {
+  int x = 0;
+  while (__llair_choice()) {
+    x += 1;
+    while (__llair_choice()) {
+      x += 3;
+      if (__llair_choice()) {
+        x += 5;
+      } else {
+        x += 7;
+      }
+      if (__llair_choice())
+        break;
+    }
+  }
+  return x;
+}
diff --git a/sledge/test/analyze/nonreducible_call_graph.c b/sledge/test/analyze/nonreducible_call_graph.c
index b64dbf504..24e567f07 100644
--- a/sledge/test/analyze/nonreducible_call_graph.c
+++ b/sledge/test/analyze/nonreducible_call_graph.c
@@ -4,33 +4,32 @@
  * This source code is licensed under the MIT license found in the
  * LICENSE file in the root directory of this source tree.
  */
-#include <stdio.h>
 
 char* a = "I'm a string";
 char* b = "I'm a different string";
 char* c = "foo bar";
 char* d = "hello world";
-FILE* file;
 
 void f();
 void g();
 
-int main() {        // accesses: a,b,c,d
-  if (getc(file)) { // nondeterministic
-    f();
-  } else {
-    g();
-  }
-  char* s = a;
-  return 0;
-}
-
 void f() { // accesses: b, c, d
   char* s1 = b;
   g();
   char* s2 = c;
 }
+
 void g() { // accesses: b, c, d
   char* s = d;
   f();
 }
+
+int main() { // accesses: a,b,c,d
+  if (__llair_choice()) {
+    f();
+  } else {
+    g();
+  }
+  char* s = a;
+  return 0;
+}
diff --git a/sledge/test/analyze/range_for.cpp b/sledge/test/analyze/range_for.cpp
new file mode 100644
index 000000000..d44adb009
--- /dev/null
+++ b/sledge/test/analyze/range_for.cpp
@@ -0,0 +1,22 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+#include <memory>
+#include <vector>
+
+std::shared_ptr<std::vector<int>> get() {
+  std::vector<int> v = {1, 2, 3};
+  return std::make_shared<std::vector<int>>(v);
+}
+
+int main() {
+  int n;
+  for (auto& t : *get()) {
+    n += t;
+  }
+  return n;
+}
diff --git a/sledge/test/analyze/recursion.c b/sledge/test/analyze/recursion.c
index 3195b2fd5..602764da2 100644
--- a/sledge/test/analyze/recursion.c
+++ b/sledge/test/analyze/recursion.c
@@ -5,12 +5,11 @@
  * LICENSE file in the root directory of this source tree.
  */
 
-/* Simple mutual recursion. Sledge should respect execution
- * bounds and terminate quickly for small bounds */
 void mutal_rec_d();
 void mutal_rec_a() { mutal_rec_d(); }
 void mutal_rec_d() { mutal_rec_a(); }
 void recurse() { recurse(); }
+
 int main() {
   recurse();
   mutal_rec_a();
diff --git a/sledge/test/analyze/struct_array_copy.c b/sledge/test/analyze/struct_array_copy.c
new file mode 100644
index 000000000..8c964fb63
--- /dev/null
+++ b/sledge/test/analyze/struct_array_copy.c
@@ -0,0 +1,17 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+typedef struct _ {
+  int x;
+  int a[30];
+} S;
+
+int main() {
+  S s;
+  s = s;
+  return s.x;
+}
diff --git a/sledge/test/analyze/uad.cpp b/sledge/test/analyze/uad.cpp
new file mode 100644
index 000000000..3bae39bdf
--- /dev/null
+++ b/sledge/test/analyze/uad.cpp
@@ -0,0 +1,40 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+struct B {
+  void foo() {}
+  ~B() {
+    if (!i_) {
+      foo();
+    }
+  }
+  int i_;
+};
+
+struct A {
+  ~A() {
+    if (b_) {
+      b_->foo();
+    }
+  }
+
+  B* b_{nullptr};
+};
+
+struct S {
+  S() { a.b_ = &b; }
+
+  A a;
+  B b;
+};
+
+int main(int argc, char* argv[]) {
+  S s;
+  return 0;
+}
+
+int _llair_main() { return main(0, nullptr); }
diff --git a/sledge/test/analyze/wrap_malloc.c b/sledge/test/analyze/wrap_malloc.c
index fe059e5c4..73e650277 100644
--- a/sledge/test/analyze/wrap_malloc.c
+++ b/sledge/test/analyze/wrap_malloc.c
@@ -8,6 +8,7 @@
 #include <stdlib.h>
 
 char* c() { return malloc(12); }
+
 int main() {
   char* s = c();
   return s ? *s : 1;