diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp
index c32d9608332..fb16c66635f 100644
--- a/src/ansi-c/ansi_c_convert_type.cpp
+++ b/src/ansi-c/ansi_c_convert_type.cpp
@@ -250,7 +250,7 @@ void ansi_c_convert_typet::read_rec(const typet &type)
   {
     const exprt &as_expr =
       static_cast<const exprt &>(static_cast<const irept &>(type));
-    requires.push_back(to_unary_expr(as_expr).op());
+    c_requires.push_back(to_unary_expr(as_expr).op());
   }
   else if(type.id() == ID_C_spec_assigns)
   {
@@ -258,7 +258,7 @@ void ansi_c_convert_typet::read_rec(const typet &type)
       static_cast<const exprt &>(static_cast<const irept &>(type));
 
     for(const exprt &target : to_unary_expr(as_expr).op().operands())
-      assigns.push_back(target);
+      c_assigns.push_back(target);
   }
   else if(type.id() == ID_C_spec_frees)
   {
@@ -266,13 +266,13 @@ void ansi_c_convert_typet::read_rec(const typet &type)
       static_cast<const exprt &>(static_cast<const irept &>(type));
 
     for(const exprt &target : to_unary_expr(as_expr).op().operands())
-      frees.push_back(target);
+      c_frees.push_back(target);
   }
   else if(type.id() == ID_C_spec_ensures)
   {
     const exprt &as_expr =
       static_cast<const exprt &>(static_cast<const irept &>(type));
-    ensures.push_back(to_unary_expr(as_expr).op());
+    c_ensures.push_back(to_unary_expr(as_expr).op());
   }
   else
     other.push_back(type);
@@ -322,17 +322,17 @@ void ansi_c_convert_typet::write(typet &type)
     type.swap(other.front());
 
     // the contract expressions are meant for function types only
-    if(!requires.empty())
-      to_code_with_contract_type(type).requires() = std::move(requires);
+    if(!c_requires.empty())
+      to_code_with_contract_type(type).c_requires() = std::move(c_requires);
 
-    if(!assigns.empty())
-      to_code_with_contract_type(type).assigns() = std::move(assigns);
+    if(!c_assigns.empty())
+      to_code_with_contract_type(type).c_assigns() = std::move(c_assigns);
 
-    if(!frees.empty())
-      to_code_with_contract_type(type).frees() = std::move(frees);
+    if(!c_frees.empty())
+      to_code_with_contract_type(type).c_frees() = std::move(c_frees);
 
-    if(!ensures.empty())
-      to_code_with_contract_type(type).ensures() = std::move(ensures);
+    if(!c_ensures.empty())
+      to_code_with_contract_type(type).c_ensures() = std::move(c_ensures);
 
     if(constructor || destructor)
     {
diff --git a/src/ansi-c/ansi_c_convert_type.h b/src/ansi-c/ansi_c_convert_type.h
index a0e2ad650f9..67aa894efb3 100644
--- a/src/ansi-c/ansi_c_convert_type.h
+++ b/src/ansi-c/ansi_c_convert_type.h
@@ -48,7 +48,7 @@ class ansi_c_convert_typet
   bool constructor, destructor;
 
   // contracts
-  exprt::operandst assigns, frees, ensures, requires;
+  exprt::operandst c_assigns, c_frees, c_ensures, c_requires;
 
   // storage spec
   c_storage_spect c_storage_spec;
diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp
index 0b7bcb42b69..a442be43e47 100644
--- a/src/ansi-c/c_typecheck_base.cpp
+++ b/src/ansi-c/c_typecheck_base.cpp
@@ -905,20 +905,20 @@ void c_typecheck_baset::typecheck_declaration(
             parameter_identifier, p.type());
         }
 
-        for(auto &requires : code_type.requires())
+        for(auto &c_requires : code_type.c_requires())
         {
-          typecheck_expr(requires);
-          implicit_typecast_bool(requires);
+          typecheck_expr(c_requires);
+          implicit_typecast_bool(c_requires);
           std::string clause_type = "preconditions";
-          check_history_expr_return_value(requires, clause_type);
-          check_was_freed(requires, clause_type);
-          lambda_exprt lambda{temporary_parameter_symbols, requires};
-          lambda.add_source_location() = requires.source_location();
-          requires.swap(lambda);
+          check_history_expr_return_value(c_requires, clause_type);
+          check_was_freed(c_requires, clause_type);
+          lambda_exprt lambda{temporary_parameter_symbols, c_requires};
+          lambda.add_source_location() = c_requires.source_location();
+          c_requires.swap(lambda);
         }
 
-        typecheck_spec_assigns(code_type.assigns());
-        for(auto &assigns : code_type.assigns())
+        typecheck_spec_assigns(code_type.c_assigns());
+        for(auto &assigns : code_type.c_assigns())
         {
           std::string clause_type = "assigns clauses";
           check_history_expr_return_value(assigns, clause_type);
@@ -927,15 +927,15 @@ void c_typecheck_baset::typecheck_declaration(
           assigns.swap(lambda);
         }
 
-        typecheck_spec_frees(code_type.frees());
-        for(auto &frees : code_type.frees())
+        typecheck_spec_frees(code_type.c_frees());
+        for(auto &frees : code_type.c_frees())
         {
           lambda_exprt lambda{temporary_parameter_symbols, frees};
           lambda.add_source_location() = frees.source_location();
           frees.swap(lambda);
         }
 
-        for(auto &ensures : code_type.ensures())
+        for(auto &ensures : code_type.c_ensures())
         {
           typecheck_expr(ensures);
           implicit_typecast_bool(ensures);
diff --git a/src/cprover/instrument_contracts.cpp b/src/cprover/instrument_contracts.cpp
index 1c09c7b4d80..ff6e71a6834 100644
--- a/src/cprover/instrument_contracts.cpp
+++ b/src/cprover/instrument_contracts.cpp
@@ -286,11 +286,11 @@ void instrument_contract_checks(
   goto_programt add_at_beginning;
 
   // precondition?
-  if(!contract.requires().empty())
+  if(!contract.c_requires().empty())
   {
     // stick these in as assumptions, preserving the ordering
     goto_programt dest;
-    for(auto &assumption : contract.requires())
+    for(auto &assumption : contract.c_requires())
     {
       exprt assumption_instance = instantiate_contract_lambda(assumption);
       auto fixed_assumption = add_function(f.first, assumption_instance);
@@ -304,19 +304,19 @@ void instrument_contract_checks(
   const auto old_prefix = "old::" + id2string(f.first);
 
   // postcondition?
-  if(!contract.ensures().empty())
+  if(!contract.c_ensures().empty())
   {
     // Stick the postconditions in as assertions at the end
     auto last = body.instructions.end();
     if(std::prev(last)->is_end_function())
       last = std::prev(last);
 
-    for(auto &assertion : contract.ensures())
+    for(auto &assertion : contract.c_ensures())
     {
       exprt assertion_instance = instantiate_contract_lambda(assertion);
 
       std::string comment = "postcondition";
-      if(contract.ensures().size() >= 2)
+      if(contract.c_ensures().size() >= 2)
         comment += " " + expr2text(assertion_instance, ns);
 
       auto location = assertion.source_location();
@@ -338,8 +338,8 @@ void instrument_contract_checks(
 
   // do 'old' in the body
   if(
-    !contract.assigns().empty() || !contract.requires().empty() ||
-    !contract.ensures().empty())
+    !contract.c_assigns().empty() || !contract.c_requires().empty() ||
+    !contract.c_ensures().empty())
   {
     for(auto &instruction : body.instructions)
       instruction.transform(
@@ -359,8 +359,8 @@ void instrument_contract_checks(
 
   // assigns?
   if(
-    !contract.assigns().empty() || !contract.requires().empty() ||
-    !contract.ensures().empty())
+    !contract.c_assigns().empty() || !contract.c_requires().empty() ||
+    !contract.c_ensures().empty())
   {
     for(auto it = body.instructions.begin(); it != body.instructions.end();
         it++)
@@ -378,7 +378,7 @@ void instrument_contract_checks(
 
         // maybe not ok
         auto assigns_assertion =
-          make_assigns_assertion(f.first, contract.assigns(), lhs);
+          make_assigns_assertion(f.first, contract.c_assigns(), lhs);
         auto location = it->source_location();
         location.set_property_class("assigns");
         location.set_comment("assigns clause");
@@ -449,7 +449,7 @@ void replace_function_calls_by_contracts(
         goto_programt dest;
 
         // assert the preconditions
-        for(auto &precondition : contract.requires())
+        for(auto &precondition : contract.c_requires())
         {
           auto instantiated_precondition =
             instantiate_contract_lambda(precondition);
@@ -468,7 +468,7 @@ void replace_function_calls_by_contracts(
         }
 
         // havoc the 'assigned' variables
-        for(auto &assigns_clause_lambda : contract.assigns())
+        for(auto &assigns_clause_lambda : contract.c_assigns())
         {
           auto location = it->source_location();
 
@@ -519,7 +519,7 @@ void replace_function_calls_by_contracts(
         }
 
         // assume the postconditions
-        for(auto &postcondition : contract.ensures())
+        for(auto &postcondition : contract.c_ensures())
         {
           auto &location = it->source_location();
 
diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp
index e9ba3b202be..ef56f62ef4a 100644
--- a/src/goto-instrument/contracts/contracts.cpp
+++ b/src/goto-instrument/contracts/contracts.cpp
@@ -629,7 +629,9 @@ void code_contractst::apply_function_contract(
       // If the function does return a value, but the return value is
       // disregarded, check if the postcondition includes the return value.
       if(std::any_of(
-           type.ensures().begin(), type.ensures().end(), [](const exprt &e) {
+           type.c_ensures().begin(),
+           type.c_ensures().end(),
+           [](const exprt &e) {
              return has_symbol_expr(
                to_lambda_expr(e).where(), CPROVER_PREFIX "return_value", true);
            }))
@@ -674,7 +676,7 @@ void code_contractst::apply_function_contract(
   is_fresh.add_memory_map_decl(new_program);
 
   // Generate: assert(requires)
-  for(const auto &clause : type.requires())
+  for(const auto &clause : type.c_requires())
   {
     auto instantiated_clause =
       to_lambda_expr(clause).application(instantiation_values);
@@ -690,8 +692,8 @@ void code_contractst::apply_function_contract(
       converter,
       instantiated_clause,
       mode,
-      [&is_fresh](goto_programt &requires) {
-        is_fresh.update_requires(requires);
+      [&is_fresh](goto_programt &c_requires) {
+        is_fresh.update_requires(c_requires);
       },
       new_program,
       _location);
@@ -699,7 +701,7 @@ void code_contractst::apply_function_contract(
 
   // Generate all the instructions required to initialize history variables
   exprt::operandst instantiated_ensures_clauses;
-  for(auto clause : type.ensures())
+  for(auto clause : type.c_ensures())
   {
     auto instantiated_clause =
       to_lambda_expr(clause).application(instantiation_values);
@@ -712,7 +714,7 @@ void code_contractst::apply_function_contract(
   // ASSIGNS clause should not refer to any quantified variables,
   // and only refer to the common symbols to be replaced.
   exprt::operandst targets;
-  for(auto &target : type.assigns())
+  for(auto &target : type.c_assigns())
     targets.push_back(to_lambda_expr(target).application(instantiation_values));
 
   // Create a sequence of non-deterministic assignments ...
@@ -1138,7 +1140,7 @@ void code_contractst::check_frame_conditions_function(const irep_idt &function)
     instantiation_values.push_back(
       ns.lookup(param.get_identifier()).symbol_expr());
   }
-  for(auto &target : get_contract(function, ns).assigns())
+  for(auto &target : get_contract(function, ns).c_assigns())
   {
     goto_programt payload;
     instrument_spec_assigns.track_spec_target(
@@ -1299,7 +1301,7 @@ void code_contractst::add_contract_check(
   visitor.add_memory_map_decl(check);
 
   // Generate: assume(requires)
-  for(const auto &clause : code_type.requires())
+  for(const auto &clause : code_type.c_requires())
   {
     auto instantiated_clause =
       to_lambda_expr(clause).application(instantiation_values);
@@ -1318,8 +1320,8 @@ void code_contractst::add_contract_check(
       converter,
       instantiated_clause,
       function_symbol.mode,
-      [&visitor](goto_programt &requires) {
-        visitor.update_requires(requires);
+      [&visitor](goto_programt &c_requires) {
+        visitor.update_requires(c_requires);
       },
       check,
       _location);
@@ -1327,7 +1329,7 @@ void code_contractst::add_contract_check(
 
   // Generate all the instructions required to initialize history variables
   exprt::operandst instantiated_ensures_clauses;
-  for(auto clause : code_type.ensures())
+  for(auto clause : code_type.c_ensures())
   {
     auto instantiated_clause =
       to_lambda_expr(clause).application(instantiation_values);
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.cpp
index 957c50fcae4..9e2c545dfd9 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.cpp
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.cpp
@@ -150,7 +150,7 @@ void dfcc_contract_functionst::gen_spec_assigns_function()
 
   exprt::operandst targets;
 
-  for(const exprt &target : code_with_contract.assigns())
+  for(const exprt &target : code_with_contract.c_assigns())
   {
     auto new_target = to_lambda_expr(target).application(lambda_parameters);
     new_target.add_source_location() = target.source_location();
@@ -201,7 +201,7 @@ void dfcc_contract_functionst::gen_spec_frees_function()
 
   exprt::operandst targets;
 
-  for(const exprt &target : code_with_contract.frees())
+  for(const exprt &target : code_with_contract.c_frees())
   {
     auto new_target = to_lambda_expr(target).application(lambda_parameters);
     new_target.add_source_location() = target.source_location();
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 7511f6fcd21..d0a811c6b56 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.h
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.h
@@ -42,7 +42,7 @@ class conditional_target_group_exprt;
 /// ```c
 /// // Populates write_set_to_fill with targets of the assigns clause
 /// // checks its own body against write_set_to_check:
-/// void contract_id::assigns(
+/// void contract_id::c_assigns(
 ///     function-params,
 ///     write_set_to_fill,
 ///     write_set_to_check);
@@ -50,8 +50,8 @@ class conditional_target_group_exprt;
 ///
 /// ```c
 /// // Havocs the targets specified in the assigns clause, assuming
-/// // write_set_to_havoc is a snapshot created using contract_id::assigns
-/// void contract_id::assigns::havoc(write_set_to_havoc);
+/// // write_set_to_havoc is a snapshot created using contract_id::c_assigns
+/// void contract_id::c_assigns::havoc(write_set_to_havoc);
 /// ```
 ///
 /// ```c
@@ -89,10 +89,10 @@ class dfcc_contract_functionst
   void instrument_without_loop_contracts_check_no_pointer_contracts(
     const irep_idt &spec_function_id);
 
-  /// Returns the contract::assigns function symbol
+  /// Returns the contract::c_assigns function symbol
   const symbolt &get_spec_assigns_function_symbol() const;
 
-  /// Returns the contract::assigns::havoc function symbol
+  /// Returns the contract::c_assigns::havoc function symbol
   const symbolt &get_spec_assigns_havoc_function_symbol() const;
 
   /// Returns the contract::frees function symbol
@@ -110,10 +110,10 @@ class dfcc_contract_functionst
   /// The code_with_contract_type carrying the contract clauses
   const code_with_contract_typet &code_with_contract;
 
-  /// Identifier of the contract::assigns function
+  /// Identifier of the contract::c_assigns function
   const irep_idt spec_assigns_function_id;
 
-  /// Identifier of the contract::assigns::havoc function
+  /// Identifier of the contract::c_assigns::havoc function
   const irep_idt spec_assigns_havoc_function_id;
 
   /// Identifier of the contract::frees function
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 3155088a398..ab39b874757 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp
@@ -577,7 +577,7 @@ void dfcc_wrapper_programt::encode_requires_clauses()
   goto_programt requires_program;
 
   // translate each requires clause
-  for(const auto &r : contract_code_type.requires())
+  for(const auto &r : contract_code_type.c_requires())
   {
     exprt requires = to_lambda_expr(r).application(contract_lambda_parameters);
     requires.add_source_location() = r.source_location();
@@ -621,7 +621,7 @@ void dfcc_wrapper_programt::encode_ensures_clauses()
   goto_programt ensures_program;
 
   // translate each ensures clause
-  for(const auto &e : contract_code_type.ensures())
+  for(const auto &e : contract_code_type.c_ensures())
   {
     exprt ensures = to_lambda_expr(e)
                       .application(contract_lambda_parameters)
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 004366dee66..6bfb51432fb 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h
@@ -224,7 +224,7 @@ class dfcc_wrapper_programt
   /// (populated by calling functions provided in contract_functions)
   /// - Adds declaration of write set and pointer to write set to \ref preamble
   /// - Adds initialisation function call in \ref write_set_checks
-  /// - Adds contract::assigns and contract::frees function call
+  /// - Adds contract::c_assigns and contract::frees function call
   /// in \ref write_set_checks
   /// - Adds release function call in \ref postamble
   void encode_contract_write_set();
diff --git a/src/linking/remove_internal_symbols.cpp b/src/linking/remove_internal_symbols.cpp
index 5c36f61ab50..23b24c9aee7 100644
--- a/src/linking/remove_internal_symbols.cpp
+++ b/src/linking/remove_internal_symbols.cpp
@@ -67,11 +67,11 @@ static void get_symbols(
         to_code_with_contract_type(code_type);
 
       find_symbols_sett new_symbols;
-      for(const exprt &a : maybe_contract.assigns())
+      for(const exprt &a : maybe_contract.c_assigns())
         find_type_and_expr_symbols(a, new_symbols);
-      for(const exprt &e : maybe_contract.ensures())
+      for(const exprt &e : maybe_contract.c_ensures())
         find_type_and_expr_symbols(e, new_symbols);
-      for(const exprt &r : maybe_contract.requires())
+      for(const exprt &r : maybe_contract.c_requires())
         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 cc261e74e79..9cf96cf1103 100644
--- a/src/util/c_types.h
+++ b/src/util/c_types.h
@@ -390,46 +390,46 @@ class code_with_contract_typet : public code_typet
 
   bool has_contract() const
   {
-    return !ensures().empty() || !requires().empty() || !assigns().empty() ||
-           !frees().empty();
+    return !c_ensures().empty() || !c_requires().empty() ||
+           !c_assigns().empty() || !c_frees().empty();
   }
 
-  const exprt::operandst &assigns() const
+  const exprt::operandst &c_assigns() const
   {
     return static_cast<const exprt &>(find(ID_C_spec_assigns)).operands();
   }
 
-  exprt::operandst &assigns()
+  exprt::operandst &c_assigns()
   {
     return static_cast<exprt &>(add(ID_C_spec_assigns)).operands();
   }
 
-  const exprt::operandst &frees() const
+  const exprt::operandst &c_frees() const
   {
     return static_cast<const exprt &>(find(ID_C_spec_frees)).operands();
   }
 
-  exprt::operandst &frees()
+  exprt::operandst &c_frees()
   {
     return static_cast<exprt &>(add(ID_C_spec_frees)).operands();
   }
 
-  const exprt::operandst &requires() const
+  const exprt::operandst &c_requires() const
   {
     return static_cast<const exprt &>(find(ID_C_spec_requires)).operands();
   }
 
-  exprt::operandst &requires()
+  exprt::operandst &c_requires()
   {
     return static_cast<exprt &>(add(ID_C_spec_requires)).operands();
   }
 
-  const exprt::operandst &ensures() const
+  const exprt::operandst &c_ensures() const
   {
     return static_cast<const exprt &>(find(ID_C_spec_ensures)).operands();
   }
 
-  exprt::operandst &ensures()
+  exprt::operandst &c_ensures()
   {
     return static_cast<exprt &>(add(ID_C_spec_ensures)).operands();
   }