diff --git a/regression/contracts-dfcc/function-pointer-contracts-enforce/main.c b/regression/contracts-dfcc/function-pointer-contracts-enforce/main.c
deleted file mode 100644
index e91358d6577..00000000000
--- a/regression/contracts-dfcc/function-pointer-contracts-enforce/main.c
+++ /dev/null
@@ -1,65 +0,0 @@
-#include <stdbool.h>
-#include <stdlib.h>
-
-bool nondet_bool();
-
-// type of functions that manipulate arrays
-typedef void (*arr_fun_t)(char *arr, size_t size);
-
-// A contract for the arr_fun_t type
-// requires a fresh array and positive size
-// resets the first element to zero
-void arr_fun_contract(char *arr, size_t size)
-  // clang-format off
-__CPROVER_requires(__CPROVER_is_fresh(arr, size) && size > 0)
-__CPROVER_assigns(arr[0])
-__CPROVER_ensures(arr[0] == 0)
-// clang-format on
-{
-}
-
-arr_fun_t bar()
-  // clang-format off
- __CPROVER_ensures_contract(__CPROVER_return_value, arr_fun_contract)
-// clang-format on
-{
-  // return a function that satisfies the contract
-  return arr_fun_contract;
-}
-
-// Testing pre-conditions constructs
-// Takes a function pointer as input, uses it if its preconditions are met
-int foo(char *arr, size_t size, arr_fun_t arr_fun)
-  // clang-format off
-__CPROVER_requires_contract(arr_fun, arr_fun_contract)
-__CPROVER_requires(arr == NULL || __CPROVER_is_fresh(arr, size))
-__CPROVER_assigns(arr && size > 0: arr[0])
-__CPROVER_ensures(arr && size > 0 ==> (arr[0] == 0 && __CPROVER_return_value == 0))
-__CPROVER_ensures(!(arr && size > 0) ==> __CPROVER_return_value == -1)
-// clang-format on
-{
-  if(nondet_bool())
-    arr_fun = bar(); // non-deterministically get a function pointer from bar()
-
-  int retval = -1;
-  if(arr && size > 0) // check the preconditions of the function pointer
-  {
-    // calls the function pointer to do update the array
-    arr_fun(arr, size);
-    retval = 0;
-  }
-  // the post conditions of foo are established thanks to the post conditions
-  // of arr_fun
-  return retval;
-}
-
-void main()
-{
-  size_t size;
-  char *arr;
-  arr_fun_t arr_fun;
-  // The precondition that `arr_fun` obeys `arr_fun`
-  // and that bar returns a function that obeys `arr_fun`
-  // are used establish the post-conditions of `foo`
-  foo(arr, size, arr_fun);
-}
diff --git a/regression/contracts-dfcc/function-pointer-contracts-enforce/test-manual-swap.desc b/regression/contracts-dfcc/function-pointer-contracts-enforce/test-manual-swap.desc
deleted file mode 100644
index 716ddc6b4ff..00000000000
--- a/regression/contracts-dfcc/function-pointer-contracts-enforce/test-manual-swap.desc
+++ /dev/null
@@ -1,22 +0,0 @@
-CORE
-main.c
---restrict-function-pointer foo.function_pointer_call.1/arr_fun_contract --dfcc main --enforce-contract foo --replace-call-with-contract bar --replace-call-with-contract arr_fun_contract
-^\[arr_fun_contract.assigns.\d+\].*Check that the assigns clause of contract::arr_fun_contract is included in the caller's assigns clause: SUCCESS$
-^\[arr_fun_contract.frees.\d+\].*Check that the frees clause of contract::arr_fun_contract is included in the caller's frees clause: SUCCESS$
-^\[arr_fun_contract.precondition.\d+\].*Check requires clause of contract contract::arr_fun_contract for function arr_fun_contract: SUCCESS$
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
---
-foo requires that a function pointer given as input satisfies
-the contract arr_fun_contract. It nondeterministically updates the function
-pointer by calling the function bar. The new function pointer is also assumed
-to satisfy the same contract by virtue of bar's post conditions.
-Foo then calls the function pointer, after making sure that its preconditions
-are satified.
-We check that the preconditions of arr_fun_contract are checked and satisfied
-and that the assigns clause and frees clause inclusion checks of the function
-pointer against foo are also checked and satisfied.
-In this test, the function pointer is manually swapped with itself so
-goto-instrument should not attempt to wrap it again.
\ No newline at end of file
diff --git a/regression/contracts-dfcc/function-pointer-contracts-enforce/test.desc b/regression/contracts-dfcc/function-pointer-contracts-enforce/test.desc
deleted file mode 100644
index 324d9eea078..00000000000
--- a/regression/contracts-dfcc/function-pointer-contracts-enforce/test.desc
+++ /dev/null
@@ -1,22 +0,0 @@
-CORE
-main.c
---restrict-function-pointer foo.function_pointer_call.1/arr_fun_contract --dfcc main --enforce-contract foo --replace-call-with-contract bar
-^\[arr_fun_contract.assigns.\d+\].*Check that the assigns clause of contract::arr_fun_contract is included in the caller's assigns clause: SUCCESS$
-^\[arr_fun_contract.frees.\d+\].*Check that the frees clause of contract::arr_fun_contract is included in the caller's frees clause: SUCCESS$
-^\[arr_fun_contract.precondition.\d+\].*Check requires clause of contract contract::arr_fun_contract for function arr_fun_contract: SUCCESS$
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
---
-foo requires that a function pointer given as input satisfies
-the contract arr_fun_contract. It nondeterministically updates the function
-pointer by calling the function bar. The new function pointer is also assumed
-to satisfy the same contract by virtue of bar's post conditions.
-Foo then calls the function pointer, after making sure that its preconditions
-are satified.
-We check that the preconditions of arr_fun_contract are checked and satisfied
-and that the assigns clause and frees clause inclusion checks of the function
-pointer against foo are also checked and satisfied.
-In this test, the function pointer contract is automatically discovered and
-swapped with itself.
\ No newline at end of file
diff --git a/regression/contracts-dfcc/function-pointer-contracts-replace/main.c b/regression/contracts-dfcc/function-pointer-contracts-replace/main.c
deleted file mode 100644
index bcdbd1de4bb..00000000000
--- a/regression/contracts-dfcc/function-pointer-contracts-replace/main.c
+++ /dev/null
@@ -1,39 +0,0 @@
-#include <assert.h>
-#include <stdlib.h>
-
-// type of functions that manipulate arrays
-typedef void (*arr_fun_t)(char *arr, size_t size);
-
-// A contract for the arr_fun_t type
-void arr_fun_contract(char *arr, size_t size)
-  // clang-format off
-__CPROVER_requires((size > 0 && __CPROVER_is_fresh(arr, size)))
-__CPROVER_assigns(arr[0])
-__CPROVER_ensures(arr[0] == 0)
-// clang-format on
-{
-}
-
-arr_fun_t foo(arr_fun_t infun, arr_fun_t *outfun)
-  // clang-format off
-__CPROVER_requires_contract(infun, arr_fun_contract)
-__CPROVER_ensures_contract(*outfun, arr_fun_contract)
-__CPROVER_ensures_contract(__CPROVER_return_value, arr_fun_contract)
-// clang-format on
-{
-  *outfun = arr_fun_contract;
-  return infun;
-}
-
-void main()
-{
-  // establish pre-conditions before replacement
-  arr_fun_t infun = arr_fun_contract;
-
-  arr_fun_t outfun1 = NULL;
-  arr_fun_t outfun2 = foo(infun, &outfun1);
-
-  // checking post-conditions after replacement
-  assert(outfun1 == arr_fun_contract);
-  assert(outfun2 == arr_fun_contract);
-}
diff --git a/regression/contracts-dfcc/function-pointer-contracts-replace/test.desc b/regression/contracts-dfcc/function-pointer-contracts-replace/test.desc
deleted file mode 100644
index 6a07d76a425..00000000000
--- a/regression/contracts-dfcc/function-pointer-contracts-replace/test.desc
+++ /dev/null
@@ -1,15 +0,0 @@
-CORE
-main.c
---dfcc main --replace-call-with-contract foo
-^\[foo.precondition.\d+\].*Assert function pointer 'infun_wrapper' obeys contract 'arr_fun_contract': SUCCESS$
-^\[main.assertion.\d+\].*assertion outfun1 == arr_fun_contract: SUCCESS$
-^\[main.assertion.\d+\].*assertion outfun2 == arr_fun_contract: SUCCESS$
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
---
-This test checks that, when replacing a call by its contract,
-requires_contract clauses are translated to equality checks
-and that ensures_contract are translated to assignments of the function pointer
-variable to the contract symbol.
diff --git a/regression/contracts/function-pointer-contracts-enforce/main.c b/regression/contracts/function-pointer-contracts-enforce/main.c
deleted file mode 100644
index 2ec46d402c0..00000000000
--- a/regression/contracts/function-pointer-contracts-enforce/main.c
+++ /dev/null
@@ -1,62 +0,0 @@
-#include <stdbool.h>
-#include <stdlib.h>
-
-bool nondet_bool();
-
-// type of functions that manipulate arrays
-typedef void (*arr_fun_t)(char *arr, size_t size);
-
-// A contract for the arr_fun_t type
-// requires a fresh array and positive size
-// resets the first element to zero
-void contract(char *arr, size_t size)
-  // clang-format off
-__CPROVER_requires((size > 0 && __CPROVER_is_fresh(arr, size)))
-__CPROVER_assigns(arr[0]) 
-__CPROVER_ensures(arr[0] == 0)
-// clang-format on
-{
-}
-
-arr_fun_t bar()
-  // clang-format off
- __CPROVER_ensures_contract(__CPROVER_return_value, contract)
-// clang-format on
-{
-  return contract;
-}
-
-// Testing pre-conditions constructs
-// Takes a function pointer as input, uses it if its preconditions are met
-int foo(char *arr, size_t size, arr_fun_t fun)
-  // clang-format off
-__CPROVER_requires_contract(fun, contract)
-__CPROVER_requires(arr == NULL || __CPROVER_is_fresh(arr, size))
-__CPROVER_assigns(arr && size > 0: arr[0])
-__CPROVER_ensures(arr && size > 0 ==> (arr[0] == 0 && __CPROVER_return_value == 0))
-__CPROVER_ensures(!(arr && size > 0) ==> __CPROVER_return_value == -1)
-// clang-format on
-{
-  if(nondet_bool())
-    fun = bar(); // non-deterministically get a function pointer from bar()
-
-  int retval = -1;
-  if(arr && size > 0)
-  {
-    // calls the function pointer to do update the array
-    fun(arr, size);
-    retval = 0;
-  }
-  return retval;
-}
-
-void main()
-{
-  size_t size;
-  char *arr;
-  arr_fun_t fun;
-  // The precondition that `fun` obeys `contract`
-  // and that bar returns a function that obeys `contract`
-  // are used establish the post-conditions of `foo`
-  foo(arr, size, fun);
-}
diff --git a/regression/contracts/function-pointer-contracts-enforce/test.desc b/regression/contracts/function-pointer-contracts-enforce/test.desc
deleted file mode 100644
index 125f674c36e..00000000000
--- a/regression/contracts/function-pointer-contracts-enforce/test.desc
+++ /dev/null
@@ -1,11 +0,0 @@
-CORE
-main.c
---enforce-contract foo --restrict-function-pointer foo.function_pointer_call.1/contract --replace-call-with-contract contract --replace-call-with-contract bar
-^file main.c line 23: require_contracts or ensures_contract clauses are not supported$
-^EXIT=6$
-^SIGNAL=0$
---
---
-This test checks that we can require that a function pointer satisfies some named
-contract when verifying another function, and successfully replace a call to this 
-function pointer by the contract.
diff --git a/regression/contracts/function-pointer-contracts-replace/main.c b/regression/contracts/function-pointer-contracts-replace/main.c
deleted file mode 100644
index 0f8f8f83395..00000000000
--- a/regression/contracts/function-pointer-contracts-replace/main.c
+++ /dev/null
@@ -1,39 +0,0 @@
-#include <assert.h>
-#include <stdlib.h>
-
-// type of functions that manipulate arrays
-typedef void (*arr_fun_t)(char *arr, size_t size);
-
-// A contract for the arr_fun_t type
-void contract(char *arr, size_t size)
-  // clang-format off
-__CPROVER_requires((size > 0 && __CPROVER_is_fresh(arr, size)))
-__CPROVER_assigns(arr[0]) 
-__CPROVER_ensures(arr[0] == 0)
-// clang-format on
-{
-}
-
-arr_fun_t foo(arr_fun_t infun, arr_fun_t *outfun)
-  // clang-format off
-__CPROVER_requires_contract(infun, contract)
-__CPROVER_ensures_contract(*outfun, contract)
-__CPROVER_ensures_contract(__CPROVER_return_value, contract)
-// clang-format on
-{
-  *outfun = contract;
-  return infun;
-}
-
-void main()
-{
-  // establish pre-conditions before replacement
-  arr_fun_t infun = contract;
-
-  arr_fun_t outfun1 = NULL;
-  arr_fun_t outfun2 = foo(infun, &outfun1);
-
-  // checking post-conditions after replacement
-  assert(outfun1 == contract);
-  assert(outfun2 == contract);
-}
diff --git a/regression/contracts/function-pointer-contracts-replace/test.desc b/regression/contracts/function-pointer-contracts-replace/test.desc
deleted file mode 100644
index e0208f3bd4f..00000000000
--- a/regression/contracts/function-pointer-contracts-replace/test.desc
+++ /dev/null
@@ -1,11 +0,0 @@
-CORE
-main.c
---replace-call-with-contract foo
-^file main.c line 19 function foo: require_contracts or ensures_contract clauses are not supported$
-^EXIT=6$
-^SIGNAL=0$
---
---
-This test checks that, when replacing a call by its contract,
-requires_contract clauses are translated to equality checks
-and that ensures_contract are translated to assignments.
diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp
index 014f1050cf6..431a9f0a908 100644
--- a/src/ansi-c/ansi_c_convert_type.cpp
+++ b/src/ansi-c/ansi_c_convert_type.cpp
@@ -258,12 +258,6 @@ void ansi_c_convert_typet::read_rec(const typet &type)
       static_cast<const exprt &>(static_cast<const irept &>(type));
     requires.push_back(to_unary_expr(as_expr).op());
   }
-  else if(type.id() == ID_C_spec_requires_contract)
-  {
-    const exprt &as_expr =
-      static_cast<const exprt &>(static_cast<const irept &>(type));
-    requires_contract.push_back(to_unary_expr(as_expr).op());
-  }
   else if(type.id() == ID_C_spec_assigns)
   {
     const exprt &as_expr =
@@ -286,12 +280,6 @@ void ansi_c_convert_typet::read_rec(const typet &type)
       static_cast<const exprt &>(static_cast<const irept &>(type));
     ensures.push_back(to_unary_expr(as_expr).op());
   }
-  else if(type.id() == ID_C_spec_ensures_contract)
-  {
-    const exprt &as_expr =
-      static_cast<const exprt &>(static_cast<const irept &>(type));
-    ensures_contract.push_back(to_unary_expr(as_expr).op());
-  }
   else
     other.push_back(type);
 }
@@ -341,10 +329,6 @@ void ansi_c_convert_typet::write(typet &type)
     if(!requires.empty())
       to_code_with_contract_type(type).requires() = std::move(requires);
 
-    if(!requires_contract.empty())
-      to_code_with_contract_type(type).requires_contract() =
-        std::move(requires_contract);
-
     if(!assigns.empty())
       to_code_with_contract_type(type).assigns() = std::move(assigns);
 
@@ -354,10 +338,6 @@ void ansi_c_convert_typet::write(typet &type)
     if(!ensures.empty())
       to_code_with_contract_type(type).ensures() = std::move(ensures);
 
-    if(!ensures_contract.empty())
-      to_code_with_contract_type(type).ensures_contract() =
-        std::move(ensures_contract);
-
     if(constructor || destructor)
     {
       if(constructor && destructor)
diff --git a/src/ansi-c/ansi_c_convert_type.h b/src/ansi-c/ansi_c_convert_type.h
index 1eabc279006..7aff1a9953b 100644
--- a/src/ansi-c/ansi_c_convert_type.h
+++ b/src/ansi-c/ansi_c_convert_type.h
@@ -47,8 +47,7 @@ class ansi_c_convert_typet:public messaget
   bool constructor, destructor;
 
   // contracts
-  exprt::operandst assigns, frees, ensures, requires, ensures_contract,
-    requires_contract;
+  exprt::operandst assigns, frees, ensures, requires;
 
   // storage spec
   c_storage_spect c_storage_spec;
diff --git a/src/ansi-c/c_expr.h b/src/ansi-c/c_expr.h
index 9ab48212c78..c58c4e41716 100644
--- a/src/ansi-c/c_expr.h
+++ b/src/ansi-c/c_expr.h
@@ -320,106 +320,4 @@ to_conditional_target_group_expr(exprt &expr)
   return ret;
 }
 
-/// \brief A class for expressions representing a
-/// `requires_contract(fptr, contract)` clause
-/// or an `ensures_contract(fptr, contract)` clause
-/// in a function contract.
-class function_pointer_obeys_contract_exprt : public exprt
-{
-public:
-  explicit function_pointer_obeys_contract_exprt(
-    exprt _function_pointer,
-    exprt _contract)
-    : exprt(ID_function_pointer_obeys_contract, empty_typet{})
-  {
-    add_to_operands(std::move(_function_pointer));
-    add_to_operands(std::move(_contract));
-  }
-
-  static void check(
-    const exprt &expr,
-    const validation_modet vm = validation_modet::INVARIANT)
-  {
-    DATA_CHECK(
-      vm,
-      expr.operands().size() == 2,
-      "function pointer obeys contract expression must have two operands");
-  }
-
-  static void validate(
-    const exprt &expr,
-    const namespacet &,
-    const validation_modet vm = validation_modet::INVARIANT)
-  {
-    check(expr, vm);
-  }
-
-  const exprt &function_pointer() const
-  {
-    return op0();
-  }
-
-  exprt &function_pointer()
-  {
-    return op0();
-  }
-
-  const symbol_exprt &contract_symbol_expr() const
-  {
-    return to_symbol_expr(op1().operands().at(0));
-  }
-
-  symbol_exprt &contract_symbol_expr()
-  {
-    return to_symbol_expr(op1().operands().at(0));
-  }
-
-  const exprt &address_of_contract() const
-  {
-    return op1();
-  }
-
-  exprt &address_of_contract()
-  {
-    return op1();
-  }
-};
-
-inline void validate_expr(const function_pointer_obeys_contract_exprt &value)
-{
-  function_pointer_obeys_contract_exprt::check(value);
-}
-
-template <>
-inline bool
-can_cast_expr<function_pointer_obeys_contract_exprt>(const exprt &base)
-{
-  return base.id() == ID_function_pointer_obeys_contract;
-}
-
-/// \brief Cast an exprt to a \ref function_pointer_obeys_contract_exprt
-///
-/// \a expr must be known to be \ref function_pointer_obeys_contract_exprt
-///
-/// \param expr: Source expression
-/// \return Object of type \ref function_pointer_obeys_contract_exprt
-inline const function_pointer_obeys_contract_exprt &
-to_function_pointer_obeys_contract_expr(const exprt &expr)
-{
-  PRECONDITION(expr.id() == ID_function_pointer_obeys_contract);
-  auto &ret = static_cast<const function_pointer_obeys_contract_exprt &>(expr);
-  validate_expr(ret);
-  return ret;
-}
-
-/// \copydoc to_function_pointer_obeys_contract_expr(const exprt &expr)
-inline function_pointer_obeys_contract_exprt &
-to_function_pointer_obeys_contract_expr(exprt &expr)
-{
-  PRECONDITION(expr.id() == ID_function_pointer_obeys_contract);
-  auto &ret = static_cast<function_pointer_obeys_contract_exprt &>(expr);
-  validate_expr(ret);
-  return ret;
-}
-
 #endif // CPROVER_ANSI_C_C_EXPR_H
diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp
index 4870c033487..9c4d97c52d6 100644
--- a/src/ansi-c/c_typecheck_base.cpp
+++ b/src/ansi-c/c_typecheck_base.cpp
@@ -860,16 +860,6 @@ void c_typecheck_baset::typecheck_declaration(
             parameter_identifier, p.type());
         }
 
-        for(auto &expr : code_type.requires_contract())
-        {
-          typecheck_spec_function_pointer_obeys_contract(expr);
-          std::string clause_type = "function pointer preconditions";
-          check_history_expr_return_value(expr, clause_type);
-          lambda_exprt lambda{temporary_parameter_symbols, expr};
-          lambda.add_source_location() = expr.source_location();
-          expr.swap(lambda);
-        }
-
         for(auto &requires : code_type.requires())
         {
           typecheck_expr(requires);
@@ -900,18 +890,6 @@ void c_typecheck_baset::typecheck_declaration(
           frees.swap(lambda);
         }
 
-        for(auto &expr : code_type.ensures_contract())
-        {
-          typecheck_spec_function_pointer_obeys_contract(expr);
-          disallow_subexpr_by_id(
-            expr,
-            ID_loop_entry,
-            CPROVER_PREFIX "loop_entry is not allowed in postconditions.");
-          lambda_exprt lambda{temporary_parameter_symbols, expr};
-          lambda.add_source_location() = expr.source_location();
-          expr.swap(lambda);
-        }
-
         for(auto &ensures : code_type.ensures())
         {
           typecheck_expr(ensures);
@@ -954,9 +932,7 @@ void c_typecheck_baset::typecheck_declaration(
         new_symbol.type.remove(ID_C_spec_assigns);
         new_symbol.type.remove(ID_C_spec_frees);
         new_symbol.type.remove(ID_C_spec_ensures);
-        new_symbol.type.remove(ID_C_spec_ensures_contract);
         new_symbol.type.remove(ID_C_spec_requires);
-        new_symbol.type.remove(ID_C_spec_requires_contract);
       }
     }
   }
diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h
index 0666537b398..6ac270196cd 100644
--- a/src/ansi-c/c_typecheck_base.h
+++ b/src/ansi-c/c_typecheck_base.h
@@ -157,7 +157,6 @@ class c_typecheck_baset:
   /// is found in expr.
   virtual void check_was_freed(const exprt &expr, std::string &clause_type);
 
-  virtual void typecheck_spec_function_pointer_obeys_contract(exprt &expr);
   virtual void typecheck_spec_assigns(exprt::operandst &targets);
   virtual void typecheck_spec_frees(exprt::operandst &targets);
   virtual void typecheck_conditional_targets(
diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp
index 80f095b4a79..df68d74adcc 100644
--- a/src/ansi-c/c_typecheck_code.cpp
+++ b/src/ansi-c/c_typecheck_code.cpp
@@ -1096,88 +1096,6 @@ void c_typecheck_baset::typecheck_spec_frees_target(exprt &target)
   }
 }
 
-void c_typecheck_baset::typecheck_spec_function_pointer_obeys_contract(
-  exprt &expr)
-{
-  if(!can_cast_expr<function_pointer_obeys_contract_exprt>(expr))
-  {
-    error().source_location = expr.source_location();
-    error() << "expected ID_function_pointer_obeys_contract expression in "
-               "requires_contract/ensures_contract clause, found "
-            << expr.id() << eom;
-    throw 0;
-  }
-
-  auto &obeys_expr = to_function_pointer_obeys_contract_expr(expr);
-
-  validate_expr(obeys_expr);
-
-  // the first parameter must be a function pointer typed assignable path
-  // expression, without side effects or ternary operator
-  auto &function_pointer = obeys_expr.function_pointer();
-  typecheck_expr(function_pointer);
-
-  if(
-    function_pointer.type().id() != ID_pointer ||
-    to_pointer_type(function_pointer.type()).base_type().id() != ID_code)
-  {
-    error().source_location = expr.source_location();
-    error() << "the first parameter of the clause must be a function pointer "
-               "expression"
-            << eom;
-    throw 0;
-  }
-
-  if(!function_pointer.get_bool(ID_C_lvalue))
-  {
-    error().source_location = function_pointer.source_location();
-    error() << "first parameter of the clause must be an lvalue" << eom;
-    throw 0;
-  }
-
-  if(has_subexpr(function_pointer, ID_side_effect))
-  {
-    error().source_location = function_pointer.source_location();
-    error() << "first parameter of the clause must have no side-effects" << eom;
-    throw 0;
-  }
-
-  if(has_subexpr(function_pointer, ID_if))
-  {
-    error().source_location = function_pointer.source_location();
-    error() << "first parameter of the clause must have no ternary operator"
-            << eom;
-    throw 0;
-  }
-
-  // second parameter must be the address of a function symbol
-  auto &address_of_contract = obeys_expr.address_of_contract();
-  typecheck_expr(address_of_contract);
-
-  if(
-    address_of_contract.id() != ID_address_of ||
-    to_address_of_expr(address_of_contract).object().id() != ID_symbol ||
-    address_of_contract.type().id() != ID_pointer ||
-    to_pointer_type(address_of_contract.type()).base_type().id() != ID_code)
-  {
-    error().source_location = expr.source_location();
-    error() << "the second parameter of the requires_contract/ensures_contract "
-               "clause must be a function symbol"
-            << eom;
-    throw 0;
-  }
-
-  if(function_pointer.type() != address_of_contract.type())
-  {
-    error().source_location = expr.source_location();
-    error() << "the first and second parameter of the "
-               "requires_contract/ensures_contract clause must have the same "
-               "function pointer type "
-            << eom;
-    throw 0;
-  }
-}
-
 void c_typecheck_baset::typecheck_spec_loop_invariant(codet &code)
 {
   if(code.find(ID_C_spec_loop_invariant).is_not_nil())
diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y
index 16fd64254d9..abb8b2246bb 100644
--- a/src/ansi-c/parser.y
+++ b/src/ansi-c/parser.y
@@ -204,9 +204,7 @@ extern char *yyansi_ctext;
 %token TOK_CPROVER_ID  "__CPROVER_ID"
 %token TOK_CPROVER_LOOP_INVARIANT  "__CPROVER_loop_invariant"
 %token TOK_CPROVER_DECREASES "__CPROVER_decreases"
-%token TOK_CPROVER_REQUIRES_CONTRACT "__CPROVER_requires_contract"
 %token TOK_CPROVER_REQUIRES  "__CPROVER_requires"
-%token TOK_CPROVER_ENSURES_CONTRACT "__CPROVER_ensures_contract"
 %token TOK_CPROVER_ENSURES  "__CPROVER_ensures"
 %token TOK_CPROVER_ASSIGNS "__CPROVER_assigns"
 %token TOK_CPROVER_FREES "__CPROVER_frees"
@@ -3299,26 +3297,6 @@ cprover_function_contract:
           set($$, ID_C_spec_requires);
           mto($$, $3);
         }
-        | TOK_CPROVER_ENSURES_CONTRACT '(' unary_expression ',' unary_expression ')'
-        {
-          $$=$1;
-          set($$, ID_C_spec_ensures_contract);
-          exprt tmp(ID_function_pointer_obeys_contract);
-          tmp.add_to_operands(std::move(parser_stack($3)));
-          tmp.add_to_operands(std::move(parser_stack($5)));
-          tmp.add_source_location()=parser_stack($$).source_location();
-          parser_stack($$).add_to_operands(std::move(tmp));
-        }
-        | TOK_CPROVER_REQUIRES_CONTRACT '(' unary_expression ',' unary_expression ')'
-        {
-          $$=$1;
-          set($$, ID_C_spec_requires_contract);
-          exprt tmp(ID_function_pointer_obeys_contract);
-          tmp.add_to_operands(std::move(parser_stack($3)));
-          tmp.add_to_operands(std::move(parser_stack($5)));
-          tmp.add_source_location()=parser_stack($$).source_location();
-          parser_stack($$).add_to_operands(std::move(tmp));
-        }
         | cprover_contract_assigns
         | cprover_contract_frees
         ;
diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l
index 8e99bfd9d82..48a30605e3b 100644
--- a/src/ansi-c/scanner.l
+++ b/src/ansi-c/scanner.l
@@ -1293,8 +1293,6 @@ __decltype          { if(PARSER.cpp98 &&
 {CPROVER_PREFIX}"ensures"      { loc(); return TOK_CPROVER_ENSURES; }
 {CPROVER_PREFIX}"assigns"      { loc(); return TOK_CPROVER_ASSIGNS; }
 {CPROVER_PREFIX}"frees"        { loc(); return TOK_CPROVER_FREES; }
-{CPROVER_PREFIX}"requires_contract" { loc(); return TOK_CPROVER_REQUIRES_CONTRACT; }
-{CPROVER_PREFIX}"ensures_contract" { loc(); return TOK_CPROVER_ENSURES_CONTRACT; }
 
 "\xe2\x88\x80" |
 "\\forall"      { /* Non-standard, obviously. Found in ACSL syntax. */
diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp
index 5db3567eb3b..f7b1a2ffb48 100644
--- a/src/goto-instrument/contracts/contracts.cpp
+++ b/src/goto-instrument/contracts/contracts.cpp
@@ -654,17 +654,6 @@ void code_contractst::apply_function_contract(
       _location);
   }
 
-  // Translate requires_contract(ptr, contract) clauses to assertions
-  for(auto &expr : type.requires_contract())
-  {
-    assert_function_pointer_obeys_contract(
-      to_function_pointer_obeys_contract_expr(
-        to_lambda_expr(expr).application(instantiation_values)),
-      ID_precondition,
-      mode,
-      new_program);
-  }
-
   // Generate all the instructions required to initialize history variables
   exprt::operandst instantiated_ensures_clauses;
   for(auto clause : type.ensures())
@@ -742,16 +731,6 @@ void code_contractst::apply_function_contract(
       _location);
   }
 
-  // Translate ensures_contract(ptr, contract) clauses to assumptions
-  for(auto &expr : type.ensures_contract())
-  {
-    assume_function_pointer_obeys_contract(
-      to_function_pointer_obeys_contract_expr(
-        to_lambda_expr(expr).application(instantiation_values)),
-      mode,
-      new_program);
-  }
-
   // Kill return value variable if fresh
   if(call_ret_is_fresh_var)
   {
@@ -1194,27 +1173,6 @@ void code_contractst::enforce_contract(const irep_idt &function)
   add_contract_check(original, mangled, wrapper.body);
 }
 
-void code_contractst::assert_function_pointer_obeys_contract(
-  const function_pointer_obeys_contract_exprt &expr,
-  const irep_idt &property_class,
-  const irep_idt &mode,
-  goto_programt &dest)
-{
-  throw invalid_source_file_exceptiont(
-    "require_contracts or ensures_contract clauses are not supported",
-    expr.source_location());
-}
-
-void code_contractst::assume_function_pointer_obeys_contract(
-  const function_pointer_obeys_contract_exprt &expr,
-  const irep_idt &mode,
-  goto_programt &dest)
-{
-  throw invalid_source_file_exceptiont(
-    "require_contracts or ensures_contract clauses are not supported",
-    expr.source_location());
-}
-
 void code_contractst::add_contract_check(
   const irep_idt &wrapper_function,
   const irep_idt &mangled_function,
@@ -1331,16 +1289,6 @@ void code_contractst::add_contract_check(
     instantiated_ensures_clauses.push_back(instantiated_clause);
   }
 
-  // Translate requires_contract(ptr, contract) clauses to assumptions
-  for(auto &expr : code_type.requires_contract())
-  {
-    assume_function_pointer_obeys_contract(
-      to_function_pointer_obeys_contract_expr(
-        to_lambda_expr(expr).application(instantiation_values)),
-      function_symbol.mode,
-      check);
-  }
-
   // ret=mangled_function(parameter1, ...)
   check.add(goto_programt::make_function_call(call, source_location));
 
@@ -1360,16 +1308,6 @@ void code_contractst::add_contract_check(
       _location);
   }
 
-  // Translate ensures_contract(ptr, contract) clauses to assertions
-  for(auto &expr : code_type.ensures_contract())
-  {
-    assert_function_pointer_obeys_contract(
-      to_function_pointer_obeys_contract_expr(
-        to_lambda_expr(expr).application(instantiation_values)),
-      ID_postcondition,
-      function_symbol.mode,
-      check);
-  }
   if(code_type.return_type() != empty_typet())
   {
     check.add(goto_programt::make_set_return_value(
diff --git a/src/goto-instrument/contracts/contracts.h b/src/goto-instrument/contracts/contracts.h
index 7372f1600ee..a6024782fc5 100644
--- a/src/goto-instrument/contracts/contracts.h
+++ b/src/goto-instrument/contracts/contracts.h
@@ -44,7 +44,6 @@ Date: February 2016
   " --enforce-contract <fun>     wrap fun with an assertion of its contract\n"
 
 class local_may_aliast;
-class function_pointer_obeys_contract_exprt;
 
 class code_contractst
 {
@@ -139,32 +138,6 @@ class code_contractst
   std::list<std::string> loop_names;
 
 public:
-  /// Translates a function_pointer_obeys_contract_exprt into an assertion
-  /// ```
-  /// ASSERT function_pointer == contract;
-  /// ```
-  /// \param expr expression to translate
-  /// \param property_class property class to use for the generated assertions
-  /// \param mode language mode to use for goto_conversion and prints
-  /// \param dest goto_program where generated instructions are appended
-  void assert_function_pointer_obeys_contract(
-    const function_pointer_obeys_contract_exprt &expr,
-    const irep_idt &property_class,
-    const irep_idt &mode,
-    goto_programt &dest);
-
-  /// Translates a function_pointer_obeys_contract_exprt into an assignment
-  /// ```
-  /// ASSIGN function_pointer = contract;
-  /// ```
-  /// \param expr expression to translate
-  /// \param mode language mode to use for goto_conversion and prints
-  /// \param dest goto_program where generated instructions are appended
-  void assume_function_pointer_obeys_contract(
-    const function_pointer_obeys_contract_exprt &expr,
-    const irep_idt &mode,
-    goto_programt &dest);
-
   /// \brief Enforce contract of a single function
   void enforce_contract(const irep_idt &function);
 
diff --git a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-contract-checking.md b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-contract-checking.md
index 2f453970dc4..d6466b41972 100644
--- a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-contract-checking.md
+++ b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-contract-checking.md
@@ -97,7 +97,6 @@ ret_t foo(foo-parameters, write_set_t caller_write_set) {
 
   // assume requires clauses
   assume(contract::requires(foo_params, requires_write_set));
-  assume(contract::requires_contract(foo_params, requires_write_set));
 
   // check that requires clause do not allocate or deallocate dynamic memory
   assert(__CPROVER_contracts_write_set_allocated_deallocated_is_empty(requires_write_set));
@@ -128,7 +127,6 @@ ret_t foo(foo-parameters, write_set_t caller_write_set) {
 
   // check post conditions
   assert(contract::ensures(foo_params, ensures_write_set));
-  assert(contract::ensures_contract(foo_params, ensures_write_set));
 
   // check that requires clause do not allocate or deallocate dynamic memory
   assert(__CPROVER_contracts_write_set_allocated_deallocated_is_empty(ensures_write_set));
diff --git a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-contract-replacement.md b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-contract-replacement.md
index 9b45b869501..3815bfaeeef 100644
--- a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-contract-replacement.md
+++ b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-contract-replacement.md
@@ -37,7 +37,6 @@ ret_t foo(foo_params, write_set_t caller_write_set) {
 
   // assert requires clauses
   assert(contract::requires(foo_params, requires_write_set));
-  assert(contract::requires_contract(foo_params, requires_write_set));
 
   // snapshot history variables
   hist1_t hist1 = ...;
@@ -82,7 +81,6 @@ ret_t foo(foo_params, write_set_t caller_write_set) {
 
   // assume post conditions
   assume(contract::ensures(foo_params, ensures_write_set));
-  assume(contract::ensures_contract(foo_params, ensures_write_set));
 
   // postamble
   assert(__CPROVER_contracts_write_set_check_allocated_deallocated_is_empty(ensures_write_set));
diff --git a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-reminder.md b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-reminder.md
index a7fb8c259ad..57b16f74659 100644
--- a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-reminder.md
+++ b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-reminder.md
@@ -15,11 +15,9 @@ definition:
 ret_t foo(parameters)
 // preconditions
 __CPROVER_requires(R)
-__CPROVER_requires_contract(P, C)
 
 // postconditions
 __CPROVER_ensures(E)
-__CPROVER_ensures_contract(P, C)
 
 // frame conditions
 __CPROVER_assigns(A)
@@ -31,20 +29,12 @@ __CPROVER_frees(F)
   precondition as boolean expression R that may only depend on program globals,
   function parameters, [memory predicates](@ref contracts-memory-predicates) and
   deterministic, side effect-free function calls;
-- A `__CPROVER_requires_contract` clause clause specifies the precondition that
-  a function pointer expression P satisfies a contract C, where P may only
-  depend on program globals and function parameters;
 - A `__CPROVER_ensures` clause (@ref contracts-requires-ensures) specifies a
   postcondition as boolean expression E that may only depend on program globals,
   function parameters, [memory predicates](@ref contracts-memory-predicates),
   deterministic, side effect-free function calls,
   [history variables](@ref contracts-history-variables), and the special
   variable `__CPROVER_return_value`;
-- A `__CPROVER_ensures_contract` clause specifies the postcondition that a
-  function pointer expression P satisfies a contract C, where P may only depend
-  on program globals, function parameters,
-  [history variables](@ref contracts-history-variables) and the special
-  variable `__CPROVER_return_value`;
 - A `__CPROVER_assigns` clause (@ref contracts-assigns) specifies a set A of
   memory locations that may be assigned to by any function satisfying the
   contract;
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.h
index 523f4408f21..95d9721de98 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.h
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.h
@@ -32,7 +32,6 @@ class dfcc_utilst;
 class dfcc_spec_functionst;
 class code_with_contract_typet;
 class conditional_target_group_exprt;
-class function_pointer_obeys_contract_exprt;
 
 /// Generates GOTO functions modelling a contract assigns and frees clauses.
 ///
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.h
index 2d21a4c17f3..11bcae93fe3 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.h
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.h
@@ -32,7 +32,6 @@ class dfcc_instrumentt;
 class dfcc_spec_functionst;
 class code_with_contract_typet;
 class conditional_target_group_exprt;
-class function_pointer_obeys_contract_exprt;
 
 /// A contract is represented by a function declaration or definition
 /// with contract clauses attached to its signature:
@@ -40,11 +39,9 @@ class function_pointer_obeys_contract_exprt;
 /// ```
 /// ret_t foo(foo_params)
 /// __CPROVER_requires(R)
-/// __CPROVER_requires_contract(ptr, contract)
 /// __CPROVER_assigns(A)
 /// __CPROVER_frees(F)
 /// __CPROVER_ensures(E)
-/// __CPROVER_ensures_contract(ptr, contract)
 /// { foo_body; } [optional]
 /// ```
 ///
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp
index 6ef75380955..967dc0fbbf3 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp
@@ -249,11 +249,9 @@ dfcc_wrapper_programt::dfcc_wrapper_programt(
   encode_ensures_write_set();
   encode_is_fresh_set();
   encode_requires_clauses();
-  encode_requires_contract_clauses();
   encode_contract_write_set();
   encode_function_call();
   encode_ensures_clauses();
-  encode_ensures_contract_clauses();
 }
 
 void dfcc_wrapper_programt::add_to_dest(
@@ -798,127 +796,6 @@ void dfcc_wrapper_programt::encode_ensures_clauses()
   postconditions.destructive_append(ensures_program);
 }
 
-void dfcc_wrapper_programt::encode_requires_contract_clauses()
-{
-  const auto &requires_contract = contract_code_type.requires_contract();
-
-  if(contract_mode == dfcc_contract_modet::CHECK)
-  {
-    for(auto &expr : requires_contract)
-    {
-      auto instance =
-        to_lambda_expr(expr).application(contract_lambda_parameters);
-      instance.add_source_location() = expr.source_location();
-      INVARIANT(
-        can_cast_expr<function_pointer_obeys_contract_exprt>(instance),
-        "instance ok");
-
-      assume_function_pointer_obeys_contract(
-        to_function_pointer_obeys_contract_expr(instance), preconditions);
-    }
-  }
-  else
-  {
-    for(auto &expr : requires_contract)
-    {
-      auto instance =
-        to_lambda_expr(expr).application(contract_lambda_parameters);
-      instance.add_source_location() = expr.source_location();
-      INVARIANT(
-        can_cast_expr<function_pointer_obeys_contract_exprt>(instance),
-        "instance ok");
-
-      assert_function_pointer_obeys_contract(
-        to_function_pointer_obeys_contract_expr(instance),
-        ID_precondition,
-        preconditions);
-    }
-  }
-}
-
-void dfcc_wrapper_programt::encode_ensures_contract_clauses()
-{
-  const auto &ensures_contract = contract_code_type.ensures_contract();
-
-  if(contract_mode == dfcc_contract_modet::CHECK)
-  {
-    for(auto &expr : ensures_contract)
-    {
-      auto instance =
-        to_lambda_expr(expr).application(contract_lambda_parameters);
-      instance.add_source_location() = expr.source_location();
-      INVARIANT(
-        can_cast_expr<function_pointer_obeys_contract_exprt>(instance),
-        "instance ok");
-      assert_function_pointer_obeys_contract(
-        to_function_pointer_obeys_contract_expr(instance),
-        ID_postcondition,
-        postconditions);
-    }
-  }
-  else
-  {
-    for(auto &expr : ensures_contract)
-    {
-      auto instance =
-        to_lambda_expr(expr).application(contract_lambda_parameters);
-      instance.add_source_location() = expr.source_location();
-      INVARIANT(
-        can_cast_expr<function_pointer_obeys_contract_exprt>(instance),
-        "instance ok");
-      assume_function_pointer_obeys_contract(
-        to_function_pointer_obeys_contract_expr(instance), postconditions);
-    }
-  }
-}
-
-void dfcc_wrapper_programt::assert_function_pointer_obeys_contract(
-  const function_pointer_obeys_contract_exprt &expr,
-  const irep_idt &property_class,
-  goto_programt &dest)
-{
-  function_pointer_contracts.insert(
-    expr.contract_symbol_expr().get_identifier());
-  source_locationt loc(expr.source_location());
-  loc.set_property_class(property_class);
-  std::stringstream comment;
-  comment << "Assert function pointer '"
-          << from_expr_using_mode(
-               ns, contract_symbol.mode, expr.function_pointer())
-          << "' obeys contract '"
-          << from_expr_using_mode(
-               ns, contract_symbol.mode, expr.address_of_contract())
-          << "'";
-  loc.set_comment(comment.str());
-  code_assertt assert_expr(
-    equal_exprt{expr.function_pointer(), expr.address_of_contract()});
-  assert_expr.add_source_location() = loc;
-  goto_programt instructions;
-  converter.goto_convert(assert_expr, instructions, contract_symbol.mode);
-  dest.destructive_append(instructions);
-}
-
-void dfcc_wrapper_programt::assume_function_pointer_obeys_contract(
-  const function_pointer_obeys_contract_exprt &expr,
-  goto_programt &dest)
-{
-  function_pointer_contracts.insert(
-    expr.contract_symbol_expr().get_identifier());
-
-  source_locationt loc(expr.source_location());
-  std::stringstream comment;
-  comment << "Assume function pointer '"
-          << from_expr_using_mode(
-               ns, contract_symbol.mode, expr.function_pointer())
-          << "' obeys contract '"
-          << from_expr_using_mode(
-               ns, contract_symbol.mode, expr.contract_symbol_expr())
-          << "'";
-  loc.set_comment(comment.str());
-  dest.add(goto_programt::make_assignment(
-    expr.function_pointer(), expr.address_of_contract(), loc));
-}
-
 void dfcc_wrapper_programt::encode_function_call()
 {
   if(contract_mode == dfcc_contract_modet::CHECK)
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h
index ed7210895bf..8b108d0a60d 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h
@@ -233,38 +233,9 @@ class dfcc_wrapper_programt
   /// Encodes preconditions, instruments them to check for side effects
   void encode_requires_clauses();
 
-  /// Encodes function pointer preconditions
-  void encode_requires_contract_clauses();
-
   /// Encodes postconditions, instruments them to check for side effects
   void encode_ensures_clauses();
 
-  /// Encodes function pointer postconditions
-  void encode_ensures_contract_clauses();
-
-  /// Translates a function_pointer_obeys_contract_exprt into an assertion
-  /// ```
-  /// ASSERT function_pointer == contract;
-  /// ```
-  ///
-  /// \param expr expression to translate
-  /// \param property_class property class to use for the generated assertions
-  /// \param dest goto_program where generated instructions are appended
-  void assert_function_pointer_obeys_contract(
-    const function_pointer_obeys_contract_exprt &expr,
-    const irep_idt &property_class,
-    goto_programt &dest);
-
-  /// Translates a function_pointer_obeys_contract_exprt into an assignment
-  /// ```
-  /// ASSIGN function_pointer = contract;
-  /// ```
-  /// \param expr expression to translate
-  /// \param dest goto_program where generated instructions are appended
-  void assume_function_pointer_obeys_contract(
-    const function_pointer_obeys_contract_exprt &expr,
-    goto_programt &dest);
-
   /// Encodes the function call section of the wrapper program.
   void encode_function_call();
 
diff --git a/src/linking/remove_internal_symbols.cpp b/src/linking/remove_internal_symbols.cpp
index e26a85cbd8d..dc5218ae7fc 100644
--- a/src/linking/remove_internal_symbols.cpp
+++ b/src/linking/remove_internal_symbols.cpp
@@ -71,12 +71,8 @@ static void get_symbols(
         find_type_and_expr_symbols(a, new_symbols);
       for(const exprt &e : maybe_contract.ensures())
         find_type_and_expr_symbols(e, new_symbols);
-      for(const exprt &e : maybe_contract.ensures_contract())
-        find_type_and_expr_symbols(e, new_symbols);
       for(const exprt &r : maybe_contract.requires())
         find_type_and_expr_symbols(r, new_symbols);
-      for(const exprt &r : maybe_contract.requires_contract())
-        find_type_and_expr_symbols(r, new_symbols);
 
       for(const auto &s : new_symbols)
       {
diff --git a/src/util/c_types.h b/src/util/c_types.h
index 8c569aceb56..00460e56f27 100644
--- a/src/util/c_types.h
+++ b/src/util/c_types.h
@@ -368,9 +368,8 @@ class code_with_contract_typet : public code_typet
 
   bool has_contract() const
   {
-    return !ensures().empty() || !ensures_contract().empty() ||
-           !requires().empty() || !requires_contract().empty() ||
-           !assigns().empty() || !frees().empty();
+    return !ensures().empty() || !requires().empty() || !assigns().empty() ||
+           !frees().empty();
   }
 
   const exprt::operandst &assigns() const
@@ -393,17 +392,6 @@ class code_with_contract_typet : public code_typet
     return static_cast<exprt &>(add(ID_C_spec_frees)).operands();
   }
 
-  const exprt::operandst &requires_contract() const
-  {
-    return static_cast<const exprt &>(find(ID_C_spec_requires_contract))
-      .operands();
-  }
-
-  exprt::operandst &requires_contract()
-  {
-    return static_cast<exprt &>(add(ID_C_spec_requires_contract)).operands();
-  }
-
   const exprt::operandst &requires() const
   {
     return static_cast<const exprt &>(find(ID_C_spec_requires)).operands();
@@ -414,17 +402,6 @@ class code_with_contract_typet : public code_typet
     return static_cast<exprt &>(add(ID_C_spec_requires)).operands();
   }
 
-  const exprt::operandst &ensures_contract() const
-  {
-    return static_cast<const exprt &>(find(ID_C_spec_ensures_contract))
-      .operands();
-  }
-
-  exprt::operandst &ensures_contract()
-  {
-    return static_cast<exprt &>(add(ID_C_spec_ensures_contract)).operands();
-  }
-
   const exprt::operandst &ensures() const
   {
     return static_cast<const exprt &>(find(ID_C_spec_ensures)).operands();
diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def
index 50c3bfa306d..9eeb476691d 100644
--- a/src/util/irep_ids.def
+++ b/src/util/irep_ids.def
@@ -581,15 +581,12 @@ IREP_ID_ONE(used)
 IREP_ID_ONE(is_used)
 IREP_ID_TWO(C_spec_loop_invariant, #spec_loop_invariant)
 IREP_ID_TWO(C_spec_decreases, #spec_decreases)
-IREP_ID_TWO(C_spec_requires_contract, #spec_requires_contract)
 IREP_ID_TWO(C_spec_requires, #spec_requires)
-IREP_ID_TWO(C_spec_ensures_contract, #spec_ensures_contract)
 IREP_ID_TWO(C_spec_ensures, #spec_ensures)
 IREP_ID_TWO(C_spec_assigns, #spec_assigns)
 IREP_ID_TWO(C_spec_frees, #spec_frees)
 IREP_ID_ONE(target_list)
 IREP_ID_ONE(conditional_target_group)
-IREP_ID_ONE(function_pointer_obeys_contract)
 IREP_ID_ONE(virtual_function)
 IREP_ID_TWO(element_type, element_type)
 IREP_ID_ONE(working_directory)
diff --git a/src/util/rename_symbol.cpp b/src/util/rename_symbol.cpp
index 9b950c0d013..9df1b2ee1f0 100644
--- a/src/util/rename_symbol.cpp
+++ b/src/util/rename_symbol.cpp
@@ -187,16 +187,6 @@ bool rename_symbolt::rename(typet &dest) const
       result = false;
     }
 
-    const exprt &spec_ensures_contract =
-      static_cast<const exprt &>(dest.find(ID_C_spec_ensures_contract));
-    if(
-      spec_ensures_contract.is_not_nil() &&
-      have_to_rename(spec_ensures_contract))
-    {
-      rename(static_cast<exprt &>(dest.add(ID_C_spec_ensures_contract)));
-      result = false;
-    }
-
     const exprt &spec_requires =
       static_cast<const exprt &>(dest.find(ID_C_spec_requires));
     if(spec_requires.is_not_nil() && have_to_rename(spec_requires))
@@ -204,16 +194,6 @@ bool rename_symbolt::rename(typet &dest) const
       rename(static_cast<exprt &>(dest.add(ID_C_spec_requires)));
       result = false;
     }
-
-    const exprt &spec_requires_contract =
-      static_cast<const exprt &>(dest.find(ID_C_spec_requires_contract));
-    if(
-      spec_requires_contract.is_not_nil() &&
-      have_to_rename(spec_requires_contract))
-    {
-      rename(static_cast<exprt &>(dest.add(ID_C_spec_requires_contract)));
-      result = false;
-    }
   }
   else if(dest.id()==ID_c_enum_tag ||
           dest.id()==ID_struct_tag ||
@@ -288,28 +268,10 @@ bool rename_symbolt::have_to_rename(const typet &dest) const
     if(spec_ensures.is_not_nil() && have_to_rename(spec_ensures))
       return true;
 
-    const exprt &spec_ensures_contract =
-      static_cast<const exprt &>(dest.find(ID_C_spec_ensures_contract));
-    if(
-      spec_ensures_contract.is_not_nil() &&
-      have_to_rename(spec_ensures_contract))
-    {
-      return true;
-    }
-
     const exprt &spec_requires =
       static_cast<const exprt &>(dest.find(ID_C_spec_requires));
     if(spec_requires.is_not_nil() && have_to_rename(spec_requires))
       return true;
-
-    const exprt &spec_requires_contract =
-      static_cast<const exprt &>(dest.find(ID_C_spec_requires_contract));
-    if(
-      spec_requires_contract.is_not_nil() &&
-      have_to_rename(spec_requires_contract))
-    {
-      return true;
-    }
   }
   else if(dest.id()==ID_c_enum_tag ||
           dest.id()==ID_struct_tag ||
diff --git a/src/util/replace_symbol.cpp b/src/util/replace_symbol.cpp
index dd53c6ad3e4..1a6be91b6c5 100644
--- a/src/util/replace_symbol.cpp
+++ b/src/util/replace_symbol.cpp
@@ -247,30 +247,10 @@ bool replace_symbolt::replace(typet &dest) const
     if(spec_ensures.is_not_nil() && have_to_replace(spec_ensures))
       result &= replace(static_cast<exprt &>(dest.add(ID_C_spec_ensures)));
 
-    const exprt &spec_ensures_contract =
-      static_cast<const exprt &>(dest.find(ID_C_spec_ensures_contract));
-    if(
-      spec_ensures_contract.is_not_nil() &&
-      have_to_replace(spec_ensures_contract))
-    {
-      result &=
-        replace(static_cast<exprt &>(dest.add(ID_C_spec_ensures_contract)));
-    }
-
     const exprt &spec_requires =
       static_cast<const exprt &>(dest.find(ID_C_spec_requires));
     if(spec_requires.is_not_nil() && have_to_replace(spec_requires))
       result &= replace(static_cast<exprt &>(dest.add(ID_C_spec_requires)));
-
-    const exprt &spec_requires_contract =
-      static_cast<const exprt &>(dest.find(ID_C_spec_requires_contract));
-    if(
-      spec_requires_contract.is_not_nil() &&
-      have_to_replace(spec_requires_contract))
-    {
-      result &=
-        replace(static_cast<exprt &>(dest.add(ID_C_spec_requires_contract)));
-    }
   }
   else if(dest.id()==ID_array)
   {
@@ -327,28 +307,10 @@ bool replace_symbolt::have_to_replace(const typet &dest) const
     if(spec_ensures.is_not_nil() && have_to_replace(spec_ensures))
       return true;
 
-    const exprt &spec_ensures_contract =
-      static_cast<const exprt &>(dest.find(ID_C_spec_ensures_contract));
-    if(
-      spec_ensures_contract.is_not_nil() &&
-      have_to_replace(spec_ensures_contract))
-    {
-      return true;
-    }
-
     const exprt &spec_requires =
       static_cast<const exprt &>(dest.find(ID_C_spec_requires));
     if(spec_requires.is_not_nil() && have_to_replace(spec_requires))
       return true;
-
-    const exprt &spec_requires_contract =
-      static_cast<const exprt &>(dest.find(ID_C_spec_requires_contract));
-    if(
-      spec_requires_contract.is_not_nil() &&
-      have_to_replace(spec_requires_contract))
-    {
-      return true;
-    }
   }
   else if(dest.id()==ID_array)
     return have_to_replace(to_array_type(dest).size());