diff --git a/regression/cbmc-slice/Makefile b/regression/cbmc-slice/Makefile
new file mode 100644
index 00000000000..cbdd3378bac
--- /dev/null
+++ b/regression/cbmc-slice/Makefile
@@ -0,0 +1,20 @@
+default: tests.log
+
+test:
+	@if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \
+		../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
+
+tests.log: ../test.pl
+	@if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \
+		../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
diff --git a/regression/cbmc-slice/slice01/main.c b/regression/cbmc-slice/slice01/main.c
new file mode 100644
index 00000000000..7502ff7413a
--- /dev/null
+++ b/regression/cbmc-slice/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/cbmc-slice/slice01/test.desc b/regression/cbmc-slice/slice01/test.desc
new file mode 100644
index 00000000000..6f19f2d9ef6
--- /dev/null
+++ b/regression/cbmc-slice/slice01/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--unwind 2 --full-slice
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-slice/slice02/main.c b/regression/cbmc-slice/slice02/main.c
new file mode 100644
index 00000000000..8c7aa38de2c
--- /dev/null
+++ b/regression/cbmc-slice/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/cbmc-slice/slice02/test.desc b/regression/cbmc-slice/slice02/test.desc
new file mode 100644
index 00000000000..2d61905c826
--- /dev/null
+++ b/regression/cbmc-slice/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/cbmc-slice/slice03/main.c b/regression/cbmc-slice/slice03/main.c
new file mode 100644
index 00000000000..589c5db2e70
--- /dev/null
+++ b/regression/cbmc-slice/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/cbmc-slice/slice03/test.desc b/regression/cbmc-slice/slice03/test.desc
new file mode 100644
index 00000000000..f9810300c02
--- /dev/null
+++ b/regression/cbmc-slice/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/cbmc-slice/slice04/main.c b/regression/cbmc-slice/slice04/main.c
new file mode 100644
index 00000000000..23a87d492c9
--- /dev/null
+++ b/regression/cbmc-slice/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/cbmc-slice/slice04/test.desc b/regression/cbmc-slice/slice04/test.desc
new file mode 100644
index 00000000000..4d8899e64c7
--- /dev/null
+++ b/regression/cbmc-slice/slice04/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--floatbv --full-slice
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-slice/slice05/main.c b/regression/cbmc-slice/slice05/main.c
new file mode 100644
index 00000000000..30e59ce9c7e
--- /dev/null
+++ b/regression/cbmc-slice/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/cbmc-slice/slice05/test.desc b/regression/cbmc-slice/slice05/test.desc
new file mode 100644
index 00000000000..3793f7374e1
--- /dev/null
+++ b/regression/cbmc-slice/slice05/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--full-slice
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-slice/slice06/main.c b/regression/cbmc-slice/slice06/main.c
new file mode 100644
index 00000000000..0bdb68d3c5f
--- /dev/null
+++ b/regression/cbmc-slice/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/cbmc-slice/slice06/test.desc b/regression/cbmc-slice/slice06/test.desc
new file mode 100644
index 00000000000..3793f7374e1
--- /dev/null
+++ b/regression/cbmc-slice/slice06/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--full-slice
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-slice/slice07/main.c b/regression/cbmc-slice/slice07/main.c
new file mode 100644
index 00000000000..b0acb74a73c
--- /dev/null
+++ b/regression/cbmc-slice/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/cbmc-slice/slice07/test.desc b/regression/cbmc-slice/slice07/test.desc
new file mode 100644
index 00000000000..7d88efc76ad
--- /dev/null
+++ b/regression/cbmc-slice/slice07/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--full-slice
+^EXIT=6$
+^SIGNAL=0$
+^\-\-full\-slice does not support C/Pthreads yet$
+--
+^warning: ignoring
diff --git a/regression/cbmc-slice/slice08/main.c b/regression/cbmc-slice/slice08/main.c
new file mode 100644
index 00000000000..c16cd2784ab
--- /dev/null
+++ b/regression/cbmc-slice/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/cbmc-slice/slice08/test.desc b/regression/cbmc-slice/slice08/test.desc
new file mode 100644
index 00000000000..67625747cf1
--- /dev/null
+++ b/regression/cbmc-slice/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/cbmc-slice/slice09/main.c b/regression/cbmc-slice/slice09/main.c
new file mode 100644
index 00000000000..6cc9ba5bc92
--- /dev/null
+++ b/regression/cbmc-slice/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/cbmc-slice/slice09/test.desc b/regression/cbmc-slice/slice09/test.desc
new file mode 100644
index 00000000000..3793f7374e1
--- /dev/null
+++ b/regression/cbmc-slice/slice09/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--full-slice
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-slice/slice10/main.c b/regression/cbmc-slice/slice10/main.c
new file mode 100644
index 00000000000..dd59d87af39
--- /dev/null
+++ b/regression/cbmc-slice/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/cbmc-slice/slice10/test.desc b/regression/cbmc-slice/slice10/test.desc
new file mode 100644
index 00000000000..3793f7374e1
--- /dev/null
+++ b/regression/cbmc-slice/slice10/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--full-slice
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-slice/slice11/main.c b/regression/cbmc-slice/slice11/main.c
new file mode 100644
index 00000000000..b87123d1abe
--- /dev/null
+++ b/regression/cbmc-slice/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/cbmc-slice/slice11/test.desc b/regression/cbmc-slice/slice11/test.desc
new file mode 100644
index 00000000000..3793f7374e1
--- /dev/null
+++ b/regression/cbmc-slice/slice11/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--full-slice
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-slice/slice12/main.c b/regression/cbmc-slice/slice12/main.c
new file mode 100644
index 00000000000..7b395dc27d3
--- /dev/null
+++ b/regression/cbmc-slice/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/cbmc-slice/slice12/test.desc b/regression/cbmc-slice/slice12/test.desc
new file mode 100644
index 00000000000..3793f7374e1
--- /dev/null
+++ b/regression/cbmc-slice/slice12/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--full-slice
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-slice/slice13/main.c b/regression/cbmc-slice/slice13/main.c
new file mode 100644
index 00000000000..3354961512a
--- /dev/null
+++ b/regression/cbmc-slice/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/cbmc-slice/slice13/test.desc b/regression/cbmc-slice/slice13/test.desc
new file mode 100644
index 00000000000..4d8899e64c7
--- /dev/null
+++ b/regression/cbmc-slice/slice13/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--floatbv --full-slice
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-slice/slice14/main.c b/regression/cbmc-slice/slice14/main.c
new file mode 100644
index 00000000000..ef23ab68a1a
--- /dev/null
+++ b/regression/cbmc-slice/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/cbmc-slice/slice14/test.desc b/regression/cbmc-slice/slice14/test.desc
new file mode 100644
index 00000000000..a2b36885fc7
--- /dev/null
+++ b/regression/cbmc-slice/slice14/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --full-slice
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/regression/cbmc-slice/slice15/main.c b/regression/cbmc-slice/slice15/main.c
new file mode 100644
index 00000000000..0572b279999
--- /dev/null
+++ b/regression/cbmc-slice/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/cbmc-slice/slice15/test.desc b/regression/cbmc-slice/slice15/test.desc
new file mode 100644
index 00000000000..8e6dafcc8e6
--- /dev/null
+++ b/regression/cbmc-slice/slice15/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--fixedbv --full-slice
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-slice/slice16/main.c b/regression/cbmc-slice/slice16/main.c
new file mode 100644
index 00000000000..99d0cda2c16
--- /dev/null
+++ b/regression/cbmc-slice/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/cbmc-slice/slice16/test.desc b/regression/cbmc-slice/slice16/test.desc
new file mode 100644
index 00000000000..0f63776547f
--- /dev/null
+++ b/regression/cbmc-slice/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/cbmc-slice/slice17/main.c b/regression/cbmc-slice/slice17/main.c
new file mode 100644
index 00000000000..ccc03df0596
--- /dev/null
+++ b/regression/cbmc-slice/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/cbmc-slice/slice17/test.desc b/regression/cbmc-slice/slice17/test.desc
new file mode 100644
index 00000000000..9efefbc7362
--- /dev/null
+++ b/regression/cbmc-slice/slice17/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-slice/slice18/main.c b/regression/cbmc-slice/slice18/main.c
new file mode 100644
index 00000000000..0661315487b
--- /dev/null
+++ b/regression/cbmc-slice/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/cbmc-slice/slice18/test.desc b/regression/cbmc-slice/slice18/test.desc
new file mode 100644
index 00000000000..9efefbc7362
--- /dev/null
+++ b/regression/cbmc-slice/slice18/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/analyses/ai.h b/src/analyses/ai.h
index a0938b514bc..c8e6dff9d57 100644
--- a/src/analyses/ai.h
+++ b/src/analyses/ai.h
@@ -274,6 +274,14 @@ class ait:public ai_baset
     ai_baset::clear();
   }
 
+  // this one just finds states
+  virtual const bool state_exist(locationt l) const
+  {
+    typename state_mapt::const_iterator it=state_map.find(l);
+    if(it==state_map.end()) return false;
+    return true;
+  }
+
 protected:
   typedef hash_map_cont<locationt, domainT, const_target_hash> state_mapt;
   state_mapt state_map;
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 08955180271..9ed14620649 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -855,11 +855,37 @@ bool cbmc_parse_optionst::process_goto_program(
       cmdline.isset("pointer-check"));
     remove_virtual_functions(symbol_table, goto_functions);
 
+    // do partial inlining
+    status() << "Partial Inlining" << eom;
+    goto_partial_inline(goto_functions, ns, ui_message_handler);
+
+    // remove returns, gcc vectors, complex
+    remove_returns(symbol_table, goto_functions);
+    remove_vector(symbol_table, goto_functions);
+    remove_complex(symbol_table, goto_functions);
+
+    // add generic checks
+    status() << "Generic Property Instrumentation" << eom;
+    goto_check(ns, options, goto_functions);
+
     // full slice?
     if(cmdline.isset("full-slice"))
     {
       status() << "Performing a full slice" << eom;
-      full_slicer(goto_functions, ns);
+      remove_virtual_functions(symbol_table,goto_functions);
+      remove_function_pointers(symbol_table,goto_functions,cmdline.isset("pointer-check"));
+      remove_returns(symbol_table,goto_functions);
+      goto_functions.update();
+      try
+      {
+        full_slicer(goto_functions, ns);
+      }
+
+      catch(const char *error_msg)
+      {
+        error() << error_msg << eom;
+        return 1;
+      }
     }
 
     // do partial inlining
diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp
index 7672036cecf..9b1959ecc7f 100644
--- a/src/goto-instrument/full_slicer.cpp
+++ b/src/goto-instrument/full_slicer.cpp
@@ -6,8 +6,12 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
+#include <iostream>
+
 #include <util/find_symbols.h>
 #include <util/cprover_prefix.h>
+#include <util/prefix.h>
+
 #ifdef DEBUG_FULL_SLICERT
 #include <util/i2string.h>
 #endif
@@ -37,14 +41,17 @@ void full_slicert::add_dependencies(
   const dependence_grapht &dep_graph,
   const dep_node_to_cfgt &dep_node_to_cfg)
 {
-  const dependence_grapht::nodet &d_node=
-    dep_graph[dep_graph[node.PC].get_node_id()];
-
-  for(dependence_grapht::edgest::const_iterator
-      it=d_node.in.begin();
-      it!=d_node.in.end();
-      ++it)
-    add_to_queue(queue, dep_node_to_cfg[it->first], node.PC);
+  if (dep_graph.state_exist(node.PC))
+  {
+    const dependence_grapht::nodet &d_node=
+      dep_graph[dep_graph[node.PC].get_node_id()];
+
+    for(dependence_grapht::edgest::const_iterator
+        it=d_node.in.begin();
+        it!=d_node.in.end();
+        ++it)
+      add_to_queue(queue, dep_node_to_cfg[it->first], node.PC);
+  }
 }
 
 /*******************************************************************\
@@ -270,7 +277,7 @@ void full_slicert::fixedpoint(
 {
   std::vector<cfgt::entryt> dep_node_to_cfg;
   dep_node_to_cfg.reserve(dep_graph.size());
-  for(dependence_grapht::node_indext i=0; i<dep_graph.size(); ++i)
+  for(unsigned i=0; i<dep_graph.size(); ++i)
   {
     cfgt::entry_mapt::const_iterator entry=
       cfg.entry_map.find(dep_graph[i].PC);
@@ -322,18 +329,38 @@ Function: implicit
 
 \*******************************************************************/
 
-static bool implicit(goto_programt::const_targett target)
+static bool implicit(const namespacet &ns, goto_programt::const_targett target)
 {
   // some variables are used during symbolic execution only
 
+  const irep_idt &statement=target->code.get(ID_statement);
+  if (statement==ID_array_copy) return true;
+
+  if (target->is_assume()) return true;
   if(!target->is_assign()) return false;
 
   const code_assignt &a=to_code_assign(target->code);
+  if(a.lhs().id()==ID_dereference) return true;
   if(a.lhs().id()!=ID_symbol) return false;
 
   const symbol_exprt &s=to_symbol_expr(a.lhs());
 
-  return s.get_identifier()==CPROVER_PREFIX "rounding_mode";
+  if (s.source_location().get_function().empty())
+  {
+    // is it a __CPROVER_* variable?
+    if(has_prefix(id2string(s.get_identifier()), CPROVER_PREFIX))
+	  return true;
+
+    // static lifetime?
+    if(ns.lookup(s.get_identifier()).is_static_lifetime)
+      return true;
+  }
+
+  if (s.get_identifier()==CPROVER_PREFIX "rounding_mode" ||
+      s.get_identifier()==CPROVER_PREFIX "deallocated")
+    return true;
+
+  return false;
 }
 
 /*******************************************************************\
@@ -370,7 +397,7 @@ void full_slicert::operator()(
   {
     if(criterion(e_it->first))
       add_to_queue(queue, e_it->second, e_it->first);
-    else if(implicit(e_it->first))
+    else if(implicit(ns,e_it->first))
       add_to_queue(queue, e_it->second, e_it->first);
     else if((e_it->first->is_goto() && e_it->first->guard.is_true()) ||
             e_it->first->is_throw())
@@ -385,6 +412,8 @@ void full_slicert::operator()(
       const exprt &s=to_code_dead(e_it->first->code).symbol();
       decl_dead[to_symbol_expr(s).get_identifier()].push(e_it->second);
     }
+    else if(e_it->first->is_function_call())
+      add_to_queue(queue, e_it->second, e_it->first);
   }
 
   // compute program dependence graph (and post-dominators)
@@ -400,6 +429,9 @@ void full_slicert::operator()(
   Forall_goto_functions(f_it, goto_functions)
     if(f_it->second.body_available())
     {
+   	  if(f_it->first=="pthread_create")
+   		throw "--full-slice does not support C/Pthreads yet";
+
       Forall_goto_program_instructions(i_it, f_it->second.body)
       {
         const cfgt::entryt &e=cfg.entry_map[i_it];
diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp
index d758e40c987..90acadc1dcc 100644
--- a/src/pointer-analysis/value_set_fi.cpp
+++ b/src/pointer-analysis/value_set_fi.cpp
@@ -1723,6 +1723,10 @@ void value_set_fit::apply_code(
   {
 	  // doesn't do anything
   }
+  else if(statement==ID_array_copy)
+  {
+    // doesn't do anything
+  }
   else
     throw
       code.pretty()+"\n"+