diff --git a/regression/cbmc-concurrency/deadlock1/main.c b/regression/cbmc-concurrency/deadlock1/main.c
index 891fb419e7e..8bf26775d37 100644
--- a/regression/cbmc-concurrency/deadlock1/main.c
+++ b/regression/cbmc-concurrency/deadlock1/main.c
@@ -19,4 +19,4 @@ void main() {
   pthread_join(tid2, NULL); 
   // deadlock in the threads; assertion should not be reachable
   assert(0);
-} 
+}
diff --git a/regression/cbmc-cover/location10/main.c b/regression/cbmc-cover/location10/main.c
new file mode 100644
index 00000000000..c06b43a470e
--- /dev/null
+++ b/regression/cbmc-cover/location10/main.c
@@ -0,0 +1,23 @@
+#include <assert.h>
+
+int myfunc(int x, int y)
+{
+  int z = x + y;
+  return z;
+}
+
+int main(void)
+{
+  _Bool x=0, y;
+  if (x)
+    assert(myfunc(2,3)==5);
+  else
+    y=1;
+
+  if (y)
+    assert(myfunc(4,3)==7);
+  else 
+    assume(0);
+
+  assert(y==1);
+}
diff --git a/regression/cbmc-cover/location10/test.desc b/regression/cbmc-cover/location10/test.desc
new file mode 100644
index 00000000000..4ade078f961
--- /dev/null
+++ b/regression/cbmc-cover/location10/test.desc
@@ -0,0 +1,20 @@
+CORE
+main.c
+--cover location
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.1\] file main.c line 11 function main block 1: SATISFIED$
+^\[main.coverage.2\] file main.c line 13 function main block 2: FAILED$
+^\[main.coverage.3\] file main.c line 13 function main block 3: FAILED$
+^\[main.coverage.4\] file main.c line 15 function main block 5: SATISFIED$
+^\[main.coverage.5\] file main.c line 17 function main block 6: SATISFIED$
+^\[main.coverage.6\] file main.c line 18 function main block 7: SATISFIED$
+^\[main.coverage.7\] file main.c line 18 function main block 8: SATISFIED$
+^\[main.coverage.8\] file main.c line 20 function main block 10: FAILED$
+^\[main.coverage.9\] file main.c line 22 function main block 11: SATISFIED$
+^\[main.coverage.10\] file main.c line 23 function main block 12: SATISFIED$
+^\[myfunc.coverage.1\] file main.c line 5 function myfunc block 1: SATISFIED$
+^\[myfunc.coverage.2\] file main.c line 7 function myfunc block 2: SATISFIED$
+^\*\* 9 of 12 covered (75.0%)
+--
+^warning: ignoring
diff --git a/regression/cbmc-cover/location11/main.c b/regression/cbmc-cover/location11/main.c
new file mode 100644
index 00000000000..cf22990b042
--- /dev/null
+++ b/regression/cbmc-cover/location11/main.c
@@ -0,0 +1,23 @@
+#include <assert.h>
+
+int myfunc(int x, int y)
+{
+  int z = x + y;
+  return z;
+}
+
+int main(void)
+{
+  _Bool x=0, y;
+  if (x)
+    assert(myfunc(2,3)==5);
+  else
+    y=1;
+
+  if (y)
+    y=0;
+  else 
+    __CPROVER_assume(0);
+
+  assert(y==1);
+}
diff --git a/regression/cbmc-cover/location11/test.desc b/regression/cbmc-cover/location11/test.desc
new file mode 100644
index 00000000000..398e9b8b36f
--- /dev/null
+++ b/regression/cbmc-cover/location11/test.desc
@@ -0,0 +1,19 @@
+CORE
+main.c
+--cover location
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.1\] file main.c line 11 function main block 1: SATISFIED$
+^\[main.coverage.2\] file main.c line 13 function main block 2: FAILED$
+^\[main.coverage.3\] file main.c line 13 function main block 3: FAILED$
+^\[main.coverage.4\] file main.c line 15 function main block 5: SATISFIED$
+^\[main.coverage.5\] file main.c line 17 function main block 6: SATISFIED$
+^\[main.coverage.6\] file main.c line 18 function main block 7: SATISFIED$
+^\[main.coverage.7\] file main.c line 20 function main block 8: FAILED$
+^\[main.coverage.8\] file main.c line 22 function main block 9: SATISFIED$
+^\[main.coverage.9\] file main.c line 23 function main block 10: SATISFIED$
+^\[myfunc.coverage.1\] file main.c line 5 function myfunc block 1: FAILED$
+^\[myfunc.coverage.2\] file main.c line 7 function myfunc block 2: FAILED$
+^\*\* 6 of 11 covered (54.5%)
+--
+^warning: ignoring
diff --git a/regression/cbmc-cover/location12/main.c b/regression/cbmc-cover/location12/main.c
new file mode 100644
index 00000000000..118401511b6
--- /dev/null
+++ b/regression/cbmc-cover/location12/main.c
@@ -0,0 +1,12 @@
+#include <assert.h>
+
+int foo (int iX, int iY)
+{
+  return iX + iY;
+  __CPROVER_assume(0);
+}
+
+int main(void)
+{
+  assert(foo(5,3)==8);
+}
diff --git a/regression/cbmc-cover/location12/test.desc b/regression/cbmc-cover/location12/test.desc
new file mode 100644
index 00000000000..8b46af0784d
--- /dev/null
+++ b/regression/cbmc-cover/location12/test.desc
@@ -0,0 +1,15 @@
+CORE
+main.c
+--cover location
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.1\] file main.c line 11 function main block 1: SATISFIED$
+^\[main.coverage.2\] file main.c line 11 function main block 2: SATISFIED$
+^\[main.coverage.3\] file main.c line 12 function main block 3: SATISFIED$
+^\[foo.coverage.1\] file main.c line 5 function foo block 1: SATISFIED$
+^\[foo.coverage.2\] file main.c line 6 function foo block 2: FAILED$
+^\[foo.coverage.3\] file main.c line 7 function foo block 3: FAILED$
+^\[foo.coverage.4\] file main.c line 7 function foo block 4: SATISFIED$
+^\*\* 5 of 7 covered (71.4%)
+--
+^warning: ignoring
diff --git a/regression/cbmc-cover/location13/main.c b/regression/cbmc-cover/location13/main.c
new file mode 100644
index 00000000000..f8d18141ca9
--- /dev/null
+++ b/regression/cbmc-cover/location13/main.c
@@ -0,0 +1,17 @@
+#include <assert.h>
+
+int myfunc(int a, int b)
+{
+  return a+b;
+}
+
+int foo (int iX, int iY)
+{
+  return iX + iY;
+  assert(myfunc(iX,iY)==8);
+}
+
+int main(void)
+{
+  assert(foo(5,3)==8);
+}
diff --git a/regression/cbmc-cover/location13/test.desc b/regression/cbmc-cover/location13/test.desc
new file mode 100644
index 00000000000..543be77b095
--- /dev/null
+++ b/regression/cbmc-cover/location13/test.desc
@@ -0,0 +1,18 @@
+CORE
+main.c
+--cover location
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.1\] file main.c line 16 function main block 1: SATISFIED$
+^\[main.coverage.2\] file main.c line 16 function main block 2: SATISFIED$
+^\[main.coverage.3\] file main.c line 17 function main block 3: SATISFIED$
+^\[myfunc.coverage.1\] file main.c line 5 function myfunc block 1: FAILED$
+^\[myfunc.coverage.2\] file main.c line 6 function myfunc block 2: FAILED$
+^\[foo.coverage.1\] file main.c line 10 function foo block 1: SATISFIED$
+^\[foo.coverage.2\] file main.c line 11 function foo block 2: FAILED$
+^\[foo.coverage.3\] file main.c line 11 function foo block 3: FAILED$
+^\[foo.coverage.4\] file main.c line 12 function foo block 4: FAILED$
+^\[foo.coverage.5\] file main.c line 12 function foo block 5: SATISFIED$
+^\*\* 5 of 10 covered (50.0%)
+--
+^warning: ignoring
diff --git a/regression/cbmc-cover/location14/main.c b/regression/cbmc-cover/location14/main.c
new file mode 100644
index 00000000000..5fbf0c498e7
--- /dev/null
+++ b/regression/cbmc-cover/location14/main.c
@@ -0,0 +1,13 @@
+#include <assert.h>
+
+int foo (int iX, int iY)
+{
+  return iX + iY;
+}
+
+int main(void)
+{
+  int iN = 2 + 1;
+  if (iN == 4)
+    assert(foo(5,3)==8);
+}
diff --git a/regression/cbmc-cover/location14/test.desc b/regression/cbmc-cover/location14/test.desc
new file mode 100644
index 00000000000..f3cb25573da
--- /dev/null
+++ b/regression/cbmc-cover/location14/test.desc
@@ -0,0 +1,14 @@
+CORE
+main.c
+--cover location
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.1\] file main.c line 10 function main block 1: SATISFIED$
+^\[main.coverage.2\] file main.c line 12 function main block 2: FAILED$
+^\[main.coverage.3\] file main.c line 12 function main block 3: FAILED$
+^\[main.coverage.4\] file main.c line 13 function main block 4: SATISFIED$
+^\[foo.coverage.1\] file main.c line 5 function foo block 1: FAILED$
+^\[foo.coverage.2\] file main.c line 6 function foo block 2: FAILED$
+^\*\* 2 of 6 covered (33.3%)
+--
+^warning: ignoring
diff --git a/regression/cbmc-cover/location15/main.c b/regression/cbmc-cover/location15/main.c
new file mode 100644
index 00000000000..799293db22c
--- /dev/null
+++ b/regression/cbmc-cover/location15/main.c
@@ -0,0 +1,17 @@
+#include <assert.h>
+#include <math.h>
+
+int foo (int iX, int iY)
+{
+  return iX + iY;
+}
+
+int main(void)
+{
+  double dX = sqrt(2);
+  if (dX > 5)
+  {
+    __CPROVER_assume(0);
+    assert(foo(5,3)==1);
+  }    
+}
diff --git a/regression/cbmc-cover/location15/test.desc b/regression/cbmc-cover/location15/test.desc
new file mode 100644
index 00000000000..3fb10c3066b
--- /dev/null
+++ b/regression/cbmc-cover/location15/test.desc
@@ -0,0 +1,17 @@
+CORE
+main.c
+--cover location
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.1\] file main.c line 11 function main block 1: SATISFIED$
+^\[main.coverage.2\] file main.c line 11 function main block 2: SATISFIED$
+^\[main.coverage.3\] file main.c line 14 function main block 3: FAILED$
+^\[main.coverage.4\] file main.c line 15 function main block 4: FAILED$
+^\[main.coverage.5\] file main.c line 15 function main block 5: FAILED$
+^\[main.coverage.6\] file main.c line 16 function main block 6: FAILED$
+^\[main.coverage.7\] file main.c line 17 function main block 7: SATISFIED$
+^\[foo.coverage.1\] file main.c line 6 function foo block 1: FAILED$
+^\[foo.coverage.2\] file main.c line 7 function foo block 2: FAILED$
+^\*\* 3 of 9 covered (33.3%)
+--
+^warning: ignoring
diff --git a/regression/cbmc-cover/location16/main.c b/regression/cbmc-cover/location16/main.c
new file mode 100644
index 00000000000..6334e4c8e88
--- /dev/null
+++ b/regression/cbmc-cover/location16/main.c
@@ -0,0 +1,21 @@
+#include <assert.h>
+
+int func(int a)
+{
+  int b = a*2;
+  return b;
+
+  if (b < 10)
+  {
+    b += 10;
+  }
+
+  assert(0);
+
+  return b;
+}
+
+int main(void)
+{
+  func(2);
+}
diff --git a/regression/cbmc-cover/location16/test.desc b/regression/cbmc-cover/location16/test.desc
new file mode 100644
index 00000000000..bb81dddf43c
--- /dev/null
+++ b/regression/cbmc-cover/location16/test.desc
@@ -0,0 +1,17 @@
+CORE
+main.c
+--cover location
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.1\] file main.c line 20 function main block 1: SATISFIED$
+^\[main.coverage.2\] file main.c line 21 function main block 2: SATISFIED$
+^\[func.coverage.1\] file main.c line 5 function func block 1: SATISFIED$
+^\[func.coverage.2\] file main.c line 8 function func block 2: FAILED$
+^\[func.coverage.3\] file main.c line 10 function func block 3: FAILED$
+^\[func.coverage.4\] file main.c line 13 function func block 4: FAILED$
+^\[func.coverage.5\] file main.c line 13 function func block 5: FAILED$
+^\[func.coverage.6\] file main.c line 15 function func block 6: FAILED$
+^\[func.coverage.7\] file main.c line 16 function func block 7: SATISFIED$
+^\*\* 4 of 9 covered (44.4%)
+--
+^warning: ignoring
diff --git a/regression/cbmc-cover/location2/main.c b/regression/cbmc-cover/location2/main.c
new file mode 100644
index 00000000000..9a0b65d37f6
--- /dev/null
+++ b/regression/cbmc-cover/location2/main.c
@@ -0,0 +1,13 @@
+int main()
+{
+  int i, j;
+
+  i = 1;
+
+  if(j > 0)
+    j += i;
+  else
+    j = 0;
+
+  assert(i != j);
+}
diff --git a/regression/cbmc-cover/location2/main.json b/regression/cbmc-cover/location2/main.json
new file mode 100644
index 00000000000..1fd3d2cd7ba
--- /dev/null
+++ b/regression/cbmc-cover/location2/main.json
@@ -0,0 +1,2 @@
+[ { "file": "main.c", "function": "main", "lines": [ {"number": 3}, {"number": 8}, {"number": 10}, {"number": 12} ] }
+]
diff --git a/regression/cbmc-cover/location2/test.desc b/regression/cbmc-cover/location2/test.desc
new file mode 100644
index 00000000000..010956452e1
--- /dev/null
+++ b/regression/cbmc-cover/location2/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--cover location --existing-coverage main.json
+^EXIT=0$
+^SIGNAL=0$
+^\*\* 0 of 0 covered (100.0%)
+--
+^warning: ignoring
diff --git a/regression/cbmc-cover/location3/main.c b/regression/cbmc-cover/location3/main.c
new file mode 100644
index 00000000000..9a0b65d37f6
--- /dev/null
+++ b/regression/cbmc-cover/location3/main.c
@@ -0,0 +1,13 @@
+int main()
+{
+  int i, j;
+
+  i = 1;
+
+  if(j > 0)
+    j += i;
+  else
+    j = 0;
+
+  assert(i != j);
+}
diff --git a/regression/cbmc-cover/location3/main.json b/regression/cbmc-cover/location3/main.json
new file mode 100644
index 00000000000..dc7fb615202
--- /dev/null
+++ b/regression/cbmc-cover/location3/main.json
@@ -0,0 +1,2 @@
+[ { "file": "main.c", "function": "main", "lines": [ {"number": 3}, {"number": 8}, {"number": 12} ] }
+]
diff --git a/regression/cbmc-cover/location3/test.desc b/regression/cbmc-cover/location3/test.desc
new file mode 100644
index 00000000000..a621fc0f941
--- /dev/null
+++ b/regression/cbmc-cover/location3/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--cover location --existing-coverage main.json
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.1\] file main.c line 10 function main block 3: SATISFIED$
+^\*\* 1 of 1 covered (100.0%)
+--
+^warning: ignoring
diff --git a/regression/cbmc-cover/location4/main.c b/regression/cbmc-cover/location4/main.c
new file mode 100644
index 00000000000..ca92d1abc09
--- /dev/null
+++ b/regression/cbmc-cover/location4/main.c
@@ -0,0 +1,41 @@
+#include <stdio.h>
+#include <assert.h>
+#include "single-linked-list.h"
+
+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;
+
+	printf("list all elements: ");
+	while(mylist)
+	{
+		printf("%d ", mylist->key);
+		mylist = mylist->next;
+	}
+	printf("\n");
+
+	temp = search_list(mylist,2);
+	printf("search for element 2: %s\n", temp->key == 2 ? "found" : "not found");
+	assert(temp->key == 2);
+
+	delete_list(temp);
+
+	mylist = head;
+
+	printf("list all elements except 2: ");
+	while(mylist)
+	{
+		printf("%d ", mylist->key);
+		mylist = mylist->next;
+	}
+	printf("\n");
+}
diff --git a/regression/cbmc-cover/location4/main.json b/regression/cbmc-cover/location4/main.json
new file mode 100644
index 00000000000..d5b80c03a30
--- /dev/null
+++ b/regression/cbmc-cover/location4/main.json
@@ -0,0 +1,7 @@
+[ { "file": "<builtin-library-free>", "function": "free", "lines": [ {"number": 22} ] },
+{ "file": "main.c", "function": "main", "lines": [ {"number": 8}, {"number": 12}, {"number": 13}, {"number": 14}, {"number": 16}, {"number": 19}, {"number": 21}, {"number": 24}, {"number": 26}, {"number": 30}, {"number": 32}, {"number": 35}, {"number": 37}, {"number": 40} ] },
+{"file": "single-linked-list.c", "function": "search_list", "lines": [ {"number": 9}, {"number": 10}, {"number": 15} ] },
+{"file": "single-linked-list.c", "function": "delete_list", "lines": [ {"number": 19}, {"number": 23}, {"number": 24}, {"number": 25}, {"number": 29}, {"number": 31}, {"number": 37}, {"number": 40}, {"number": 45}, {"number": 48} ] },
+{"file": "single-linked-list.c", "function": "insert_list", "lines": [ {"number": 37}, {"number": 40}, {"number": 45}, {"number": 48} ] }
+]
+
diff --git a/regression/cbmc-cover/location4/single-linked-list.c b/regression/cbmc-cover/location4/single-linked-list.c
new file mode 100644
index 00000000000..30fe7a0ced0
--- /dev/null
+++ b/regression/cbmc-cover/location4/single-linked-list.c
@@ -0,0 +1,51 @@
+#include <stdio.h>
+#include <stdlib.h>
+#include <assert.h>
+
+#include "single-linked-list.h"
+
+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;
+}
+
diff --git a/regression/cbmc-cover/location4/single-linked-list.h b/regression/cbmc-cover/location4/single-linked-list.h
new file mode 100644
index 00000000000..4d274a6a1e2
--- /dev/null
+++ b/regression/cbmc-cover/location4/single-linked-list.h
@@ -0,0 +1,14 @@
+#ifndef SINGLE_LINKED_LIST_H_
+#define SINGLE_LINKED_LIST_H_
+
+typedef struct list {
+	int key;
+	struct list *next;
+} mlist;
+
+mlist *head;
+mlist* search_list(mlist *l, int k);
+int delete_list(mlist *l);
+int insert_list(mlist *l, int k);
+
+#endif /* SINGLE_LINKED_LIST_H_ */
diff --git a/regression/cbmc-cover/location4/test.desc b/regression/cbmc-cover/location4/test.desc
new file mode 100644
index 00000000000..d9eaa8195c0
--- /dev/null
+++ b/regression/cbmc-cover/location4/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+single-linked-list.c --cover location --existing-coverage main.json --unwind 2
+^EXIT=0$
+^SIGNAL=0$
+^\*\* 0 of 1 covered (0.0%)
+--
+^warning: ignoring
diff --git a/regression/cbmc-cover/location5/main.c b/regression/cbmc-cover/location5/main.c
new file mode 100644
index 00000000000..ca92d1abc09
--- /dev/null
+++ b/regression/cbmc-cover/location5/main.c
@@ -0,0 +1,41 @@
+#include <stdio.h>
+#include <assert.h>
+#include "single-linked-list.h"
+
+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;
+
+	printf("list all elements: ");
+	while(mylist)
+	{
+		printf("%d ", mylist->key);
+		mylist = mylist->next;
+	}
+	printf("\n");
+
+	temp = search_list(mylist,2);
+	printf("search for element 2: %s\n", temp->key == 2 ? "found" : "not found");
+	assert(temp->key == 2);
+
+	delete_list(temp);
+
+	mylist = head;
+
+	printf("list all elements except 2: ");
+	while(mylist)
+	{
+		printf("%d ", mylist->key);
+		mylist = mylist->next;
+	}
+	printf("\n");
+}
diff --git a/regression/cbmc-cover/location5/main.json b/regression/cbmc-cover/location5/main.json
new file mode 100644
index 00000000000..86c5b8fd0ee
--- /dev/null
+++ b/regression/cbmc-cover/location5/main.json
@@ -0,0 +1,7 @@
+[ { "file": "<builtin-library-free>", "function": "free", "lines": [ {"number": 22} ] },
+{ "file": "main.c", "function": "main", "lines": [ {"number": 8}, {"number": 12}, {"number": 13}, {"number": 16}, {"number": 19}, {"number": 21}, {"number": 24}, {"number": 26}, {"number": 30}, {"number": 32}, {"number": 35}, {"number": 37}, {"number": 40} ] },
+{"file": "single-linked-list.c", "function": "search_list", "lines": [ {"number": 9}, {"number": 10}, {"number": 15} ] },
+{"file": "single-linked-list.c", "function": "delete_list", "lines": [ {"number": 19}, {"number": 23}, {"number": 24}, {"number": 25}, {"number": 29}, {"number": 31}, {"number": 37}, {"number": 40}, {"number": 45}, {"number": 48} ] },
+{"file": "single-linked-list.c", "function": "insert_list", "lines": [ {"number": 37}, {"number": 40}, {"number": 45}, {"number": 48} ] }
+]
+
diff --git a/regression/cbmc-cover/location5/single-linked-list.c b/regression/cbmc-cover/location5/single-linked-list.c
new file mode 100644
index 00000000000..30fe7a0ced0
--- /dev/null
+++ b/regression/cbmc-cover/location5/single-linked-list.c
@@ -0,0 +1,51 @@
+#include <stdio.h>
+#include <stdlib.h>
+#include <assert.h>
+
+#include "single-linked-list.h"
+
+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;
+}
+
diff --git a/regression/cbmc-cover/location5/single-linked-list.h b/regression/cbmc-cover/location5/single-linked-list.h
new file mode 100644
index 00000000000..4d274a6a1e2
--- /dev/null
+++ b/regression/cbmc-cover/location5/single-linked-list.h
@@ -0,0 +1,14 @@
+#ifndef SINGLE_LINKED_LIST_H_
+#define SINGLE_LINKED_LIST_H_
+
+typedef struct list {
+	int key;
+	struct list *next;
+} mlist;
+
+mlist *head;
+mlist* search_list(mlist *l, int k);
+int delete_list(mlist *l);
+int insert_list(mlist *l, int k);
+
+#endif /* SINGLE_LINKED_LIST_H_ */
diff --git a/regression/cbmc-cover/location5/test.desc b/regression/cbmc-cover/location5/test.desc
new file mode 100644
index 00000000000..16c53355a24
--- /dev/null
+++ b/regression/cbmc-cover/location5/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+single-linked-list.c --cover location --existing-coverage main.json --unwind 2
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.1\] file main.c line 14 function main block 4: SATISFIED$
+^\*\* 1 of 2 covered (50.0%)
+--
+^warning: ignoring
diff --git a/regression/cbmc-cover/location6/if_expr1.class b/regression/cbmc-cover/location6/if_expr1.class
new file mode 100644
index 00000000000..80db60b2bb1
Binary files /dev/null and b/regression/cbmc-cover/location6/if_expr1.class differ
diff --git a/regression/cbmc-cover/location6/if_expr1.java b/regression/cbmc-cover/location6/if_expr1.java
new file mode 100644
index 00000000000..dcb703d5030
--- /dev/null
+++ b/regression/cbmc-cover/location6/if_expr1.java
@@ -0,0 +1,12 @@
+class if_expr1
+{
+  static public void main(String[] args) throws java.io.IOException
+  {
+    int x=System.in.read();
+    int y=x==10?11:9;
+    if(x==10)
+      assert y==11;
+    else
+      assert y==9;
+  }
+};
diff --git a/regression/cbmc-cover/location6/if_expr1.json b/regression/cbmc-cover/location6/if_expr1.json
new file mode 100644
index 00000000000..09d4eaa4fca
--- /dev/null
+++ b/regression/cbmc-cover/location6/if_expr1.json
@@ -0,0 +1,3 @@
+[ { "file": "if_expr1.java", "lines": [ {"number": 1}, {"number": 5}, {"number": 6}, {"number": 8}, {"number": 10}, {"number": 11} ] }
+]
+
diff --git a/regression/cbmc-cover/location6/test.desc b/regression/cbmc-cover/location6/test.desc
new file mode 100644
index 00000000000..b47c983d68a
--- /dev/null
+++ b/regression/cbmc-cover/location6/test.desc
@@ -0,0 +1,8 @@
+CORE
+if_expr1.class
+--cover location --existing-coverage if_expr1.json
+^EXIT=0$
+^SIGNAL=0$
+^\*\* 0 of 0 covered (100.0%)$
+--
+^warning: ignoring
diff --git a/regression/cbmc-cover/location7/if_expr1.class b/regression/cbmc-cover/location7/if_expr1.class
new file mode 100644
index 00000000000..80db60b2bb1
Binary files /dev/null and b/regression/cbmc-cover/location7/if_expr1.class differ
diff --git a/regression/cbmc-cover/location7/if_expr1.java b/regression/cbmc-cover/location7/if_expr1.java
new file mode 100644
index 00000000000..dcb703d5030
--- /dev/null
+++ b/regression/cbmc-cover/location7/if_expr1.java
@@ -0,0 +1,12 @@
+class if_expr1
+{
+  static public void main(String[] args) throws java.io.IOException
+  {
+    int x=System.in.read();
+    int y=x==10?11:9;
+    if(x==10)
+      assert y==11;
+    else
+      assert y==9;
+  }
+};
diff --git a/regression/cbmc-cover/location7/if_expr1.json b/regression/cbmc-cover/location7/if_expr1.json
new file mode 100644
index 00000000000..1d1bbb6f552
--- /dev/null
+++ b/regression/cbmc-cover/location7/if_expr1.json
@@ -0,0 +1,2 @@
+[ { "file": "if_expr1.java", "lines": [ {"number": 1}, {"number": 5}, {"number": 6}, {"number": 8}, {"number": 10} ] }
+]
diff --git a/regression/cbmc-cover/location7/test.desc b/regression/cbmc-cover/location7/test.desc
new file mode 100644
index 00000000000..ea38fff1940
--- /dev/null
+++ b/regression/cbmc-cover/location7/test.desc
@@ -0,0 +1,9 @@
+CORE
+if_expr1.class
+--cover location --existing-coverage if_expr1.json
+^EXIT=0$
+^SIGNAL=0$
+^\[coverage.1\] file if_expr1.java line 11 block 14: SATISFIED$
+^\*\* 1 of 1 covered (100.0%)
+--
+^warning: ignoring
diff --git a/regression/cbmc-cover/location8/A.class b/regression/cbmc-cover/location8/A.class
new file mode 100644
index 00000000000..6ee0b76170f
Binary files /dev/null and b/regression/cbmc-cover/location8/A.class differ
diff --git a/regression/cbmc-cover/location8/B.class b/regression/cbmc-cover/location8/B.class
new file mode 100644
index 00000000000..bd7646294d1
Binary files /dev/null and b/regression/cbmc-cover/location8/B.class differ
diff --git a/regression/cbmc-cover/location8/if_acmp1.class b/regression/cbmc-cover/location8/if_acmp1.class
new file mode 100644
index 00000000000..9bca48ecdc4
Binary files /dev/null and b/regression/cbmc-cover/location8/if_acmp1.class differ
diff --git a/regression/cbmc-cover/location8/if_acmp1.java b/regression/cbmc-cover/location8/if_acmp1.java
new file mode 100644
index 00000000000..ecf66781336
--- /dev/null
+++ b/regression/cbmc-cover/location8/if_acmp1.java
@@ -0,0 +1,36 @@
+class A {
+}
+
+class B {
+}
+
+class if_acmp1
+{
+  private static B get_B() {
+    B b = new B();
+    return b;
+  }
+
+  public static void main(String[] args) {
+    A a0 = new A();
+    A a1 = new A();
+    A a2 = new A();
+    A a3 = new A();
+    A a4 = new A();
+    assert a0 == a0;
+    assert a1 == a1;
+    assert a2 == a2;
+    assert a3 == a3;
+    assert a4 == a4;
+    assert a1 != a2;
+    assert a2 != a3;
+    assert a3 != a4;
+    assert a0 != null;
+    A a5 = null;
+    assert a5 == null;
+    B b = get_B();
+    Object o0 = a0;
+    Object o1 = b;
+    assert o0 != o1;
+  }
+}
diff --git a/regression/cbmc-cover/location8/if_acmp1.json b/regression/cbmc-cover/location8/if_acmp1.json
new file mode 100644
index 00000000000..de4ebb6c29d
--- /dev/null
+++ b/regression/cbmc-cover/location8/if_acmp1.json
@@ -0,0 +1,3 @@
+[ { "file": "if_acmp1.java", "lines": [ {"number": 4}, {"number": 1}, {"number": 10}, {"number": 7}, {"number": 15}, {"number": 16}, {"number": 17}, {"number": 18}, {"number": 19}, {"number": 20}, {"number": 21}, {"number": 22}, {"number": 23}, {"number": 24}, {"number": 25}, {"number": 26}, {"number": 27}, {"number": 28}, {"number": 29}, {"number": 30}, {"number": 31}, {"number": 34}, {"number": 35} ] }
+]
+
diff --git a/regression/cbmc-cover/location8/test.desc b/regression/cbmc-cover/location8/test.desc
new file mode 100644
index 00000000000..bb29eb24d60
--- /dev/null
+++ b/regression/cbmc-cover/location8/test.desc
@@ -0,0 +1,8 @@
+CORE
+if_acmp1.class
+--cover location --existing-coverage if_acmp1.json
+^EXIT=0$
+^SIGNAL=0$
+^\*\* 0 of 0 covered (100.0%)
+--
+^warning: ignoring
diff --git a/regression/cbmc-cover/location9/A.class b/regression/cbmc-cover/location9/A.class
new file mode 100644
index 00000000000..6ee0b76170f
Binary files /dev/null and b/regression/cbmc-cover/location9/A.class differ
diff --git a/regression/cbmc-cover/location9/B.class b/regression/cbmc-cover/location9/B.class
new file mode 100644
index 00000000000..bd7646294d1
Binary files /dev/null and b/regression/cbmc-cover/location9/B.class differ
diff --git a/regression/cbmc-cover/location9/if_acmp1.class b/regression/cbmc-cover/location9/if_acmp1.class
new file mode 100644
index 00000000000..9bca48ecdc4
Binary files /dev/null and b/regression/cbmc-cover/location9/if_acmp1.class differ
diff --git a/regression/cbmc-cover/location9/if_acmp1.java b/regression/cbmc-cover/location9/if_acmp1.java
new file mode 100644
index 00000000000..ecf66781336
--- /dev/null
+++ b/regression/cbmc-cover/location9/if_acmp1.java
@@ -0,0 +1,36 @@
+class A {
+}
+
+class B {
+}
+
+class if_acmp1
+{
+  private static B get_B() {
+    B b = new B();
+    return b;
+  }
+
+  public static void main(String[] args) {
+    A a0 = new A();
+    A a1 = new A();
+    A a2 = new A();
+    A a3 = new A();
+    A a4 = new A();
+    assert a0 == a0;
+    assert a1 == a1;
+    assert a2 == a2;
+    assert a3 == a3;
+    assert a4 == a4;
+    assert a1 != a2;
+    assert a2 != a3;
+    assert a3 != a4;
+    assert a0 != null;
+    A a5 = null;
+    assert a5 == null;
+    B b = get_B();
+    Object o0 = a0;
+    Object o1 = b;
+    assert o0 != o1;
+  }
+}
diff --git a/regression/cbmc-cover/location9/if_acmp1.json b/regression/cbmc-cover/location9/if_acmp1.json
new file mode 100644
index 00000000000..8d48cb86fa0
--- /dev/null
+++ b/regression/cbmc-cover/location9/if_acmp1.json
@@ -0,0 +1,3 @@
+[ { "file": "if_acmp1.java", "lines": [ {"number": 4}, {"number": 1}, {"number": 10}, {"number": 7}, {"number": 15}, {"number": 17}, {"number": 20}, {"number": 21}, {"number": 22}, {"number": 23}, {"number": 24}, {"number": 25}, {"number": 26}, {"number": 27}, {"number": 28}, {"number": 29}, {"number": 30}, {"number": 31}, {"number": 34}, {"number": 35} ] }
+]
+
diff --git a/regression/cbmc-cover/location9/test.desc b/regression/cbmc-cover/location9/test.desc
new file mode 100644
index 00000000000..b80a98c1894
--- /dev/null
+++ b/regression/cbmc-cover/location9/test.desc
@@ -0,0 +1,11 @@
+CORE
+if_acmp1.class
+--cover location --existing-coverage if_acmp1.json
+^EXIT=0$
+^SIGNAL=0$
+^\[coverage.1\] file if_acmp1.java line 16 block 3: SATISFIED$
+^\[coverage.2\] file if_acmp1.java line 18 block 5: SATISFIED$
+^\[coverage.3\] file if_acmp1.java line 19 block 6: SATISFIED$
+^\*\* 3 of 3 covered (100.0%)
+--
+^warning: ignoring
diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile
index 8440c92fa1b..8bd53417622 100644
--- a/src/cbmc/Makefile
+++ b/src/cbmc/Makefile
@@ -27,6 +27,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../xmllang/xmllang$(LIBEXT) \
       ../assembler/assembler$(LIBEXT) \
       ../solvers/solvers$(LIBEXT) \
+      ../json/json$(LIBEXT) \
       ../util/util$(LIBEXT)
 
 INCLUDES= -I ..
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 3b0d7b5bc6a..05286737664 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -458,6 +458,10 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
 
   if(cmdline.isset("graphml-cex"))
     options.set_option("graphml-cex", cmdline.get_value("graphml-cex"));
+
+  if(cmdline.isset("existing-coverage"))
+    options.set_option("existing-coverage", cmdline.get_value("existing-coverage"));
+
 }
 
 /*******************************************************************\
@@ -945,7 +949,7 @@ bool cbmc_parse_optionst::process_goto_program(
     
     // add loop ids
     goto_functions.compute_loop_numbers();
-    
+
     // instrument cover goals
     
     if(cmdline.isset("cover"))
@@ -975,9 +979,21 @@ bool cbmc_parse_optionst::process_goto_program(
         error() << "unknown coverage criterion" << eom;
         return true;
       }
-          
+
+
+      // check existing test goals
+      coverage_goalst goals;
+      if(cmdline.isset("existing-coverage"))
+      {
+        status() << "Check existing coverage goals" << eom;
+        //get file with covered test goals
+        const std::string coverage=cmdline.get_value("existing-coverage");
+        //get a coverage_goalst object
+        goals = coverage_goalst::get_coverage_goals(coverage,get_message_handler());;
+      }
+
       status() << "Instrumenting coverage goals" << eom;
-      instrument_cover_goals(symbol_table, goto_functions, c);
+      instrument_cover_goals(symbol_table, goto_functions, c, goals);
       goto_functions.update();
     }
 
@@ -1140,6 +1156,7 @@ void cbmc_parse_optionst::help()
     " --no-assumptions             ignore user assumptions\n"
     " --error-label label          check that label is unreachable\n"
     " --cover CC                   create test-suite with coverage criterion CC\n"
+    " --existing-coverage file     instrument non-covered test goals\n"
     " --mm MM                      memory consistency model for concurrent programs\n"
     "\n"
     "Java Bytecode frontend options:\n"
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
index 33fe0ba5175..1882f57a738 100644
--- a/src/cbmc/cbmc_parse_options.h
+++ b/src/cbmc/cbmc_parse_options.h
@@ -54,6 +54,7 @@ class optionst;
   "(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
   "(graphml-cex):" \
   "(localize-faults)(localize-faults-method):" \
+  "(existing-coverage):" \
   "(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear
 
 class cbmc_parse_optionst:
diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile
index fd44907bb11..fddf70a5d51 100644
--- a/src/goto-instrument/Makefile
+++ b/src/goto-instrument/Makefile
@@ -37,6 +37,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../langapi/langapi$(LIBEXT) \
       ../xmllang/xmllang$(LIBEXT) \
       ../util/util$(LIBEXT) \
+      ../json/json$(LIBEXT) \
       ../solvers/solvers$(LIBEXT)
 
 INCLUDES= -I ..
diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp
index bb6e70d443e..0fe251bec04 100644
--- a/src/goto-instrument/cover.cpp
+++ b/src/goto-instrument/cover.cpp
@@ -8,6 +8,8 @@ Date: May 2016
 
 \*******************************************************************/
 
+#include <iostream>
+
 #include <algorithm>
 #include <iterator>
 
@@ -15,6 +17,8 @@ Date: May 2016
 #include <util/i2string.h>
 #include <util/expr_util.h>
 
+#include <json/json_parser.h>
+
 #include "cover.h"
 
 class basic_blockst
@@ -66,6 +70,123 @@ class basic_blockst
   }
 };
 
+/*******************************************************************\
+
+Function: coverage_goalst::get_coverage
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+coverage_goalst coverage_goalst::get_coverage_goals(const std::string &coverage,
+                                   message_handlert &message_handler)
+{
+  jsont json;
+  coverage_goalst goals;
+  source_locationt source_location;
+
+  //check coverage file
+  if(parse_json(coverage, message_handler, json))
+  {
+    messaget message(message_handler);
+    message.error() << coverage << " file is not a valid json file"
+                    << messaget::eom;
+    exit(0);
+  }
+
+  //make sure that we have an array of elements
+  if(!json.is_array())
+  {
+    messaget message(message_handler);
+    message.error() << "expecting an array in the " <<  coverage << " file, but got "
+                    << json << messaget::eom;
+    exit(0);
+  }
+
+  irep_idt file, function, line;
+  for(jsont::arrayt::const_iterator
+      it=json.array.begin();
+      it!=json.array.end();
+      it++)
+  {
+
+    //get the file of each existing goal
+    file=(*it)["file"].value;
+    source_location.set_file(file);
+
+    //get the function of each existing goal
+    function=(*it)["function"].value;
+    source_location.set_function(function);
+
+    //get the lines array
+    if ((*it)["lines"].is_array())
+  	{
+  	  for(jsont::arrayt::const_iterator
+  	      itg=(*it)["lines"].array.begin();
+  	      itg!=(*it)["lines"].array.end();
+  	      itg++)
+  	  {
+        //get the line of each existing goal
+        line=(*itg)["number"].value;
+        source_location.set_line(line);
+        goals.set_goals(source_location);
+  	  }
+  	}
+  }
+  return goals;
+}
+
+/*******************************************************************\
+
+Function: coverage_goalst::set_goals
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void coverage_goalst::set_goals(source_locationt goal)
+{
+  existing_goals.push_back(goal);
+}
+
+/*******************************************************************\
+
+Function: coverage_goalst::is_existing_goal
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool coverage_goalst::is_existing_goal(source_locationt source_location)
+{
+  std::vector<source_locationt>::iterator it = existing_goals.begin();
+  while (it!=existing_goals.end())
+  {
+    if (!source_location.get_file().compare(it->get_file()) &&
+    	!source_location.get_function().compare(it->get_function()) &&
+    	!source_location.get_line().compare(it->get_line()))
+      break;
+    ++it;
+  }
+  if(it == existing_goals.end())
+    return true;
+  else
+    return false;
+}
+
+
 /*******************************************************************\
 
 Function: as_string
@@ -1058,7 +1179,8 @@ Function: instrument_cover_goals
 void instrument_cover_goals(
   const symbol_tablet &symbol_table,
   goto_programt &goto_program,
-  coverage_criteriont criterion)
+  coverage_criteriont criterion,
+  coverage_goalst &goals)
 {
   const namespacet ns(symbol_table);
   basic_blockst basic_blocks(goto_program);
@@ -1120,7 +1242,9 @@ void instrument_cover_goals(
           source_locationt source_location=
             basic_blocks.source_location_map[block_nr];
           
-          if(!source_location.get_file().empty() &&
+          //check whether the current goal already exists
+          if(goals.is_existing_goal(source_location) &&
+        	 !source_location.get_file().empty() &&
              source_location.get_file()[0]!='<')
           {
             std::string comment="block "+b;
@@ -1354,7 +1478,8 @@ Function: instrument_cover_goals
 void instrument_cover_goals(
   const symbol_tablet &symbol_table,
   goto_functionst &goto_functions,
-  coverage_criteriont criterion)
+  coverage_criteriont criterion,
+  coverage_goalst &goals)
 {
   Forall_goto_functions(f_it, goto_functions)
   {
@@ -1362,6 +1487,37 @@ void instrument_cover_goals(
        f_it->first=="__CPROVER_initialize")
       continue;
       
-    instrument_cover_goals(symbol_table, f_it->second.body, criterion);
+    instrument_cover_goals(symbol_table, f_it->second.body,
+    					   criterion, goals);
+  }
+}
+
+/*******************************************************************\
+
+Function: instrument_cover_goals
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void instrument_cover_goals(
+  const symbol_tablet &symbol_table,
+  goto_functionst &goto_functions,
+  coverage_criteriont criterion)
+{
+  Forall_goto_functions(f_it, goto_functions)
+  {
+    if(f_it->first==ID__start ||
+       f_it->first=="__CPROVER_initialize")
+      continue;
+
+    //empty set of existing goals
+    coverage_goalst goals;
+    instrument_cover_goals(symbol_table, f_it->second.body,
+    					   criterion, goals);
   }
 }
diff --git a/src/goto-instrument/cover.h b/src/goto-instrument/cover.h
index cf51972f6e6..9eb85b3c7d2 100644
--- a/src/goto-instrument/cover.h
+++ b/src/goto-instrument/cover.h
@@ -13,6 +13,18 @@ Date: May 2016
 
 #include <goto-programs/goto_model.h>
 
+class coverage_goalst
+{
+public:
+  static coverage_goalst get_coverage_goals(const std::string &coverage,
+                                      message_handlert &message_handler);
+  void set_goals(source_locationt goal);
+  bool is_existing_goal(source_locationt source_location);
+
+private:
+  std::vector<source_locationt> existing_goals;
+};
+
 enum class coverage_criteriont {
   LOCATION, BRANCH, DECISION, CONDITION,
   PATH, MCDC, ASSERTION, COVER };
@@ -20,7 +32,14 @@ enum class coverage_criteriont {
 void instrument_cover_goals(
   const symbol_tablet &symbol_table,
   goto_programt &goto_program,
-  coverage_criteriont);
+  coverage_criteriont,
+  coverage_goalst &goals);
+
+void instrument_cover_goals(
+  const symbol_tablet &symbol_table,
+  goto_functionst &goto_functions,
+  coverage_criteriont,
+  coverage_goalst &goals);
 
 void instrument_cover_goals(
   const symbol_tablet &symbol_table,
diff --git a/src/symex/Makefile b/src/symex/Makefile
index 1f8e27ce063..42632b58d7b 100644
--- a/src/symex/Makefile
+++ b/src/symex/Makefile
@@ -16,6 +16,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
        ../goto-symex/rewrite_union$(OBJEXT) \
        ../pointer-analysis/dereference$(OBJEXT) \
        ../goto-instrument/cover$(OBJEXT) \
+       ../json/json$(LIBEXT) \
        ../path-symex/path-symex$(LIBEXT)
 
 INCLUDES= -I ..