diff --git a/regression/Makefile b/regression/Makefile
index c41b1080e89..9d38a19e234 100644
--- a/regression/Makefile
+++ b/regression/Makefile
@@ -18,7 +18,8 @@ DIRS = cbmc \
        goto-cc-cbmc \
        cbmc-cpp \
        goto-cc-goto-analyzer \
-       systemc
+       systemc \
+       contracts \
        # Empty last line
 
 # Tests under goto-gcc cannot be run on Windows, so appveyor.yml unlinks
diff --git a/regression/contracts/CMakeLists.txt b/regression/contracts/CMakeLists.txt
new file mode 100644
index 00000000000..f7f08694f6a
--- /dev/null
+++ b/regression/contracts/CMakeLists.txt
@@ -0,0 +1,9 @@
+if(WIN32)
+    set(is_windows true)
+else()
+    set(is_windows false)
+endif()
+
+add_test_pl_tests(
+    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> $<TARGET_FILE:cbmc> ${is_windows}"
+)
diff --git a/regression/contracts/Makefile b/regression/contracts/Makefile
new file mode 100644
index 00000000000..8d53e0b2656
--- /dev/null
+++ b/regression/contracts/Makefile
@@ -0,0 +1,35 @@
+default: tests.log
+
+include ../../src/config.inc
+include ../../src/common
+
+ifeq ($(BUILD_ENV_),MSVC)
+	exe=../../../src/goto-cc/goto-cl
+	is_windows=true
+else
+	exe=../../../src/goto-cc/goto-cc
+	is_windows=false
+endif
+
+test:
+	@../test.pl -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)'
+
+tests.log:
+	@../test.pl -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)'
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	@for dir in *; do \
+		$(RM) tests.log; \
+		if [ -d "$$dir" ]; then \
+			cd "$$dir"; \
+			$(RM) *.out *.gb; \
+			cd ..; \
+		fi \
+	done
diff --git a/regression/contracts/chain.sh b/regression/contracts/chain.sh
new file mode 100755
index 00000000000..2656ea4488f
--- /dev/null
+++ b/regression/contracts/chain.sh
@@ -0,0 +1,38 @@
+#!/bin/bash
+
+set -e
+
+goto_cc=$1
+goto_instrument=$2
+cbmc=$3
+is_windows=$4
+
+name=${*:$#}
+name=${name%.c}
+
+args=${*:5:$#-5}
+
+if [[ "${is_windows}" == "true" ]]; then
+  $goto_cc "${name}.c"
+  mv "${name}.exe" "${name}.gb"
+else
+  $goto_cc -o "${name}.gb" "${name}.c"
+fi
+
+$goto_instrument ${args} "${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
+  mv "${name}-mod.gb" "${name}-mod.c"
+
+  if [[ "${is_windows}" == "true" ]]; then
+    $goto_cc "${name}-mod.c"
+    mv "${name}-mod.exe" "${name}-mod.gb"
+  else
+    $goto_cc -o "${name}-mod.gb" "${name}-mod.c"
+  fi
+
+  rm "${name}-mod.c"
+fi
+$goto_instrument --show-goto-functions "${name}-mod.gb"
+$cbmc "${name}-mod.gb"
diff --git a/regression/contracts/function_apply_01/main.c b/regression/contracts/function_apply_01/main.c
new file mode 100644
index 00000000000..3112343940f
--- /dev/null
+++ b/regression/contracts/function_apply_01/main.c
@@ -0,0 +1,20 @@
+// function_apply_01
+
+// Note that this test is supposed to have an incorrect contract.
+// We verify that applying (without checking) the contract yields success,
+// and that checking the contract yields failure.
+
+#include <assert.h>
+
+int foo() 
+  __CPROVER_ensures(__CPROVER_return_value == 0)
+{
+  return 1;
+}
+
+int main()
+{
+  int x = foo();
+  assert(x == 0);
+  return 0;
+}
diff --git a/regression/contracts/function_apply_01/test.desc b/regression/contracts/function_apply_01/test.desc
new file mode 100644
index 00000000000..abc8686ad8e
--- /dev/null
+++ b/regression/contracts/function_apply_01/test.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+main.c
+--apply-code-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Applying code contracts currently also checks them.
diff --git a/regression/contracts/function_check_01/main.c b/regression/contracts/function_check_01/main.c
new file mode 100644
index 00000000000..27bc259c58b
--- /dev/null
+++ b/regression/contracts/function_check_01/main.c
@@ -0,0 +1,31 @@
+// function_check_01
+
+// This tests a simple example of a function with requires and
+// ensures which should both be satisfied.
+
+#include <assert.h>
+
+int min(int a, int b)
+  __CPROVER_requires(a >= 0 && b >= 0)
+  __CPROVER_ensures(__CPROVER_return_value <= a &&
+                    __CPROVER_return_value <= b &&
+                   (__CPROVER_return_value == a || __CPROVER_return_value == b)
+                   )
+{
+  if(a <= b)
+  {
+    return a;
+  }
+  else
+  {
+    return b;
+  }
+}
+
+int main()
+{
+  int x, y, z;
+  __CPROVER_assume(x >= 0 && y >= 0);
+  z = min(x, y);
+  assert(z <= x);
+}
diff --git a/regression/contracts/function_check_01/test.desc b/regression/contracts/function_check_01/test.desc
new file mode 100644
index 00000000000..d9a2ec0a8ca
--- /dev/null
+++ b/regression/contracts/function_check_01/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+--apply-code-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+--check-code-contracts not implemented yet.
+--apply-code-contracts is the current name for the flag. This should be
+updated as the flag changes.
diff --git a/regression/contracts/function_check_02/main.c b/regression/contracts/function_check_02/main.c
new file mode 100644
index 00000000000..020113bd1d5
--- /dev/null
+++ b/regression/contracts/function_check_02/main.c
@@ -0,0 +1,24 @@
+// function_check_02
+
+// This test checks the use of quantifiers in ensures clauses.
+// A known bug (resolved in PR #2278) causes the use of quantifiers
+// in ensures to fail.
+
+int initialize(int *arr)
+  __CPROVER_ensures(
+    __CPROVER_forall {int i; (0 <= i && i < 10) ==> arr[i] == i}
+  )
+{
+  for(int i = 0; i < 10; i++)
+  {
+    arr[i] = i;
+  }
+
+  return 0;
+}
+
+int main()
+{
+  int arr[10];
+  initialize(arr);
+}
diff --git a/regression/contracts/function_check_02/test.desc b/regression/contracts/function_check_02/test.desc
new file mode 100644
index 00000000000..9c4d3556c69
--- /dev/null
+++ b/regression/contracts/function_check_02/test.desc
@@ -0,0 +1,10 @@
+KNOWNBUG
+main.c
+--check-code-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Ensures statements currently do not allow quantified predicates unless the
+function has void return type.
diff --git a/regression/contracts/function_check_03/main.c b/regression/contracts/function_check_03/main.c
new file mode 100644
index 00000000000..2e2e9af0d9f
--- /dev/null
+++ b/regression/contracts/function_check_03/main.c
@@ -0,0 +1,26 @@
+// function_check_03
+
+// This extends function_check_02's test of quantifiers in ensures
+// and adds in a loop invariant which can be used to prove the ensures.
+// This currently fails because side-effect checking in loop invariants is
+// incorrect.
+
+void initialize(int *arr, int len)
+  __CPROVER_ensures(
+    __CPROVER_forall {int i; (0 <= i && i < len) ==> arr[i] == i}
+  )
+{
+  for(int i = 0; i < len; i++)
+    __CPROVER_loop_invariant(
+      __CPROVER_forall {int j; (0 <= j && j < i) ==> arr[j] == j}
+    )
+  {
+    arr[i] = i;
+  }
+}
+
+int main()
+{
+  int arr[10];
+  initialize(arr, 10);
+}
diff --git a/regression/contracts/function_check_03/test.desc b/regression/contracts/function_check_03/test.desc
new file mode 100644
index 00000000000..14848623f06
--- /dev/null
+++ b/regression/contracts/function_check_03/test.desc
@@ -0,0 +1,10 @@
+KNOWNBUG
+main.c
+--check-code-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Loop invariants currently do not support memory reads in at least some
+circumstances.
diff --git a/regression/contracts/function_check_04/main.c b/regression/contracts/function_check_04/main.c
new file mode 100644
index 00000000000..acf0122c5e4
--- /dev/null
+++ b/regression/contracts/function_check_04/main.c
@@ -0,0 +1,19 @@
+// function_check_04
+
+// Note that this test is supposed to have an incorrect contract.
+// We verify that checking this faulty contract (correctly) yields a failure.
+
+#include <assert.h>
+
+int foo() 
+  __CPROVER_ensures(__CPROVER_return_value == 0)
+{
+  return 1;
+}
+
+int main()
+{
+  int x = foo();
+  assert(x == 0);
+  return 0;
+}
diff --git a/regression/contracts/function_check_04/test.desc b/regression/contracts/function_check_04/test.desc
new file mode 100644
index 00000000000..db7ee5aa32a
--- /dev/null
+++ b/regression/contracts/function_check_04/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+--apply-code-contracts
+^\[main.assertion.1\] assertion x == 0: SUCCESS$
+^\[foo.1\] : FAILURE$
+^VERIFICATION FAILED$
+--
+--
+--check-code-contracts not implemented yet.
+--apply-code-contracts is the current name for the flag. This should be
+updated as the flag changes.
diff --git a/regression/contracts/function_check_05/main.c b/regression/contracts/function_check_05/main.c
new file mode 100644
index 00000000000..14f85546506
--- /dev/null
+++ b/regression/contracts/function_check_05/main.c
@@ -0,0 +1,26 @@
+// function_check_05
+
+// This test checks that when a function call is replaced by an invariant,
+// it adequately havocs the locations modified by the function.
+// This test currently fails because the analysis of what is modified by
+// a function is flawed.
+
+#include <assert.h>
+
+int foo(int *x) 
+  __CPROVER_ensures(__CPROVER_return_value == 1)
+{
+  *x = 1;
+  return 1;
+}
+
+int main()
+{
+  int y = 0;  
+  int z = foo(&y);
+  // This assert should fail.
+  assert(y == 0);
+  // This one should succeed.
+  assert(z == 1);
+  return 0;
+}
diff --git a/regression/contracts/function_check_05/test.desc b/regression/contracts/function_check_05/test.desc
new file mode 100644
index 00000000000..77e210f10d8
--- /dev/null
+++ b/regression/contracts/function_check_05/test.desc
@@ -0,0 +1,10 @@
+KNOWNBUG
+main.c
+--check-code-contracts
+^\[main.assertion.1\] assertion y == 0: FAILURE$
+^\[main.assertion.2\] assertion z == 1: SUCCESS$
+^\[foo.1\] : SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Contract checking does not properly havoc function calls.
diff --git a/regression/contracts/function_check_mem_01/main.c b/regression/contracts/function_check_mem_01/main.c
new file mode 100644
index 00000000000..b63364f4d57
--- /dev/null
+++ b/regression/contracts/function_check_mem_01/main.c
@@ -0,0 +1,45 @@
+// function_check_mem_01
+
+// This test checks the use of pointer-related predicates in assumptions and
+// requires.
+// This test currently fails because of the lack of support for assuming
+// pointer predicates.
+
+#include <stddef.h>
+
+#define __CPROVER_VALID_MEM(ptr, size) \
+  __CPROVER_POINTER_OBJECT((ptr)) != __CPROVER_POINTER_OBJECT(NULL) && \
+  !__CPROVER_invalid_pointer((ptr)) && \
+  __CPROVER_POINTER_OBJECT((ptr)) != \
+  __CPROVER_POINTER_OBJECT(__CPROVER_deallocated) && \
+  __CPROVER_POINTER_OBJECT((ptr)) != \
+  __CPROVER_POINTER_OBJECT(__CPROVER_dead_object) && \
+  (__builtin_object_size((ptr), 1) >= (size) && \
+  __CPROVER_POINTER_OFFSET((ptr)) >= 0l || \
+   __CPROVER_DYNAMIC_OBJECT((ptr))) && \
+  (__CPROVER_POINTER_OFFSET((ptr)) >= 0 && \
+   __CPROVER_malloc_size >= (size) + __CPROVER_POINTER_OFFSET((ptr)) || \
+   __CPROVER_POINTER_OBJECT((ptr)) != \
+   __CPROVER_POINTER_OBJECT(__CPROVER_malloc_object))
+    
+typedef struct bar
+{
+  int x;
+  int y;
+  int z;
+} bar;
+
+void foo(bar *x)
+  __CPROVER_requires(__CPROVER_VALID_MEM(x, sizeof(bar)))
+{
+  x->x += 1;
+  return
+}
+
+int main()
+{
+  bar *y;
+  __CPROVER_assume(__CPROVER_VALID_MEM(y, sizeof(bar)));
+  y->x = 0;
+  return 0;
+}
diff --git a/regression/contracts/function_check_mem_01/test.desc b/regression/contracts/function_check_mem_01/test.desc
new file mode 100644
index 00000000000..b46799f781b
--- /dev/null
+++ b/regression/contracts/function_check_mem_01/test.desc
@@ -0,0 +1,10 @@
+KNOWNBUG
+main.c
+--check-code-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+CBMC currently does not support assumptions about pointers in the general way
+that other assumptions are supported.
diff --git a/regression/contracts/invar_check_01/main.c b/regression/contracts/invar_check_01/main.c
new file mode 100644
index 00000000000..d23252ebd6b
--- /dev/null
+++ b/regression/contracts/invar_check_01/main.c
@@ -0,0 +1,20 @@
+// invar_check_01
+
+// This test checks that a basic loop invariant can be proven and used in
+// combination with the negation of the loop guard to get a result.
+
+#include <assert.h>
+
+int main()
+{
+  int r;
+  __CPROVER_assume(r >= 0);
+  while(r > 0)
+    __CPROVER_loop_invariant(r >= 0)
+  {
+    --r;
+  }
+  assert(r == 0);
+
+  return 0;
+}
diff --git a/regression/contracts/invar_check_01/test.desc b/regression/contracts/invar_check_01/test.desc
new file mode 100644
index 00000000000..d9a2ec0a8ca
--- /dev/null
+++ b/regression/contracts/invar_check_01/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+--apply-code-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+--check-code-contracts not implemented yet.
+--apply-code-contracts is the current name for the flag. This should be
+updated as the flag changes.
diff --git a/regression/contracts/invar_check_02/main.c b/regression/contracts/invar_check_02/main.c
new file mode 100644
index 00000000000..fee261011ea
--- /dev/null
+++ b/regression/contracts/invar_check_02/main.c
@@ -0,0 +1,29 @@
+// invar_check_02
+
+// This test checks that loop invariants adequately handle continues.
+
+#include <assert.h>
+
+int main()
+{
+  int r;
+  __CPROVER_assume(r >= 0);
+
+  while(r > 0)
+    __CPROVER_loop_invariant(r >= 0)
+  { 
+    --r;
+    if (r < 5)
+    {
+      continue;
+    }
+    else
+    {
+      --r;
+    }
+  }
+
+  assert(r == 0);
+
+  return 0;
+}
diff --git a/regression/contracts/invar_check_02/test.desc b/regression/contracts/invar_check_02/test.desc
new file mode 100644
index 00000000000..d9a2ec0a8ca
--- /dev/null
+++ b/regression/contracts/invar_check_02/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+--apply-code-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+--check-code-contracts not implemented yet.
+--apply-code-contracts is the current name for the flag. This should be
+updated as the flag changes.
diff --git a/regression/contracts/invar_check_03/main.c b/regression/contracts/invar_check_03/main.c
new file mode 100644
index 00000000000..253e5a951d6
--- /dev/null
+++ b/regression/contracts/invar_check_03/main.c
@@ -0,0 +1,85 @@
+// invar_check_03
+
+// This test checks the use of loop invariants on a larger problem --- in this
+// case, the partition portion of quicksort, applied to a fixed-length array.
+// This serves as a stop-gap test until issues to do with quantifiers and
+// side-effects in loop invariants are fixed.
+
+#include <assert.h>
+
+void swap(int *a, int *b)
+{
+  *a ^= *b;
+  *b ^= *a;
+  *a ^= *b;
+}
+
+int main()
+{ 
+  int arr0, arr1, arr2, arr3, arr4;
+  arr0 = 1;
+  arr1 = 2;
+  arr2 = 0;
+  arr3 = 4;
+  arr4 = 3; 
+  int *arr[5] = {&arr0, &arr1, &arr2, &arr3, &arr4};
+  int pivot = 2;
+
+  int h = 5 - 1;
+  int l = 0;
+  int r = 1;
+  while(h > l)
+    __CPROVER_loop_invariant(
+      h >= l &&
+      0 <= l && l < 5 &&
+      0 <= h && h < 5 &&
+      l <= r && r <= h &&
+      (r == 0 ==> arr0 == pivot) &&
+      (r == 1 ==> arr1 == pivot) &&
+      (r == 2 ==> arr2 == pivot) &&
+      (r == 3 ==> arr3 == pivot) &&
+      (r == 4 ==> arr4 == pivot) &&
+      (0 < l ==> arr0 <= pivot) &&
+      (1 < l ==> arr1 <= pivot) &&
+      (2 < l ==> arr2 <= pivot) &&
+      (3 < l ==> arr3 <= pivot) &&
+      (4 < l ==> arr4 <= pivot) &&
+      (0 > h ==> arr0 >= pivot) &&
+      (1 > h ==> arr1 >= pivot) &&
+      (2 > h ==> arr2 >= pivot) &&
+      (3 > h ==> arr3 >= pivot) &&
+      (4 > h ==> arr4 >= pivot)
+    )
+  {
+    if(*(arr[h]) <= pivot && *(arr[l]) >= pivot) {
+      swap(arr[h], arr[l]);
+      if (r == h) {
+        r = l;
+        h--;
+      }
+      else if(r == l) {
+        r = h;
+        l++;
+      }
+    }
+    else if(*(arr[h]) <= pivot) {
+      l++;
+    }
+    else {
+      h--;
+    }
+  }
+  assert(0 <= r && r < 5);
+  assert(*(arr[r]) == pivot);
+  assert(0 < r ==> arr0 <= pivot);
+  assert(1 < r ==> arr1 <= pivot);
+  assert(2 < r ==> arr2 <= pivot);
+  assert(3 < r ==> arr3 <= pivot);
+  assert(4 < r ==> arr4 <= pivot);
+  assert(0 > r ==> arr0 >= pivot);
+  assert(1 > r ==> arr1 >= pivot);
+  assert(2 > r ==> arr2 >= pivot);
+  assert(3 > r ==> arr3 >= pivot);
+  assert(4 > r ==> arr4 >= pivot);
+  return r;
+}
diff --git a/regression/contracts/invar_check_03/test.desc b/regression/contracts/invar_check_03/test.desc
new file mode 100644
index 00000000000..d9a2ec0a8ca
--- /dev/null
+++ b/regression/contracts/invar_check_03/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+--apply-code-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+--check-code-contracts not implemented yet.
+--apply-code-contracts is the current name for the flag. This should be
+updated as the flag changes.
diff --git a/regression/contracts/invar_check_04/main.c b/regression/contracts/invar_check_04/main.c
new file mode 100644
index 00000000000..68c2fa4ceea
--- /dev/null
+++ b/regression/contracts/invar_check_04/main.c
@@ -0,0 +1,30 @@
+// invar_check_04
+
+// This test checks the handling of break by loop invariants.
+// This test is expected to fail along the code path where r is even before
+// entering the loop.
+
+#include <assert.h>
+
+int main()
+{
+  int r;
+  __CPROVER_assume(r >= 0);
+
+  while(r>0)
+    __CPROVER_loop_invariant(r >= 0)
+  { 
+    --r;
+    if (r <= 1)
+    {
+      break;
+    }
+    else
+    {
+      --r;
+    }
+  }
+  assert(r == 0);
+
+  return 0;
+}
diff --git a/regression/contracts/invar_check_04/test.desc b/regression/contracts/invar_check_04/test.desc
new file mode 100644
index 00000000000..7414b7f58a6
--- /dev/null
+++ b/regression/contracts/invar_check_04/test.desc
@@ -0,0 +1,12 @@
+CORE
+main.c
+--apply-code-contracts
+^\[main.1\] Loop invariant violated before entry: SUCCESS$
+^\[main.2\] Loop invariant not preserved: SUCCESS$
+^\[main.assertion.1\] assertion r == 0: FAILURE$
+^VERIFICATION FAILED$
+--
+--
+--check-code-contracts not implemented yet.
+--apply-code-contracts is the current name for the flag. This should be
+updated as the flag changes.
diff --git a/regression/contracts/invar_loop_constant/main.c b/regression/contracts/invar_loop_constant/main.c
new file mode 100644
index 00000000000..34eb0575d53
--- /dev/null
+++ b/regression/contracts/invar_loop_constant/main.c
@@ -0,0 +1,25 @@
+// invar_loop_constant
+
+// This test checks to see whether loop invariant checking discards sufficiently
+// little information to be aware after the loop that s is necessarily 1.
+// This test currently fails due to excessive havocking in checking loop
+// invariants, but is not an obstacle to soundness of contract checking.
+
+#include <assert.h>
+
+int main()
+{
+  int r;
+  int s = 1;
+  __CPROVER_assume(r >= 0);
+  while(r > 0)
+    __CPROVER_loop_invariant(r >= 0)
+  {
+    s = 1;
+    r--;
+  }
+  assert(r == 0);
+  assert(s == 1);
+
+  return 0;
+}
diff --git a/regression/contracts/invar_loop_constant/test.desc b/regression/contracts/invar_loop_constant/test.desc
new file mode 100644
index 00000000000..a27604a79fd
--- /dev/null
+++ b/regression/contracts/invar_loop_constant/test.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+main.c
+--check-code-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Loop invariant checking throws away more information than needed.
diff --git a/regression/contracts/quicksort_contracts_01/main.c b/regression/contracts/quicksort_contracts_01/main.c
new file mode 100644
index 00000000000..3b846a927d3
--- /dev/null
+++ b/regression/contracts/quicksort_contracts_01/main.c
@@ -0,0 +1,112 @@
+// quicksort_contracts_01
+
+// This test checks the correctness of a quicksort implementation using explicit
+// ghost state.
+
+// This test currently fails for a variety of reasons, including:
+// (1) Lack of support for quantifiers in ensures statements.
+// (2) Lack of support for reading from memory in loop invariants (under some
+// circumstances)
+
+#include <assert.h>
+#include <stdlib.h>
+#include <string.h>
+
+void swap(int *a, int *b)
+{
+  *a ^= *b;
+  *b ^= *a;
+  *a ^= *b;
+}
+
+int partition(int arr_ghost[], int arr[], int len)
+  __CPROVER_requires(
+    __CPROVER_forall {int i; (0 <= i && i < len) ==> arr_ghost[i] == arr[i]} &&
+   len > 0 &&
+    1 == 1
+  )
+  __CPROVER_ensures(
+    __CPROVER_forall {int i; (0 <= i && i < len) ==> __CPROVER_exists {int j; 0 <= j && j < len && arr_ghost[i] == arr[j]}} &&
+    __CPROVER_forall {int i; (0 <= i && i < len) ==> __CPROVER_exists {int j; 0 <= j && j < len && arr[i] == arr_ghost[j]}} &&
+    0 <= __CPROVER_return_value && __CPROVER_return_value < len &&
+    __CPROVER_forall {int i; (0 <= i && i <= __CPROVER_return_value) ==> arr[i] <= arr[__CPROVER_return_value]} &&
+    __CPROVER_forall {int i; (__CPROVER_return_value <= i && i < len) ==> arr[__CPROVER_return_value] <= arr[i]} &&
+    1 == 1
+  )
+{
+  int h = len - 1;
+  int l = 0;
+
+  int pivot_idx = len / 2;
+  int pivot = arr[pivot_idx];
+
+  while(h > l)
+    __CPROVER_loop_invariant(
+        0 <= l && l <= pivot_idx && pivot_idx <= h && h < len &&
+      arr[pivot_idx] == pivot &&
+      __CPROVER_forall {int i; (0 <= i && i < l) ==> arr[i] <= pivot} &&
+      __CPROVER_forall {int i; (h < i && i < len) ==> pivot <= arr[i]} &&
+      1 == 1
+    )
+  {
+    if(arr[h] <= pivot && arr[l] >= pivot)
+    {
+      swap(arr + h, arr + l);
+      if(pivot_idx == h)
+      {
+        pivot_idx = l;
+        h--;
+      }
+      if(pivot_idx == l)
+      {
+        pivot_idx = h;
+        l++;
+      }
+    }
+    else if(arr[h] <= pivot)
+    {
+      l++;
+    }
+    else
+    {
+      h--;
+    }
+  }
+  return pivot_idx;
+}
+
+void quicksort(int arr_ghost[], int arr[], int len)
+  __CPROVER_requires(
+    __CPROVER_forall {int i; (0 <= i && i < len) ==> arr_ghost[i] == arr[i]} &&
+    1 == 1
+  )
+  __CPROVER_ensures(
+    __CPROVER_forall {int i; (0 <= i && i < len) ==> __CPROVER_exists {int j; 0 <= j && j < len && arr_ghost[i] == arr[j]}} &&
+    __CPROVER_forall {int i; (0 <= i && i < len) ==> __CPROVER_exists {int j; 0 <= j && j < len && arr[i] == arr_ghost[j]}} &&
+    __CPROVER_forall {int i; (0 <= i && i < len) ==> __CPROVER_forall {int j; (i <= j && j < len) ==> arr[i] <= arr[j]}} &&
+    1 == 1
+  )
+{
+  if(len <= 1)
+  {
+    return;
+  }
+  int *new_ghost = malloc(len * sizeof(int));
+  memcpy(new_ghost, arr, len * sizeof(int));
+
+  int pivot_idx = partition(new_ghost, arr, len);
+
+  memcpy(new_ghost, arr, len * sizeof(int));
+
+  quicksort(new_ghost, arr, pivot_idx);
+  quicksort(new_ghost, arr + pivot_idx + 1, len - pivot_idx - 1);
+
+  free(new_ghost);
+}
+
+int main()
+{
+  int arr[5] = {1, 2, 3, 0, 4};
+  int arr_ghost[5] = {1, 2, 3, 0, 4};
+  quicksort(arr_ghost, arr, 5);
+}
diff --git a/regression/contracts/quicksort_contracts_01/test.desc b/regression/contracts/quicksort_contracts_01/test.desc
new file mode 100644
index 00000000000..683f54a5b7a
--- /dev/null
+++ b/regression/contracts/quicksort_contracts_01/test.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+main.c
+--check-code-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Loop invariants are overzealous in deciding what counts as side effects.