diff --git a/src/example-archive/c-testsuite/working/00045.working.c b/src/example-archive/c-testsuite/working/00045.working.c
deleted file mode 100644
index cb301ab..0000000
--- a/src/example-archive/c-testsuite/working/00045.working.c
+++ /dev/null
@@ -1,22 +0,0 @@
-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
deleted file mode 100644
index 61ea427..0000000
--- a/src/example-archive/c-testsuite/working/00049.working.c
+++ /dev/null
@@ -1,19 +0,0 @@
-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;
-}
\ No newline at end of file
diff --git a/src/example-archive/c-testsuite/working/00128.working.c b/src/example-archive/c-testsuite/working/00128.working.c
deleted file mode 100644
index 9086f34..0000000
--- a/src/example-archive/c-testsuite/working/00128.working.c
+++ /dev/null
@@ -1,159 +0,0 @@
-// 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(); @*/
-
-/*@ requires (i128) MINu8() <= (i128) d; (i128) d <= (i128) MAXu8(); @*/
-/*@ requires (i128) MINu8() <= (i128) f; (i128) f <= (i128) MAXu8(); @*/
-/*@ requires (i128) MINu8() <= (i128) h; (i128) h <= (i128) MAXu8(); @*/
-/*@ requires (i128) MINu8() <= (i128) i; (i128) i <= (i128) MAXu8(); @*/
-/*@ requires (i128) MINu8() <= (i128) j; (i128) j <= (i128) MAXu8(); @*/
-
-/*@ requires (i128) MINi8() <= (i128) e; (i128) e <= (i128) MAXi8(); @*/
-/*@ requires (i128) MINi8() <= (i128) f; (i128) f <= (i128) MAXi8(); @*/
-/*@ requires (i128) MINi8() <= (i128) g; (i128) g <= (i128) MAXi8(); @*/
-/*@ requires (i128) MINi8() <= (i128) h; (i128) h <= (i128) MAXi8(); @*/
-/*@ requires (i128) MINi8() <= (i128) i; (i128) i <= (i128) MAXi8(); @*/
-/*@ requires (i128) MINi8() <= (i128) j; (i128) j <= (i128) MAXi8(); @*/
-/*@ requires (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
deleted file mode 100644
index 7275151..0000000
--- a/src/example-archive/simple-examples/working/write_4.c
+++ /dev/null
@@ -1,17 +0,0 @@
-// 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;
-}