diff --git a/src/example-archive/should-fail/README.md b/src/example-archive/should-fail/README.md
index 49e793ab..7d639c08 100644
--- a/src/example-archive/should-fail/README.md
+++ b/src/example-archive/should-fail/README.md
@@ -1,2 +1,3 @@
 This folder contains deliberately incorrect proofs, which are intended to serve
-as negative test cases for CN. 
\ No newline at end of file
+as negative test cases for CN, i.e. the ones in `broken` are behaving as
+expected and the ones in `working` show a bug of permissiveness which needs fixing.
diff --git a/src/example-archive/should-fail/working/c_sequencing_race.c b/src/example-archive/should-fail/working/c_sequencing_race.c
new file mode 100644
index 00000000..c91abf15
--- /dev/null
+++ b/src/example-archive/should-fail/working/c_sequencing_race.c
@@ -0,0 +1,10 @@
+
+
+int
+f (int *x)
+/*@ requires take xv = Owned(x); @*/
+/*@ requires 0i32 <= xv && xv < 500i32; @*/
+/*@ ensures take xv2 = Owned(x); @*/
+{
+  return ((*x) + (*x));
+}
diff --git a/src/example-archive/should-fail/working/letweak01.c b/src/example-archive/should-fail/working/letweak01.c
new file mode 100644
index 00000000..be7d7fd6
--- /dev/null
+++ b/src/example-archive/should-fail/working/letweak01.c
@@ -0,0 +1,8 @@
+
+int
+f (int x) {
+  x = (x = 1);
+
+  return x + 2;
+}
+
diff --git a/src/example-archive/simple-examples/broken/error-proof/self_ref_init.c b/src/example-archive/simple-examples/broken/error-proof/self_ref_init.c
new file mode 100644
index 00000000..6195b3c9
--- /dev/null
+++ b/src/example-archive/simple-examples/broken/error-proof/self_ref_init.c
@@ -0,0 +1,19 @@
+
+/* based on a problematic example from linux kvm/pgtable.c */
+
+struct str {
+  int x;
+  int y;
+};
+
+int f (int x)
+/*@ requires (0i32 <= x) && (x < 200i32); @*/
+{
+  struct str str_inst = {
+    .x = x + 2,
+    .y = str_inst.x + 3,
+  };
+
+  return str_inst.y;
+}
+