diff --git a/regression/contracts/chain.sh b/regression/contracts/chain.sh
index a22dc195bdc..b79aae965bb 100755
--- a/regression/contracts/chain.sh
+++ b/regression/contracts/chain.sh
@@ -11,6 +11,14 @@ name=${*:$#}
 name=${name%.c}
 
 args=${*:5:$#-5}
+if [[ "$args" != *" _ "* ]]
+then
+  args_inst=$args
+  args_cbmc=""
+else
+  args_inst="${args%%" _ "*}"
+  args_cbmc="${args#*" _ "}"
+fi
 
 if [[ "${is_windows}" == "true" ]]; then
   $goto_cc "${name}.c"
@@ -20,10 +28,10 @@ else
 fi
 
 rm -f "${name}-mod.gb"
-$goto_instrument ${args} "${name}.gb" "${name}-mod.gb"
+$goto_instrument ${args_inst} "${name}.gb" "${name}-mod.gb"
 if [ ! -e "${name}-mod.gb" ] ; then
   cp "$name.gb" "${name}-mod.gb"
-elif echo $args | grep -q -- "--dump-c" ; then
+elif echo $args_inst | grep -q -- "--dump-c" ; then
   mv "${name}-mod.gb" "${name}-mod.c"
 
   if [[ "${is_windows}" == "true" ]]; then
@@ -36,4 +44,4 @@ elif echo $args | grep -q -- "--dump-c" ; then
   rm "${name}-mod.c"
 fi
 $goto_instrument --show-goto-functions "${name}-mod.gb"
-$cbmc "${name}-mod.gb"
+$cbmc "${name}-mod.gb" ${args_cbmc}
diff --git a/regression/contracts/function-calls-01/main.c b/regression/contracts/function-calls-01/main.c
new file mode 100644
index 00000000000..26f8445d361
--- /dev/null
+++ b/regression/contracts/function-calls-01/main.c
@@ -0,0 +1,14 @@
+int f1(int *x1) __CPROVER_requires(*x1 > 1 && *x1 < 10000)
+  __CPROVER_ensures(__CPROVER_return_value == *x1 + 1)
+{
+  return *x1 + 1;
+}
+
+int main()
+{
+  int p;
+  __CPROVER_assume(p > 1 && p < 10000);
+  f1(&p);
+
+  return 0;
+}
diff --git a/regression/contracts/function-calls-01/test-enf.desc b/regression/contracts/function-calls-01/test-enf.desc
new file mode 100644
index 00000000000..1b660f56d87
--- /dev/null
+++ b/regression/contracts/function-calls-01/test-enf.desc
@@ -0,0 +1,12 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  f1       | assumed  | asserted
diff --git a/regression/contracts/function-calls-01/test-rep.desc b/regression/contracts/function-calls-01/test-rep.desc
new file mode 100644
index 00000000000..d28bfcfb20b
--- /dev/null
+++ b/regression/contracts/function-calls-01/test-rep.desc
@@ -0,0 +1,12 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  f1       | asserted | assumed
diff --git a/regression/contracts/function-calls-02-1/main.c b/regression/contracts/function-calls-02-1/main.c
new file mode 100644
index 00000000000..43a06e3ef3b
--- /dev/null
+++ b/regression/contracts/function-calls-02-1/main.c
@@ -0,0 +1,21 @@
+int f1(int *x1) __CPROVER_requires(*x1 > 1 && *x1 < 10000)
+  __CPROVER_ensures(__CPROVER_return_value == *x1 + 3)
+{
+  int loc = *x1 + 1;
+  return f2(&loc) + 1;
+}
+
+int f2(int *x2) __CPROVER_requires(*x2 > 2 && *x2 < 10001)
+  __CPROVER_ensures(__CPROVER_return_value == *x2 + 1)
+{
+  return *x2 + 1;
+}
+
+int main()
+{
+  int p;
+  __CPROVER_assume(p > 1 && p < 10000);
+  f1(&p);
+
+  return 0;
+}
\ No newline at end of file
diff --git a/regression/contracts/function-calls-02-1/test-enf.desc b/regression/contracts/function-calls-02-1/test-enf.desc
new file mode 100644
index 00000000000..817b7b9c8d8
--- /dev/null
+++ b/regression/contracts/function-calls-02-1/test-enf.desc
@@ -0,0 +1,16 @@
+KNOWNBUG
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  f1       | assumed  | asserted
+  f2       | assumed  | asserted
+
+Known bug:
+Enforce flag not handled correctly for function calls within functions.
diff --git a/regression/contracts/function-calls-02-1/test-mix.desc b/regression/contracts/function-calls-02-1/test-mix.desc
new file mode 100644
index 00000000000..edd25ca30be
--- /dev/null
+++ b/regression/contracts/function-calls-02-1/test-mix.desc
@@ -0,0 +1,13 @@
+CORE
+main.c
+--enforce-contract f1 --replace-call-with-contract f2
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  f1       | assumed  | asserted
+  f2       | asserted | assumed
diff --git a/regression/contracts/function-calls-02-1/test-rep.desc b/regression/contracts/function-calls-02-1/test-rep.desc
new file mode 100644
index 00000000000..707cdf87fc8
--- /dev/null
+++ b/regression/contracts/function-calls-02-1/test-rep.desc
@@ -0,0 +1,15 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  f1       | asserted | assumed
+  f2       | n/a      | n/a
+
+Note: the call to f2 does not occur because the call to f1 is replaced by its contracts.
diff --git a/regression/contracts/function-calls-02/main.c b/regression/contracts/function-calls-02/main.c
new file mode 100644
index 00000000000..9c698ec912d
--- /dev/null
+++ b/regression/contracts/function-calls-02/main.c
@@ -0,0 +1,20 @@
+int f1(int *x1) __CPROVER_requires(*x1 > 1 && *x1 < 10000)
+  __CPROVER_ensures(__CPROVER_return_value == *x1 + 2)
+{
+  return f2(x1) + 1;
+}
+
+int f2(int *x2) __CPROVER_requires(*x2 > 1 && *x2 < 10000)
+  __CPROVER_ensures(__CPROVER_return_value == *x2 + 1)
+{
+  return *x2 + 1;
+}
+
+int main()
+{
+  int p;
+  __CPROVER_assume(p > 1 && p < 10000);
+  f1(&p);
+
+  return 0;
+}
diff --git a/regression/contracts/function-calls-02/test-enf.desc b/regression/contracts/function-calls-02/test-enf.desc
new file mode 100644
index 00000000000..817b7b9c8d8
--- /dev/null
+++ b/regression/contracts/function-calls-02/test-enf.desc
@@ -0,0 +1,16 @@
+KNOWNBUG
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  f1       | assumed  | asserted
+  f2       | assumed  | asserted
+
+Known bug:
+Enforce flag not handled correctly for function calls within functions.
diff --git a/regression/contracts/function-calls-02/test-mix.desc b/regression/contracts/function-calls-02/test-mix.desc
new file mode 100644
index 00000000000..edd25ca30be
--- /dev/null
+++ b/regression/contracts/function-calls-02/test-mix.desc
@@ -0,0 +1,13 @@
+CORE
+main.c
+--enforce-contract f1 --replace-call-with-contract f2
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  f1       | assumed  | asserted
+  f2       | asserted | assumed
diff --git a/regression/contracts/function-calls-02/test-rep.desc b/regression/contracts/function-calls-02/test-rep.desc
new file mode 100644
index 00000000000..707cdf87fc8
--- /dev/null
+++ b/regression/contracts/function-calls-02/test-rep.desc
@@ -0,0 +1,15 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  f1       | asserted | assumed
+  f2       | n/a      | n/a
+
+Note: the call to f2 does not occur because the call to f1 is replaced by its contracts.
diff --git a/regression/contracts/function-calls-03-1/main.c b/regression/contracts/function-calls-03-1/main.c
new file mode 100644
index 00000000000..ed53e1e5d31
--- /dev/null
+++ b/regression/contracts/function-calls-03-1/main.c
@@ -0,0 +1,23 @@
+int f1(int *x1) __CPROVER_requires(*x1 > 0 && *x1 < 20)
+  __CPROVER_ensures(__CPROVER_return_value == *x1 + 2)
+{
+  return f2(x1) + 1;
+}
+
+int f2(int *x2) __CPROVER_requires(*x2 >= 0 && *x2 < 20)
+  __CPROVER_ensures(__CPROVER_return_value == *x2 + 1)
+{
+  if(*x2 < 1)
+    return -1; //Notice the change for the base case
+  int loc = *x2 - 1;
+  return f2(&loc) + 1;
+}
+
+int main()
+{
+  int p;
+  __CPROVER_assume(p > 0 && p < 20);
+  f1(&p);
+
+  return 0;
+}
diff --git a/regression/contracts/function-calls-03-1/test-enf.desc b/regression/contracts/function-calls-03-1/test-enf.desc
new file mode 100644
index 00000000000..859a593e234
--- /dev/null
+++ b/regression/contracts/function-calls-03-1/test-enf.desc
@@ -0,0 +1,19 @@
+CORE
+main.c
+--enforce-all-contracts _ --unwind 20 --unwinding-assertions
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  f1       | assumed  | asserted
+  f2       | assumed  | asserted
+
+Test should fail:
+The postcondition of f2 is incorrect, considering the recursion particularity. 
+
+Recursion:
+The base case for the recursive call to f2 provides different behavior than the common case (given the pre-conditions).
diff --git a/regression/contracts/function-calls-03/main.c b/regression/contracts/function-calls-03/main.c
new file mode 100644
index 00000000000..203ffd82a70
--- /dev/null
+++ b/regression/contracts/function-calls-03/main.c
@@ -0,0 +1,23 @@
+int f1(int *x1) __CPROVER_requires(*x1 > 0 && *x1 < 20)
+  __CPROVER_ensures(__CPROVER_return_value == *x1 + 2)
+{
+  return f2(x1) + 1;
+}
+
+int f2(int *x2) __CPROVER_requires(*x2 >= 0 && *x2 < 20)
+  __CPROVER_ensures(__CPROVER_return_value == *x2 + 1)
+{
+  if(*x2 < 1)
+    return 1;
+  int loc = *x2 - 1;
+  return f2(&loc) + 1;
+}
+
+int main()
+{
+  int p;
+  __CPROVER_assume(p > 0 && p < 20);
+  f1(&p);
+
+  return 0;
+}
diff --git a/regression/contracts/function-calls-03/test-enf.desc b/regression/contracts/function-calls-03/test-enf.desc
new file mode 100644
index 00000000000..fdbd93aacd0
--- /dev/null
+++ b/regression/contracts/function-calls-03/test-enf.desc
@@ -0,0 +1,19 @@
+KNOWNBUG
+main.c
+--enforce-all-contracts _ --unwind 20 --unwinding-assertions
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  f1       | assumed  | asserted
+  f2       | assumed  | asserted
+
+Recursion:
+The base case for the recursive call to f2 provides the same behavior as the common case (given the pre-conditions).
+
+Known bug:
+Enforce flag not handled correctly for function calls within functions.
diff --git a/regression/contracts/function-calls-03/test-mix.desc b/regression/contracts/function-calls-03/test-mix.desc
new file mode 100644
index 00000000000..ffc11785616
--- /dev/null
+++ b/regression/contracts/function-calls-03/test-mix.desc
@@ -0,0 +1,16 @@
+CORE
+main.c
+--enforce-contract f1 --replace-call-with-contract f2
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  f1       | assumed  | asserted
+  f2       | asserted | assumed
+
+Recursion:
+The base case for the recursive call to f2 provides the same behavior as the common case (given the pre-conditions).
diff --git a/regression/contracts/function-calls-03/test-rep.desc b/regression/contracts/function-calls-03/test-rep.desc
new file mode 100644
index 00000000000..cca10ac941f
--- /dev/null
+++ b/regression/contracts/function-calls-03/test-rep.desc
@@ -0,0 +1,18 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  f1       | asserted | assumed
+  f2       | n/a      | n/a
+
+Note: the call to f2 does not occur because the call to f1 is replaced by its contracts.
+
+Recursion:
+The base case for the recursive call to f2 provides the same behavior as the common case (given the pre-conditions).
diff --git a/regression/contracts/function-calls-04-1/main.c b/regression/contracts/function-calls-04-1/main.c
new file mode 100644
index 00000000000..36136e08bd2
--- /dev/null
+++ b/regression/contracts/function-calls-04-1/main.c
@@ -0,0 +1,29 @@
+int f1(int *x1) __CPROVER_requires(*x1 > 0 && *x1 < 20)
+  __CPROVER_ensures(__CPROVER_return_value == *x1 + 2)
+{
+  return f2_out(x1) + 1;
+}
+
+int f2_out(int *x2) __CPROVER_requires(*x2 >= 0 && *x2 < 20)
+  __CPROVER_ensures(__CPROVER_return_value == *x2 + 1)
+{
+  if(*x2 < 1)
+    return -1; //Notice the change for the base case
+  int loc2 = *x2 - 1;
+  return f2_in(&loc2) + 1;
+}
+
+int f2_in(int *x2) __CPROVER_requires(*x2 >= 0 && *x2 < 19)
+  __CPROVER_ensures(__CPROVER_return_value == *x2 + 1)
+{
+  return f2_out(x2);
+}
+
+int main()
+{
+  int p;
+  __CPROVER_assume(p > 0 && p < 20);
+  f1(&p);
+
+  return 0;
+}
diff --git a/regression/contracts/function-calls-04-1/test-enf.desc b/regression/contracts/function-calls-04-1/test-enf.desc
new file mode 100644
index 00000000000..4ca0e5e7948
--- /dev/null
+++ b/regression/contracts/function-calls-04-1/test-enf.desc
@@ -0,0 +1,20 @@
+CORE
+main.c
+--enforce-all-contracts _ --unwind 20 --unwinding-assertions
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  f1       | assumed  | asserted
+  f2_out   | assumed  | asserted
+  f2_in    | assumed  | asserted
+
+Test should fail:
+The postcondition of f2 is incorrect, considering the recursion particularity. 
+
+Recursion:
+The base case for the recursive call to f2 provides different behavior than the general case (given the pre-conditions).
diff --git a/regression/contracts/function-calls-04/main.c b/regression/contracts/function-calls-04/main.c
new file mode 100644
index 00000000000..f3aced38c72
--- /dev/null
+++ b/regression/contracts/function-calls-04/main.c
@@ -0,0 +1,29 @@
+int f1(int *x1) __CPROVER_requires(*x1 > 0 && *x1 < 20)
+  __CPROVER_ensures(__CPROVER_return_value == *x1 + 2)
+{
+  return f2_out(x1) + 1;
+}
+
+int f2_out(int *x2) __CPROVER_requires(*x2 >= 0 && *x2 < 20)
+  __CPROVER_ensures(__CPROVER_return_value == *x2 + 1)
+{
+  if(*x2 < 1)
+    return 1;
+  int loc2 = *x2 - 1;
+  return f2_in(&loc2) + 1;
+}
+
+int f2_in(int *x2) __CPROVER_requires(*x2 >= 0 && *x2 < 19)
+  __CPROVER_ensures(__CPROVER_return_value == *x2 + 1)
+{
+  return f2_out(x2);
+}
+
+int main()
+{
+  int p;
+  __CPROVER_assume(p > 0 && p < 20);
+  f1(&p);
+
+  return 0;
+}
diff --git a/regression/contracts/function-calls-04/test-enf.desc b/regression/contracts/function-calls-04/test-enf.desc
new file mode 100644
index 00000000000..808cdab1356
--- /dev/null
+++ b/regression/contracts/function-calls-04/test-enf.desc
@@ -0,0 +1,20 @@
+KNOWNBUG
+main.c
+--enforce-all-contracts _ --unwind 20 --unwinding-assertions
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  f1       | assumed  | asserted
+  f2_out   | assumed  | asserted
+  f2_in    | assumed  | asserted
+
+Recursion:
+The base case for the recursive call to f2 provides the same behavior as the common case (given the pre-conditions).
+
+Known bug:
+Enforce flag not handled correctly for function calls within functions.
diff --git a/regression/contracts/function-calls-04/test-mix-1.desc b/regression/contracts/function-calls-04/test-mix-1.desc
new file mode 100644
index 00000000000..3073097c3ee
--- /dev/null
+++ b/regression/contracts/function-calls-04/test-mix-1.desc
@@ -0,0 +1,19 @@
+CORE
+main.c
+--enforce-contract f1 --replace-call-with-contract f2_out
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  f1       | assumed  | asserted
+  f2_out   | asserted | assumed
+  f2_in    | n/a      | n/a
+
+Note: the calls to f2_in does not occur because the call to f2_out is replaced by its contracts.
+
+Recursion:
+The base case for the recursive call to f2 provides the same behavior as the common case (given the pre-conditions).
diff --git a/regression/contracts/function-calls-04/test-mix-2.desc b/regression/contracts/function-calls-04/test-mix-2.desc
new file mode 100644
index 00000000000..243d70b6f19
--- /dev/null
+++ b/regression/contracts/function-calls-04/test-mix-2.desc
@@ -0,0 +1,22 @@
+KNOWNBUG
+main.c
+--enforce-contract f1 --enforce-contract f2_out --replace-call-with-contract f2_in
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  f1       | assumed  | asserted
+  f2_out   | assumed  | asserted
+  f2_in    | asserted | assumed
+
+Recursion
+(1) This test checks the mutualy recursive f2_out and f2-in functions by enforcing f2_out and replacing the internal f2_in call with its contract.
+(2) This test does not require unwinding.
+(3) The base case for the recursive call to f2 provides the same behavior as the common case (given the pre-conditions).
+
+Known bug:
+Enforce flag not handled correctly for function calls within functions.
diff --git a/regression/contracts/function-calls-04/test-rep.desc b/regression/contracts/function-calls-04/test-rep.desc
new file mode 100644
index 00000000000..0551bd1a6b7
--- /dev/null
+++ b/regression/contracts/function-calls-04/test-rep.desc
@@ -0,0 +1,19 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  f1       | asserted | assumed
+  f2_out   | n/a      | n/a
+  f2_in    | n/a      | n/a
+
+Note: the calls to f2_out and to f2_in do not occur because the call to f1 is replaced by its contracts.
+
+Recursion:
+The base case for the recursive call to f2 provides the same behavior as the common case (given the pre-conditions).