diff --git a/regression/cbmc-cover/mcdc10/main.c b/regression/cbmc-cover/mcdc10/main.c
new file mode 100644
index 00000000000..703132cb4f2
--- /dev/null
+++ b/regression/cbmc-cover/mcdc10/main.c
@@ -0,0 +1,19 @@
+int main()
+{
+  _Bool A, B, C;
+
+  __CPROVER_input("cold", A);
+  __CPROVER_input("raining", B);
+  __CPROVER_input("windy", C);
+
+  if ( A || B || C )
+  {
+  /* instructions */
+  }
+  else
+  {
+  /* instructions */
+  }
+
+  return 1;
+}
diff --git a/regression/cbmc-cover/mcdc10/test.desc b/regression/cbmc-cover/mcdc10/test.desc
new file mode 100644
index 00000000000..daf502e74af
--- /dev/null
+++ b/regression/cbmc-cover/mcdc10/test.desc
@@ -0,0 +1,13 @@
+CORE
+main.c
+--cover mcdc
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.1\] file main.c line 9 function main MC/DC independence condition `A != FALSE && !(B != FALSE) && !(C != FALSE).*: SATISFIED$
+^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition `!(A != FALSE) && B != FALSE && !(C != FALSE).*: SATISFIED$
+^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition `!(A != FALSE) && !(B != FALSE) && C != FALSE.*: SATISFIED$
+^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition `!(A != FALSE) && !(B != FALSE) && !(C != FALSE).*: SATISFIED$
+^\*\* .* of .* covered (100.0%)$
+^\*\* Used 5 iterations$
+--
+^warning: ignoring
diff --git a/regression/cbmc-cover/mcdc11/main.c b/regression/cbmc-cover/mcdc11/main.c
new file mode 100644
index 00000000000..fc4970ab459
--- /dev/null
+++ b/regression/cbmc-cover/mcdc11/main.c
@@ -0,0 +1,27 @@
+int main()
+{
+  _Bool A, B, C, D;
+
+  __CPROVER_input("A", A);
+  __CPROVER_input("B", B);
+  __CPROVER_input("C", C);
+  __CPROVER_input("D", D);
+
+  if (A && B)
+  {
+    if (C || D)
+    {
+      /* instructions */
+    }
+    else
+    {
+      /* instructions */
+    }
+  }
+  else
+  {
+    /* instructions */
+  }
+
+  return 1;
+}
diff --git a/regression/cbmc-cover/mcdc11/test.desc b/regression/cbmc-cover/mcdc11/test.desc
new file mode 100644
index 00000000000..616b3249b0d
--- /dev/null
+++ b/regression/cbmc-cover/mcdc11/test.desc
@@ -0,0 +1,15 @@
+CORE
+main.c
+--cover mcdc
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.1\] file main.c line 10 function main MC/DC independence condition `A != FALSE && B != FALSE.*: SATISFIED$
+^\[main.coverage.2\] file main.c line 10 function main MC/DC independence condition `A != FALSE && !(B != FALSE).*: SATISFIED$
+^\[main.coverage.3\] file main.c line 10 function main MC/DC independence condition `!(A != FALSE) && B != FALSE.*: SATISFIED$
+^\[main.coverage.10\] file main.c line 12 function main MC/DC independence condition `C != FALSE && !(D != FALSE).*: SATISFIED$
+^\[main.coverage.11\] file main.c line 12 function main MC/DC independence condition `!(C != FALSE) && D != FALSE.*: SATISFIED$
+^\[main.coverage.12\] file main.c line 12 function main MC/DC independence condition `!(C != FALSE) && !(D != FALSE).*: SATISFIED$
+^\*\* .* of .* covered (100.0%)$
+^\*\* Used 6 iterations$
+--
+^warning: ignoring
diff --git a/regression/cbmc-cover/mcdc12/main.c b/regression/cbmc-cover/mcdc12/main.c
new file mode 100644
index 00000000000..f0f79018416
--- /dev/null
+++ b/regression/cbmc-cover/mcdc12/main.c
@@ -0,0 +1,36 @@
+int main()
+{
+  _Bool A, B, C, D, E, F;
+
+  __CPROVER_input("A", A);
+  __CPROVER_input("B", B);
+  __CPROVER_input("C", C);
+  __CPROVER_input("D", D);
+  __CPROVER_input("E", D);
+  __CPROVER_input("F", D);
+
+  if (A && B)
+  {
+    if (C || D)
+    {
+      /* instructions */
+    }
+    else
+    {
+      /* instructions */
+    }
+  }
+  else
+  {
+    if (E || F)
+    {
+      /* instructions */
+    }
+    else
+    {
+      /* instructions */
+    }
+  }
+
+  return 1;
+}
diff --git a/regression/cbmc-cover/mcdc12/test.desc b/regression/cbmc-cover/mcdc12/test.desc
new file mode 100644
index 00000000000..44e823e13c4
--- /dev/null
+++ b/regression/cbmc-cover/mcdc12/test.desc
@@ -0,0 +1,18 @@
+CORE
+main.c
+--cover mcdc
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.1\] file main.c line 12 function main MC/DC independence condition `A != FALSE && B != FALSE.*: SATISFIED$
+^\[main.coverage.2\] file main.c line 12 function main MC/DC independence condition `A != FALSE && !(B != FALSE).*: SATISFIED$
+^\[main.coverage.3\] file main.c line 12 function main MC/DC independence condition `!(A != FALSE) && B != FALSE.*: SATISFIED$
+^\[main.coverage.10\] file main.c line 14 function main MC/DC independence condition `C != FALSE && !(D != FALSE).*: SATISFIED$
+^\[main.coverage.11\] file main.c line 14 function main MC/DC independence condition `!(C != FALSE) && D != FALSE.*: SATISFIED$
+^\[main.coverage.12\] file main.c line 14 function main MC/DC independence condition `!(C != FALSE) && !(D != FALSE).*: SATISFIED$
+^\[main.coverage.19\] file main.c line 25 function main MC/DC independence condition `E != FALSE && !(F != FALSE).*: SATISFIED$
+^\[main.coverage.20\] file main.c line 25 function main MC/DC independence condition `!(E != FALSE) && F != FALSE.*: SATISFIED$
+^\[main.coverage.21\] file main.c line 25 function main MC/DC independence condition `!(E != FALSE) && !(F != FALSE).*: SATISFIED$
+^\*\* .* of .* covered (100.0%)$
+^\*\* Used 10 iterations$
+--
+^warning: ignoring
diff --git a/regression/cbmc-cover/mcdc13/main.c b/regression/cbmc-cover/mcdc13/main.c
new file mode 100644
index 00000000000..d875b00235f
--- /dev/null
+++ b/regression/cbmc-cover/mcdc13/main.c
@@ -0,0 +1,15 @@
+int main()
+{
+  _Bool A, B, C;
+
+  __CPROVER_input("A", A);
+  __CPROVER_input("B", B);
+  __CPROVER_input("C", C);
+
+  if (A && B && C)
+  {
+    /* instructions */
+  }
+
+  return 1;
+}
diff --git a/regression/cbmc-cover/mcdc13/test.desc b/regression/cbmc-cover/mcdc13/test.desc
new file mode 100644
index 00000000000..c7983f47aa9
--- /dev/null
+++ b/regression/cbmc-cover/mcdc13/test.desc
@@ -0,0 +1,13 @@
+CORE
+main.c
+--cover mcdc
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.1\] file main.c line 9 function main MC/DC independence condition `A != FALSE && B != FALSE && C != FALSE.* SATISFIED$
+^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition `A != FALSE && B != FALSE && !(C != FALSE).* SATISFIED$
+^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition `A != FALSE && !(B != FALSE) && C != FALSE.* SATISFIED$
+^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition `!(A != FALSE) && B != FALSE && C != FALSE.* SATISFIED$
+^\*\* .* of .* covered (100.0%)$
+^\*\* Used 6 iterations$
+--
+^warning: ignoring
diff --git a/regression/cbmc-cover/mcdc14/main.c b/regression/cbmc-cover/mcdc14/main.c
new file mode 100644
index 00000000000..ebc094c78d5
--- /dev/null
+++ b/regression/cbmc-cover/mcdc14/main.c
@@ -0,0 +1,13 @@
+int main()
+{
+  int altitude;
+
+  __CPROVER_input("altitude", altitude);
+
+  if (altitude > 2500)
+  {
+    /* instructions */  
+  }
+
+  return 1;
+}
diff --git a/regression/cbmc-cover/mcdc14/test.desc b/regression/cbmc-cover/mcdc14/test.desc
new file mode 100644
index 00000000000..6778dfcc2f8
--- /dev/null
+++ b/regression/cbmc-cover/mcdc14/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+--cover mcdc
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.1\] file main.c line 7 function main decision/condition `altitude > 2500.* SATISFIED$
+^\[main.coverage.2\] file main.c line 7 function main decision/condition `altitude > 2500.* SATISFIED$
+^\*\* .* of .* covered (100.0%)$
+^\*\* Used 2 iterations$
+--
+^warning: ignoring
diff --git a/regression/cbmc-cover/mcdc8/main.c b/regression/cbmc-cover/mcdc8/main.c
new file mode 100644
index 00000000000..3eb9a0010e9
--- /dev/null
+++ b/regression/cbmc-cover/mcdc8/main.c
@@ -0,0 +1,19 @@
+int main()
+{
+  _Bool a, b, c;
+  
+  __CPROVER_input("a", a);
+  __CPROVER_input("b", b);
+  __CPROVER_input("c", c);
+
+  if ( (a || b) && c )
+  {
+  /* instructions */
+  }
+  else
+  {
+  /* instructions */
+  }
+
+  return 1;
+}
diff --git a/regression/cbmc-cover/mcdc8/test.desc b/regression/cbmc-cover/mcdc8/test.desc
new file mode 100644
index 00000000000..bf8dabbfa0f
--- /dev/null
+++ b/regression/cbmc-cover/mcdc8/test.desc
@@ -0,0 +1,13 @@
+CORE
+main.c
+--cover mcdc
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.1\] file main.c line 9 function main MC/DC independence condition `c != FALSE && a != FALSE && !(b != FALSE).* SATISFIED$
+^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition `c != FALSE && !(a != FALSE) && b != FALSE.* SATISFIED$
+^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition `c != FALSE && !(a != FALSE) && !(b != FALSE).* SATISFIED$
+^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition `!(c != FALSE) && a != FALSE && !(b != FALSE).* SATISFIED$
+^\*\* .* of .* covered (100.0%)$
+^\*\* Used 6 iterations$
+--
+^warning: ignoring
diff --git a/regression/cbmc-cover/mcdc9/main.c b/regression/cbmc-cover/mcdc9/main.c
new file mode 100644
index 00000000000..f239e63f287
--- /dev/null
+++ b/regression/cbmc-cover/mcdc9/main.c
@@ -0,0 +1,26 @@
+int main()
+{
+  _Bool u, x, y, z;
+  _Bool A, B, C, D;
+
+  A = (u==0);
+  B = (x>5);
+  C = (y<6);
+  D = (z==0);
+
+  __CPROVER_input("A", A);
+  __CPROVER_input("B", B);
+  __CPROVER_input("C", C);
+  __CPROVER_input("D", D);
+
+  if ( (A || B) && (C || D) )
+  {
+  /* instructions */
+  }
+  else
+  {
+  /* instructions */
+  }
+
+  return 1;
+}
diff --git a/regression/cbmc-cover/mcdc9/test.desc b/regression/cbmc-cover/mcdc9/test.desc
new file mode 100644
index 00000000000..d8ec7ea5f82
--- /dev/null
+++ b/regression/cbmc-cover/mcdc9/test.desc
@@ -0,0 +1,14 @@
+CORE
+main.c
+--cover mcdc
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.9\] file main.c line 16 function main MC/DC independence condition `A != FALSE && !(B != FALSE) && C != FALSE && !(D != FALSE).* SATISFIED$
+^\[main.coverage.10\] file main.c line 16 function main MC/DC independence condition `!(C != FALSE) && D != FALSE && A != FALSE && !(B != FALSE).* SATISFIED$
+^\[main.coverage.11\] file main.c line 16 function main MC/DC independence condition `!(C != FALSE) && !(D != FALSE) && A != FALSE && !(B != FALSE).* SATISFIED$
+^\[main.coverage.12\] file main.c line 16 function main MC/DC independence condition `!(A != FALSE) && B != FALSE && C != FALSE && !(D != FALSE).* SATISFIED$
+^\[main.coverage.13\] file main.c line 16 function main MC/DC independence condition `!(A != FALSE) && !(B != FALSE) && C != FALSE && !(D != FALSE).* SATISFIED$
+^\*\* .* of .* covered (100.0%)$
+^\*\* Used 8 iterations$
+--
+^warning: ignoring