diff --git a/regression/cbmc-concurrency/global_pointer1/main.c b/regression/cbmc-concurrency/global_pointer1/main.c
new file mode 100644
index 00000000000..604e94f181a
--- /dev/null
+++ b/regression/cbmc-concurrency/global_pointer1/main.c
@@ -0,0 +1,33 @@
+#include <pthread.h>
+#include <assert.h>
+
+int *v;
+int g;
+
+void *thread1(void * arg)
+{
+  v = &g;
+}
+
+void *thread2(void *arg)
+{
+  assert(v == &g);
+  *v = 1;
+}
+
+int main()
+{
+  pthread_t t1, t2;
+
+  pthread_create(&t1, 0, thread1, 0);
+  pthread_join(t1, 0);
+
+  pthread_create(&t2, 0, thread2, 0);
+  pthread_join(t2, 0);
+
+  assert(v == &g);
+  assert(*v == 1);
+
+  return 0;
+}
+
diff --git a/regression/cbmc-concurrency/global_pointer1/test.desc b/regression/cbmc-concurrency/global_pointer1/test.desc
new file mode 100644
index 00000000000..52168c7eba4
--- /dev/null
+++ b/regression/cbmc-concurrency/global_pointer1/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-concurrency/stack1/main.c b/regression/cbmc-concurrency/stack1/main.c
new file mode 100644
index 00000000000..b4fcad2afaa
--- /dev/null
+++ b/regression/cbmc-concurrency/stack1/main.c
@@ -0,0 +1,23 @@
+#include <pthread.h>
+#include <assert.h>
+
+void *thread(void *arg)
+{
+  int *i = (int *)arg;
+  *i = 1;
+}
+
+int main(void)
+{
+  int x;
+  x = 0;
+
+  pthread_t t;
+
+  pthread_create(&t, NULL, thread, &x);
+  pthread_join(t, NULL);
+
+  assert(x == 1);
+
+  return 0;
+}
diff --git a/regression/cbmc-concurrency/stack1/test.desc b/regression/cbmc-concurrency/stack1/test.desc
new file mode 100644
index 00000000000..52168c7eba4
--- /dev/null
+++ b/regression/cbmc-concurrency/stack1/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-concurrency/struct_and_array1/main.c b/regression/cbmc-concurrency/struct_and_array1/main.c
index 42164904232..fdc909d823b 100644
--- a/regression/cbmc-concurrency/struct_and_array1/main.c
+++ b/regression/cbmc-concurrency/struct_and_array1/main.c
@@ -22,7 +22,7 @@ void *foo1(void *arg1)
 void *foo2(void *arg2)
 {
   st.y = 1;
-  my_array[2]=2;
+  my_array[2]=1;
   done2 = 1;
 }