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