diff --git a/regression/goto-instrument/slice01/main.c b/regression/goto-instrument/slice01/main.c
new file mode 100644
index 00000000000..7502ff7413a
--- /dev/null
+++ b/regression/goto-instrument/slice01/main.c
@@ -0,0 +1,70 @@
+#include <stdio.h>
+#include <stdlib.h>
+#include <assert.h>
+
+typedef struct list 
+{
+  int key;
+  struct list *next;
+} mlist;
+
+mlist *head;
+
+mlist* search_list(mlist *l, int k)
+{
+  l = head;
+  while(l!=NULL && l->key!=k)
+  {
+    l = l->next;
+  }
+  return l;
+}
+
+int delete_list(mlist *l)
+{
+  mlist *tmp;
+  tmp = head;
+  if (head != l)
+  {
+    while(tmp->next!=l)
+      tmp = tmp->next;
+      tmp->next = l->next;
+  }
+  else
+  {
+    head = l->next;
+  }
+  free(l);
+  return 0;
+}
+
+int insert_list(mlist *l, int k)
+{
+  l = (mlist*)malloc(sizeof(mlist));
+  if (head==NULL)
+  {
+    l->key = k;
+    l->next = NULL;
+  }
+  else
+  {
+    l->key = k;
+    l->next = head;
+  }
+  head = l;
+  return 0;
+}
+
+int main(void)
+{
+  int i;
+  mlist *mylist, *temp;
+  insert_list(mylist,2);
+  insert_list(mylist,5);
+  insert_list(mylist,1);
+  insert_list(mylist,3);
+  mylist = head;
+  temp = search_list(mylist,2);
+  assert(temp->key == 2);
+  delete_list(temp);
+}
diff --git a/regression/goto-instrument/slice01/test.desc b/regression/goto-instrument/slice01/test.desc
new file mode 100644
index 00000000000..76cbcfa81bd
--- /dev/null
+++ b/regression/goto-instrument/slice01/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+--unwind 2 --full-slice
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/goto-instrument/slice02/main.c b/regression/goto-instrument/slice02/main.c
new file mode 100644
index 00000000000..8c7aa38de2c
--- /dev/null
+++ b/regression/goto-instrument/slice02/main.c
@@ -0,0 +1,73 @@
+#include <stdio.h>
+
+#define TRUE	(1)
+#define FALSE	(0) 
+#define SIZE	(10)
+int topo=0;
+
+void inc_topo(void){
+	topo++;
+}
+
+void dec_topo(void){
+	topo--;
+}
+
+int get_topo(void){
+	return topo;
+}
+
+int stack_empty(void){
+	(topo==0) ? TRUE : FALSE; 
+}
+
+int push(int *stack, int x){
+	if (topo==SIZE) {
+		printf("stack overflow\n");
+		return -1;
+	} else {
+		stack[get_topo()] = x;
+		printf("push: stack[%d] = %d\n", get_topo(), stack[get_topo()]);
+		inc_topo();
+	}
+}
+
+int pop(int *stack){
+	if (get_topo()==0) {
+		printf("stack underflow\n");	
+		return -1;
+	} else {
+		dec_topo();
+		printf("pop: stack[%d] = %d\n", get_topo(), stack[get_topo()]);
+		return stack[get_topo()];  
+	}
+}
+
+int main(void) {
+	int arr[SIZE];
+
+	push(arr,3);
+	push(arr,4);
+	push(arr,5);
+	push(arr,1);
+	push(arr,9);
+	push(arr,10);
+	push(arr,6);
+	push(arr,12);
+	push(arr,15);
+	push(arr,8);
+	push(arr,20);
+
+	pop(arr);
+	pop(arr);
+	pop(arr);
+	pop(arr);
+	pop(arr);
+	pop(arr);
+	pop(arr);
+	pop(arr);
+	pop(arr);
+	pop(arr);
+	pop(arr);
+
+}
diff --git a/regression/goto-instrument/slice02/test.desc b/regression/goto-instrument/slice02/test.desc
new file mode 100644
index 00000000000..2d61905c826
--- /dev/null
+++ b/regression/goto-instrument/slice02/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --full-slice
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/goto-instrument/slice03/main.c b/regression/goto-instrument/slice03/main.c
new file mode 100644
index 00000000000..589c5db2e70
--- /dev/null
+++ b/regression/goto-instrument/slice03/main.c
@@ -0,0 +1,102 @@
+#include <stdio.h>
+
+#define SIZE 10
+
+typedef struct{
+    int elemento[SIZE];
+    int inicio;
+    int fim;
+    int quantidade;
+} QType;
+
+int inicializa(QType *q) {
+	q->inicio=0;
+	q->fim=0;
+	q->quantidade=0;
+}
+
+int empty(QType * q) {
+  if (q->inicio == q->fim) { 
+	printf("queue is empty\n");
+    return -1;
+  }
+  else return 0;
+}
+
+int full(QType * q) {
+
+	if (q->quantidade == SIZE) {  
+		printf("queue is full\n");
+		return -1;
+	} else{
+		return 0;
+	}
+}
+
+int enqueue(QType *q, int x) {
+	q->elemento[q->fim] = x;
+	q->quantidade++;
+	if (q->fim == SIZE) {
+		q->fim = 0;
+	} else {
+		q->fim++;
+	}
+	return 0;
+}
+
+int dequeue(QType *q) {
+
+	int x;
+
+	x = q->elemento[q->inicio];
+	q->quantidade--;
+	if (q->inicio == SIZE) {
+		q->inicio = 0;
+	} else { 
+		q->inicio++;
+	}
+
+	return x;
+}
+
+
+int main(void) {
+
+	QType queue;
+
+	int i,temp;
+
+	inicializa(&queue);
+
+	empty(&queue);
+
+	enqueue(&queue,2);
+
+	empty(&queue);
+
+	enqueue(&queue,4);
+	enqueue(&queue,1);
+	enqueue(&queue,5);
+	enqueue(&queue,3);
+	enqueue(&queue,8);
+	enqueue(&queue,6);
+	enqueue(&queue,7);
+	enqueue(&queue,10);
+	enqueue(&queue,9);
+	
+	full(&queue);
+
+	temp = dequeue(&queue);
+
+	printf("temp = %d\n", temp);
+
+	temp = dequeue(&queue);
+
+	printf("temp = %d\n", temp);
+
+	for(i=queue.inicio; i<queue.fim; i++){
+		printf("queue[%d] = %d\n", i, queue.elemento[i]);
+	}
+
+	return 0;
+}
diff --git a/regression/goto-instrument/slice03/test.desc b/regression/goto-instrument/slice03/test.desc
new file mode 100644
index 00000000000..f9810300c02
--- /dev/null
+++ b/regression/goto-instrument/slice03/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--unwind 10 --pointer-check --bounds-check --full-slice
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/goto-instrument/slice04/main.c b/regression/goto-instrument/slice04/main.c
new file mode 100644
index 00000000000..23a87d492c9
--- /dev/null
+++ b/regression/goto-instrument/slice04/main.c
@@ -0,0 +1,58 @@
+/*
+** float-rounder-bug.c
+**
+** Martin Brain
+** martin.brain@cs.ox.ac.uk
+** 20/05/13
+**
+** Another manifestation of the casting bug.
+** If the number is in (0,0x1p-126) it is rounded to zero rather than a subnormal number.
+*/
+#include <assert.h>
+
+#define FULP 1
+
+void bug (float min) {
+  __CPROVER_assume(min == 0x1.fffffep-105f);
+  float modifier = (0x1.0p-23 * (1<<FULP));
+  float ulpdiff = min * modifier;
+
+  assert(ulpdiff == 0x1p-126f);    // Should be true
+
+  return;
+}
+
+void bugBrokenOut (float min) {
+  __CPROVER_assume(min == 0x1.fffffep-105f);
+  float modifier = (0x1.0p-23 * (1<<FULP));
+  double dulpdiff = (double)min * (double)modifier;  // Fine up to here
+  float ulpdiff = (float)dulpdiff;  // Error
+
+  assert(ulpdiff == 0x1p-126f); // Should be true
+
+  return;
+}
+
+void bugCasting (double d) {
+  __CPROVER_assume(d == 0x1.fffffep-127);
+
+  float f = (float) d;
+
+  assert(f == 0x1p-126f); // Should be true
+
+  return;
+}
+
+int main (void) {
+  float f;
+  bug(f);
+
+  float g;
+  bugBrokenOut(g);
+
+  double d;
+  bugCasting(d);
+
+  return 1;
+}
+
diff --git a/regression/goto-instrument/slice04/test.desc b/regression/goto-instrument/slice04/test.desc
new file mode 100644
index 00000000000..3793f7374e1
--- /dev/null
+++ b/regression/goto-instrument/slice04/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--full-slice
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/goto-instrument/slice05/main.c b/regression/goto-instrument/slice05/main.c
new file mode 100644
index 00000000000..30e59ce9c7e
--- /dev/null
+++ b/regression/goto-instrument/slice05/main.c
@@ -0,0 +1,15 @@
+int main()
+{
+  int x = 1; /* considering changing this line */
+  int y = 3;
+  int p = x + y;
+  int z = y -2;
+  int r = 0;
+
+  if(p==0)
+  r++;
+
+  assert(r==0);
+
+  return 0;
+}
diff --git a/regression/goto-instrument/slice05/test.desc b/regression/goto-instrument/slice05/test.desc
new file mode 100644
index 00000000000..3793f7374e1
--- /dev/null
+++ b/regression/goto-instrument/slice05/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--full-slice
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/goto-instrument/slice06/main.c b/regression/goto-instrument/slice06/main.c
new file mode 100644
index 00000000000..0bdb68d3c5f
--- /dev/null
+++ b/regression/goto-instrument/slice06/main.c
@@ -0,0 +1,15 @@
+#define N 10
+
+int main()
+{
+  int i;
+  int sum = 0;
+  int product = 1;
+  for(i = 1; i < N; ++i) {
+    sum = sum + i;
+    product = product * i;
+  }
+  assert(sum>0);
+
+  return 0;
+}
diff --git a/regression/goto-instrument/slice06/test.desc b/regression/goto-instrument/slice06/test.desc
new file mode 100644
index 00000000000..3793f7374e1
--- /dev/null
+++ b/regression/goto-instrument/slice06/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--full-slice
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/goto-instrument/slice07/main.c b/regression/goto-instrument/slice07/main.c
new file mode 100644
index 00000000000..b0acb74a73c
--- /dev/null
+++ b/regression/goto-instrument/slice07/main.c
@@ -0,0 +1,50 @@
+#include <assert.h>
+#include <pthread.h>
+
+//#define NULL 0
+
+int g;
+
+void *t1(void *arg)
+{
+  int a1, *aptr1;
+  
+  aptr1=(int *)arg;
+  a1=*aptr1;
+  g=0;
+  // this should pass
+  assert(a1==10);
+  assert(g==0);
+
+  return NULL;
+}
+
+void *t2(void *arg)
+{
+  int a2, *aptr2;
+  
+  aptr2=(int *)arg;
+  a2=*aptr2;
+  g=0;
+  // this should pass
+  assert(a2==20);
+
+  return NULL;
+}
+
+int main()
+{
+  pthread_t id1, id2;
+  
+  int arg1=10, arg2=20;
+
+  pthread_create(&id1, NULL, t1, &arg1);
+  pthread_create(&id2, NULL, t2, &arg2);
+
+  assert(g==0);
+
+  pthread_join(id1, NULL);
+  pthread_join(id2, NULL);
+
+  return 0;
+}
diff --git a/regression/goto-instrument/slice07/test.desc b/regression/goto-instrument/slice07/test.desc
new file mode 100644
index 00000000000..f40f8bd1c64
--- /dev/null
+++ b/regression/goto-instrument/slice07/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+--full-slice
+^EXIT=6$
+^SIGNAL=0$
+^\-\-full\-slice does not support C/Pthreads yet$
+--
+^warning: ignoring
diff --git a/regression/goto-instrument/slice08/main.c b/regression/goto-instrument/slice08/main.c
new file mode 100644
index 00000000000..c16cd2784ab
--- /dev/null
+++ b/regression/goto-instrument/slice08/main.c
@@ -0,0 +1,21 @@
+#include <assert.h>
+#include <pthread.h>
+
+int main (void) 
+{
+  int x;
+  int i;
+
+  if (x > 0) {
+    for (i = 0; i < x; ++i) {
+        // Do nothing;
+    }
+  } else {
+    x = 1;
+  }
+
+  assert(x >= 1);
+
+  return 0;
+}
+
diff --git a/regression/goto-instrument/slice08/test.desc b/regression/goto-instrument/slice08/test.desc
new file mode 100644
index 00000000000..67625747cf1
--- /dev/null
+++ b/regression/goto-instrument/slice08/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--full-slice --unwind 1
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/goto-instrument/slice09/main.c b/regression/goto-instrument/slice09/main.c
new file mode 100644
index 00000000000..6cc9ba5bc92
--- /dev/null
+++ b/regression/goto-instrument/slice09/main.c
@@ -0,0 +1,9 @@
+#include <assert.h>
+int n=2;
+void main()
+{
+  int i=1;
+  while (i <= n) 
+    i++;
+  assert(i>=0);
+}
diff --git a/regression/goto-instrument/slice09/test.desc b/regression/goto-instrument/slice09/test.desc
new file mode 100644
index 00000000000..3793f7374e1
--- /dev/null
+++ b/regression/goto-instrument/slice09/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--full-slice
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/goto-instrument/slice10/main.c b/regression/goto-instrument/slice10/main.c
new file mode 100644
index 00000000000..dd59d87af39
--- /dev/null
+++ b/regression/goto-instrument/slice10/main.c
@@ -0,0 +1,18 @@
+#include <assert.h>
+int n=2, i, s, a = 0;
+void main()
+{
+  i = 1;
+  s = 1;
+  if (a > 0)
+    s = 0;
+  while (i <= n) 
+  {
+    if (a > 0)
+      s += 2;
+    else
+      s *= 2;
+    i++;
+  }
+  assert(s>0);
+}
diff --git a/regression/goto-instrument/slice10/test.desc b/regression/goto-instrument/slice10/test.desc
new file mode 100644
index 00000000000..3793f7374e1
--- /dev/null
+++ b/regression/goto-instrument/slice10/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--full-slice
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/goto-instrument/slice11/main.c b/regression/goto-instrument/slice11/main.c
new file mode 100644
index 00000000000..b87123d1abe
--- /dev/null
+++ b/regression/goto-instrument/slice11/main.c
@@ -0,0 +1,18 @@
+#include <assert.h>
+int n=2, i, s, a = 0;
+void main()
+{
+  i = 1;
+  s = 1;
+  if (a > 0)
+    s = 0;
+  while (i <= n) 
+  {
+    if (a > 0)
+      s += 2;
+    else
+      s *= 2;
+    i++;
+  }
+  assert(i>0);
+}
diff --git a/regression/goto-instrument/slice11/test.desc b/regression/goto-instrument/slice11/test.desc
new file mode 100644
index 00000000000..3793f7374e1
--- /dev/null
+++ b/regression/goto-instrument/slice11/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--full-slice
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/goto-instrument/slice12/main.c b/regression/goto-instrument/slice12/main.c
new file mode 100644
index 00000000000..7b395dc27d3
--- /dev/null
+++ b/regression/goto-instrument/slice12/main.c
@@ -0,0 +1,12 @@
+#include <assert.h>
+int n=2, i, s, a = 0;
+void main()
+{
+  i = 1;
+  s = 1;
+  if (a > 0)
+    s = 0;
+  if (n==1)
+    s=1;
+  assert(n>0);
+}
diff --git a/regression/goto-instrument/slice12/test.desc b/regression/goto-instrument/slice12/test.desc
new file mode 100644
index 00000000000..3793f7374e1
--- /dev/null
+++ b/regression/goto-instrument/slice12/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--full-slice
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/goto-instrument/slice13/main.c b/regression/goto-instrument/slice13/main.c
new file mode 100644
index 00000000000..3354961512a
--- /dev/null
+++ b/regression/goto-instrument/slice13/main.c
@@ -0,0 +1,23 @@
+#ifdef __GNUC__
+#include <assert.h>
+#include <math.h>
+#include <fenv.h>
+
+float setRoundingModeAndCast(int mode, double d) {
+  fesetround(mode);
+  return (float)d;
+}
+
+void test (int mode, double d, float result) {
+  float f = setRoundingModeAndCast(mode,d);
+  assert(f == result);
+  return;
+}
+#endif
+
+int main (void)
+{
+  // Nearer to 0x1.fffffep+127 than to 0x1.000000p+128
+  test(FE_UPWARD, 0x1.fffffe0000001p+127, +INFINITY);
+  return 1;
+}
diff --git a/regression/goto-instrument/slice13/test.desc b/regression/goto-instrument/slice13/test.desc
new file mode 100644
index 00000000000..cc8dd41ed5f
--- /dev/null
+++ b/regression/goto-instrument/slice13/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+--floatbv --full-slice
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/goto-instrument/slice14/main.c b/regression/goto-instrument/slice14/main.c
new file mode 100644
index 00000000000..ef23ab68a1a
--- /dev/null
+++ b/regression/goto-instrument/slice14/main.c
@@ -0,0 +1,15 @@
+void *malloc(__CPROVER_size_t);
+void free(void *);
+
+int main()
+{
+  int *p=malloc(sizeof(int));
+  int *q=p;
+  int i, x;
+  i=x;
+  
+  if(i==4711) free(q);
+
+  // should fail if i==4711
+  *p=1;
+}
diff --git a/regression/goto-instrument/slice14/test.desc b/regression/goto-instrument/slice14/test.desc
new file mode 100644
index 00000000000..ef912633761
--- /dev/null
+++ b/regression/goto-instrument/slice14/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+--pointer-check --full-slice
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/regression/goto-instrument/slice15/main.c b/regression/goto-instrument/slice15/main.c
new file mode 100644
index 00000000000..0572b279999
--- /dev/null
+++ b/regression/goto-instrument/slice15/main.c
@@ -0,0 +1,24 @@
+int nondet_int();
+
+double d = 0.0;
+
+void f1()
+{
+  d = 1.0;
+}
+
+int main()
+{
+  int x = 2;
+
+  if(nondet_int())
+    x = 4;
+
+  (void) f1();
+
+  d += (x == 2);
+
+  d += (x > 3);
+
+  assert(d == 2.0);
+}
diff --git a/regression/goto-instrument/slice15/test.desc b/regression/goto-instrument/slice15/test.desc
new file mode 100644
index 00000000000..3793f7374e1
--- /dev/null
+++ b/regression/goto-instrument/slice15/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--full-slice
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/goto-instrument/slice16/main.c b/regression/goto-instrument/slice16/main.c
new file mode 100644
index 00000000000..99d0cda2c16
--- /dev/null
+++ b/regression/goto-instrument/slice16/main.c
@@ -0,0 +1,48 @@
+/* running example extracted from 
+"In Slicing Programs with Jump Statements" 
+by Hiralal Afrawal */
+#include <assert.h>
+int x;
+_Bool nondet_bool();
+unsigned int nondet_uint();
+
+_Bool leof() {
+  return nondet_bool();
+}
+
+int f1(int x) {
+  return x*1;
+}
+
+int f2(int x) {
+  return x*2;
+}
+
+int f3(int x) {
+  return x*3;
+}
+
+void read(int *x) {
+  x = nondet_uint();
+}
+
+int main() {
+  int sum=0;
+  int positives=0;
+  while(leof())
+  {
+    read(x);
+    if (x <= 0)  
+      sum = sum + f1(x);
+    else
+    {
+      positives = positives + 1;
+      if (x%2 == 0)
+        sum = sum + f2(x);
+      else
+        sum = sum + f3(x);
+    }
+  }
+  assert(sum>=0);
+  assert(positives>=0);
+}
diff --git a/regression/goto-instrument/slice16/test.desc b/regression/goto-instrument/slice16/test.desc
new file mode 100644
index 00000000000..0f63776547f
--- /dev/null
+++ b/regression/goto-instrument/slice16/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--full-slice --unwind 2
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/goto-instrument/slice17/main.c b/regression/goto-instrument/slice17/main.c
new file mode 100644
index 00000000000..ccc03df0596
--- /dev/null
+++ b/regression/goto-instrument/slice17/main.c
@@ -0,0 +1,35 @@
+#include <assert.h>
+#include <stdint.h>
+
+union u
+{
+  uint32_t x;
+   int32_t y;
+   int8_t  z[4];
+};
+
+union u pass_through_union (uint32_t q)
+{
+  union u un;
+
+  un.z[0] = 0x0;
+  un.y = q;
+  un.z[3] = 0x0;
+  un.z[0] = 0x0;
+
+  return un;
+}
+
+int main (void)
+{
+  uint32_t q;
+
+  __CPROVER_assume((q & q - 1) == 0);
+  __CPROVER_assume(256 <= q && q <= (1 << 23));
+
+  union u un = pass_through_union(q);
+
+  assert(q == un.y);
+
+  return 1;
+}
diff --git a/regression/goto-instrument/slice17/test.desc b/regression/goto-instrument/slice17/test.desc
new file mode 100644
index 00000000000..03cff4a4fac
--- /dev/null
+++ b/regression/goto-instrument/slice17/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+--full-slice
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/goto-instrument/slice18/main.c b/regression/goto-instrument/slice18/main.c
new file mode 100644
index 00000000000..0661315487b
--- /dev/null
+++ b/regression/goto-instrument/slice18/main.c
@@ -0,0 +1,11 @@
+void exit(int status);
+
+int main() {
+  int x;
+  
+  if(x==10)
+    exit(1);
+
+  if(x==10)
+    assert(0);
+}
diff --git a/regression/goto-instrument/slice18/test.desc b/regression/goto-instrument/slice18/test.desc
new file mode 100644
index 00000000000..03cff4a4fac
--- /dev/null
+++ b/regression/goto-instrument/slice18/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+--full-slice
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/goto-instrument/slice19/main.c b/regression/goto-instrument/slice19/main.c
new file mode 100644
index 00000000000..ecd39ff0d4c
--- /dev/null
+++ b/regression/goto-instrument/slice19/main.c
@@ -0,0 +1,45 @@
+#include <string.h>
+#include <stdio.h>
+#include <assert.h>
+
+void sort_items_by_criteria( int * item, int left, int right )
+{
+  int lidx = left, ridx = (left+right)/2 + 1, lsize = (left+right)/2 - left + 1;
+  int tmp;
+
+  if ( right - left < 1 ) return;
+  sort_items_by_criteria( item, left, (left+right)/2 );
+  sort_items_by_criteria( item, (left+right)/2 + 1, right );
+
+  while ( ridx <= right && lidx < ridx ) {
+    if ( item[lidx] > item[ridx] ) {
+      tmp = item[ridx];
+      memmove( item + lidx + 1, item + lidx, lsize * sizeof(int) );
+      item[lidx] = tmp;
+      ++ridx;
+      ++lsize;
+    }
+    ++lidx;
+    --lsize;
+  }
+}
+
+int main(int argc, char * argv[]) {
+  int a[7];
+
+  //CBMC reports wrong results for 256, -2147221455, -2147221455, -2147221455, 16, -2147483600, 16384
+  a[0] = 256;
+  a[1] = -2147221455;
+  a[2] = -2147221455;
+  a[3] = -2147221455;
+  a[4] = 16;
+  a[5] = -2147483600;
+  a[6] = 16384;
+
+  sort_items_by_criteria(a, 0, 6);
+
+  printf("%d %d %d %d %d %d %d\n", a[0], a[1], a[2], a[3], a[4], a[5], a[6]);
+
+  assert(a[0]==-2147483600);
+  return 0;
+}
diff --git a/regression/goto-instrument/slice19/test.desc b/regression/goto-instrument/slice19/test.desc
new file mode 100644
index 00000000000..03cff4a4fac
--- /dev/null
+++ b/regression/goto-instrument/slice19/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+--full-slice
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/goto-instrument/slice20/main.c b/regression/goto-instrument/slice20/main.c
new file mode 100644
index 00000000000..6a9f339e7e0
--- /dev/null
+++ b/regression/goto-instrument/slice20/main.c
@@ -0,0 +1,29 @@
+#include <assert.h>
+
+void recursion(_Bool rec, int *p)
+{
+  int some_local, other_local;
+
+  if(rec)
+  {
+    some_local=2;
+    other_local=30;
+    rec=1;
+    *p=20; // overwrites other_local in previous frame
+    assert(other_local==30);
+  }
+  else
+  {
+    some_local=1;
+    other_local=10;
+    recursion(1, &other_local);
+    assert(!rec);
+    assert(some_local==1);
+    assert(other_local==20);
+  }
+}
+
+int main()
+{
+  recursion(0, 0);
+}
diff --git a/regression/goto-instrument/slice20/test.desc b/regression/goto-instrument/slice20/test.desc
new file mode 100644
index 00000000000..03cff4a4fac
--- /dev/null
+++ b/regression/goto-instrument/slice20/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+--full-slice
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/goto-instrument/slice21/main.c b/regression/goto-instrument/slice21/main.c
new file mode 100644
index 00000000000..ccc03df0596
--- /dev/null
+++ b/regression/goto-instrument/slice21/main.c
@@ -0,0 +1,35 @@
+#include <assert.h>
+#include <stdint.h>
+
+union u
+{
+  uint32_t x;
+   int32_t y;
+   int8_t  z[4];
+};
+
+union u pass_through_union (uint32_t q)
+{
+  union u un;
+
+  un.z[0] = 0x0;
+  un.y = q;
+  un.z[3] = 0x0;
+  un.z[0] = 0x0;
+
+  return un;
+}
+
+int main (void)
+{
+  uint32_t q;
+
+  __CPROVER_assume((q & q - 1) == 0);
+  __CPROVER_assume(256 <= q && q <= (1 << 23));
+
+  union u un = pass_through_union(q);
+
+  assert(q == un.y);
+
+  return 1;
+}
diff --git a/regression/goto-instrument/slice21/test.desc b/regression/goto-instrument/slice21/test.desc
new file mode 100644
index 00000000000..03cff4a4fac
--- /dev/null
+++ b/regression/goto-instrument/slice21/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+--full-slice
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring