diff --git a/src/example-archive/c-testsuite/working/00045.working.c b/src/example-archive/c-testsuite/working/00045.working.c
new file mode 100644
index 0000000..85ff652
--- /dev/null
+++ b/src/example-archive/c-testsuite/working/00045.working.c
@@ -0,0 +1,22 @@
+int x = 5;
+long y = 6;
+int *p = &x;
+
+int
+main()
+/*@ accesses x, y, p;
+    requires
+			x == 5i32;
+			y == 6i64;
+			p == &x;
+    ensures return == 0i32; @*/
+{
+	if (x != 5)
+		return 1;
+	if (y != 6)
+		return 2;
+	if (*p != 5)
+		return 3;
+	return 0;
+}
+
diff --git a/src/example-archive/c-testsuite/working/00049.working.c b/src/example-archive/c-testsuite/working/00049.working.c
new file mode 100644
index 0000000..5750145
--- /dev/null
+++ b/src/example-archive/c-testsuite/working/00049.working.c
@@ -0,0 +1,19 @@
+int x = 10;
+
+struct S {int a; int *p;};
+struct S s = { .p = &x, .a = 1};
+
+int
+main()
+/*@ accesses s, x;
+    requires
+			x == 10i32;
+			s.p == &x; s.a == 1i32;
+    ensures return == 0i32; @*/
+{
+	if(s.a != 1)
+		return 1;
+	if(*s.p != 10)
+		return 2;
+	return 0;
+}
diff --git a/src/example-archive/c-testsuite/working/00128.working.c b/src/example-archive/c-testsuite/working/00128.working.c
new file mode 100644
index 0000000..e52950f
--- /dev/null
+++ b/src/example-archive/c-testsuite/working/00128.working.c
@@ -0,0 +1,159 @@
+// TODO: could probably remove some of these requires clauses
+
+int a;
+unsigned b;
+char c;
+signed char d;
+unsigned char e;
+long f;
+unsigned long g;
+long long h;
+unsigned long long i;
+short j;
+unsigned short k;
+
+int
+main(void)
+/*@ accesses a, b, c, d, e, f, g, h, i, j, k;
+
+    requires (i128) MINi32() <= (i128) b; (i128) b <= (i128) MAXi32();
+
+             (i128) MINu8() <= (i128) d; (i128) d <= (i128) MAXu8();
+             (i128) MINu8() <= (i128) f; (i128) f <= (i128) MAXu8();
+             (i128) MINu8() <= (i128) h; (i128) h <= (i128) MAXu8();
+             (i128) MINu8() <= (i128) i; (i128) i <= (i128) MAXu8();
+             (i128) MINu8() <= (i128) j; (i128) j <= (i128) MAXu8();
+
+             (i128) MINi8() <= (i128) e; (i128) e <= (i128) MAXi8();
+             (i128) MINi8() <= (i128) f; (i128) f <= (i128) MAXi8();
+             (i128) MINi8() <= (i128) g; (i128) g <= (i128) MAXi8();
+             (i128) MINi8() <= (i128) h; (i128) h <= (i128) MAXi8();
+             (i128) MINi8() <= (i128) i; (i128) i <= (i128) MAXi8();
+             (i128) MINi8() <= (i128) j; (i128) j <= (i128) MAXi8();
+             (i128) MINi8() <= (i128) k; (i128) k <= (i128) MAXi8();
+
+    ensures return == 0i32; @*/
+{
+	a = b;
+	a = c;
+	a = d;
+	a = e;
+	a = f;
+	a = g;
+	a = h;
+	a = i;
+	a = j;
+	a = k;
+
+	b = a;
+	b = c;
+	b = d;
+	b = e;
+	b = f;
+	b = g;
+	b = h;
+	b = i;
+	b = j;
+	b = k;
+
+	c = a;
+	c = b;
+	c = d;
+	c = e;
+	c = f;
+	c = g;
+	c = h;
+	c = i;
+	c = j;
+	c = k;
+
+	d = a;
+	d = b;
+	d = c;
+	d = e;
+	d = f;
+	d = g;
+	d = h;
+	d = i;
+	d = j;
+	d = k;
+
+	e = a;
+	e = b;
+	e = c;
+	e = d;
+	e = f;
+	e = g;
+	e = h;
+	e = i;
+	e = j;
+	e = k;
+
+	f = a;
+	f = b;
+	f = c;
+	f = d;
+	f = e;
+	f = g;
+	f = h;
+	f = i;
+	f = j;
+	f = k;
+
+	g = a;
+	g = b;
+	g = c;
+	g = d;
+	g = e;
+	g = f;
+	g = h;
+	g = i;
+	g = j;
+	g = k;
+
+	h = a;
+	h = b;
+	h = c;
+	h = d;
+	h = e;
+	h = f;
+	h = g;
+	h = i;
+	h = j;
+	h = k;
+
+	i = a;
+	i = b;
+	i = c;
+	i = d;
+	i = e;
+	i = f;
+	i = g;
+	i = h;
+	i = j;
+	i = k;
+
+	j = a;
+	j = b;
+	j = c;
+	j = d;
+	j = e;
+	j = f;
+	j = g;
+	j = h;
+	j = i;
+	j = k;
+
+	k = a;
+	k = b;
+	k = c;
+	k = d;
+	k = e;
+	k = f;
+	k = g;
+	k = h;
+	k = j;
+	k = i;
+
+	return 0;
+}
diff --git a/src/example-archive/simple-examples/working/write_4.c b/src/example-archive/simple-examples/working/write_4.c
new file mode 100644
index 0000000..4f6eee2
--- /dev/null
+++ b/src/example-archive/simple-examples/working/write_4.c
@@ -0,0 +1,17 @@
+// Write to two static global memory cells
+
+static int *cell1, *cell2;
+void write_4()
+/*@ accesses cell1, cell2;
+    requires
+      take Cell1Pre = Owned<int>(cell1);
+      take Cell2Pre = Owned<int>(cell2);
+    ensures
+      take Cell1Post = Owned<int>(cell1);
+      take Cell2Post = Owned<int>(cell2);
+      Cell1Post == 7i32;
+      Cell2Post == 8i32; @*/
+{
+  *cell1 = 7;
+  *cell2 = 8;
+}