diff --git a/src/analyses/local_may_alias.cpp b/src/analyses/local_may_alias.cpp
index 200916d58e9..b536c885a90 100644
--- a/src/analyses/local_may_alias.cpp
+++ b/src/analyses/local_may_alias.cpp
@@ -217,7 +217,7 @@ void local_may_aliast::get_rec(
       if(index_expr.array().id()==ID_symbol)
       {
         index_exprt tmp1=index_expr;
-        tmp1.index()=from_integer(0, index_type());
+        tmp1.index() = from_integer(0, c_index_type());
         address_of_exprt tmp2(tmp1);
         unsigned object_nr=objects.number(tmp2);
         dest.insert(object_nr);
@@ -229,7 +229,7 @@ void local_may_aliast::get_rec(
       else if(index_expr.array().id()==ID_string_constant)
       {
         index_exprt tmp1=index_expr;
-        tmp1.index()=from_integer(0, index_type());
+        tmp1.index() = from_integer(0, c_index_type());
         address_of_exprt tmp2(tmp1);
         unsigned object_nr=objects.number(tmp2);
         dest.insert(object_nr);
diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp
index 0f7b7e360c7..41f134b6f1b 100644
--- a/src/ansi-c/ansi_c_entry_point.cpp
+++ b/src/ansi-c/ansi_c_entry_point.cpp
@@ -448,7 +448,7 @@ bool generate_ansi_c_start_function(
 
         {
           index_exprt index_expr(
-            argv_symbol.symbol_expr(), from_integer(0, index_type()));
+            argv_symbol.symbol_expr(), from_integer(0, c_index_type()));
 
           // disable bounds check on that one
           index_expr.set(ID_C_bounds_check, false);
@@ -466,7 +466,7 @@ bool generate_ansi_c_start_function(
           const symbolt &envp_symbol=ns.lookup("envp'");
 
           index_exprt index_expr(
-            envp_symbol.symbol_expr(), from_integer(0, index_type()));
+            envp_symbol.symbol_expr(), from_integer(0, c_index_type()));
 
           const pointer_typet &pointer_type =
             to_pointer_type(parameters[2].type());
diff --git a/src/ansi-c/c_typecast.cpp b/src/ansi-c/c_typecast.cpp
index 54e5d0c8a28..abe6ac6a9d8 100644
--- a/src/ansi-c/c_typecast.cpp
+++ b/src/ansi-c/c_typecast.cpp
@@ -722,7 +722,7 @@ void c_typecastt::do_typecast(exprt &expr, const typet &dest_type)
 
   if(src_type.id()==ID_array)
   {
-    index_exprt index(expr, from_integer(0, index_type()));
+    index_exprt index(expr, from_integer(0, c_index_type()));
     expr = typecast_exprt::conditional_cast(address_of_exprt(index), dest_type);
     return;
   }
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index 455b83ccc49..5fd118b43be 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -1185,7 +1185,7 @@ void c_typecheck_baset::typecheck_expr_typecast(exprt &expr)
   }
   else if(op_type.id()==ID_array)
   {
-    index_exprt index(op, from_integer(0, index_type()));
+    index_exprt index(op, from_integer(0, c_index_type()));
     op=address_of_exprt(index);
   }
   else if(op_type.id()==ID_empty)
@@ -1245,7 +1245,7 @@ void c_typecheck_baset::typecheck_expr_typecast(exprt &expr)
 
 void c_typecheck_baset::make_index_type(exprt &expr)
 {
-  implicit_typecast(expr, index_type());
+  implicit_typecast(expr, c_index_type());
 }
 
 void c_typecheck_baset::typecheck_expr_index(exprt &expr)
@@ -1456,7 +1456,7 @@ void c_typecheck_baset::typecheck_expr_ptrmember(exprt &expr)
   if(op0_type.id() == ID_array)
   {
     // a->f is the same as a[0].f
-    exprt zero=from_integer(0, index_type());
+    exprt zero = from_integer(0, c_index_type());
     index_exprt index_expr(op, zero, op0_type.subtype());
     index_expr.set(ID_C_lvalue, true);
     op.swap(index_expr);
@@ -1774,7 +1774,7 @@ void c_typecheck_baset::typecheck_expr_dereference(exprt &expr)
     // *a is the same as a[0]
     expr.id(ID_index);
     expr.type()=op_type.subtype();
-    expr.copy_to_operands(from_integer(0, index_type()));
+    expr.copy_to_operands(from_integer(0, c_index_type()));
     assert(expr.operands().size()==2);
   }
   else if(op_type.id()==ID_pointer)
diff --git a/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp b/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp
index 5fc5413601d..e81d7c8927d 100644
--- a/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp
+++ b/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp
@@ -1445,7 +1445,7 @@ exprt c_typecheck_baset::typecheck_shuffle_vector(
     for(std::size_t i = 0; i < indices_size; ++i)
     {
       // only the least significant bits of each mask element are considered
-      mod_exprt mod_index{index_exprt{indices, from_integer(i, index_type())},
+      mod_exprt mod_index{index_exprt{indices, from_integer(i, c_index_type())},
                           size};
       mod_index.add_source_location() = source_location;
       operands.push_back(std::move(mod_index));
diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp
index 604ea0b61b0..8bf35e658cb 100644
--- a/src/ansi-c/c_typecheck_initializer.cpp
+++ b/src/ansi-c/c_typecheck_initializer.cpp
@@ -542,7 +542,7 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
         if(current_symbol.is_static_lifetime)
         {
           byte_update_exprt byte_update =
-            make_byte_update(*dest, from_integer(0, index_type()), *zero);
+            make_byte_update(*dest, from_integer(0, c_index_type()), *zero);
           byte_update.add_source_location() = value.source_location();
           *dest = std::move(byte_update);
           dest = &(to_byte_update_expr(*dest).op2());
@@ -1029,7 +1029,7 @@ exprt c_typecheck_baset::do_initializer_list(
     // make complete by setting array size
     size_t size=result.operands().size();
     result.type().id(ID_array);
-    result.type().set(ID_size, from_integer(size, index_type()));
+    result.type().set(ID_size, from_integer(size, c_index_type()));
   }
 
   return result;
diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp
index 2b542854552..2c61f525b0d 100644
--- a/src/ansi-c/c_typecheck_type.cpp
+++ b/src/ansi-c/c_typecheck_type.cpp
@@ -1011,7 +1011,7 @@ void c_typecheck_baset::typecheck_compound_body(
 
         // make it zero-length
         c_type.id(ID_array);
-        c_type.set(ID_size, from_integer(0, index_type()));
+        c_type.set(ID_size, from_integer(0, c_index_type()));
       }
     }
   }
diff --git a/src/ansi-c/literals/convert_string_literal.cpp b/src/ansi-c/literals/convert_string_literal.cpp
index b36a7aeb3c1..6961326141c 100644
--- a/src/ansi-c/literals/convert_string_literal.cpp
+++ b/src/ansi-c/literals/convert_string_literal.cpp
@@ -127,7 +127,7 @@ exprt convert_string_literal(const std::string &src)
     result.set(ID_C_string_constant, true);
     result.type()=typet(ID_array);
     result.type().subtype()=subtype;
-    result.type().set(ID_size, from_integer(value.size(), index_type()));
+    result.type().set(ID_size, from_integer(value.size(), c_index_type()));
 
     result.operands().resize(value.size());
     for(std::size_t i=0; i<value.size(); i++)
diff --git a/src/cpp/cpp_constructor.cpp b/src/cpp/cpp_constructor.cpp
index d8b86944412..4262663b173 100644
--- a/src/cpp/cpp_constructor.cpp
+++ b/src/cpp/cpp_constructor.cpp
@@ -97,7 +97,7 @@ optionalt<codet> cpp_typecheckt::cpp_constructor(
       {
         exprt::operandst tmp_operands;
 
-        exprt constant=from_integer(i, index_type());
+        exprt constant = from_integer(i, c_index_type());
         constant.add_source_location()=source_location;
 
         index_exprt index(object, constant);
diff --git a/src/cpp/cpp_destructor.cpp b/src/cpp/cpp_destructor.cpp
index f1b985bc1f0..2282b5d4186 100644
--- a/src/cpp/cpp_destructor.cpp
+++ b/src/cpp/cpp_destructor.cpp
@@ -56,7 +56,7 @@ optionalt<codet> cpp_typecheckt::cpp_destructor(
     // for each element of the array, call the destructor
     for(mp_integer i=0; i < s; ++i)
     {
-      exprt constant=from_integer(i, index_type());
+      exprt constant = from_integer(i, c_index_type());
       constant.add_source_location()=source_location;
 
       index_exprt index(object, constant);
diff --git a/src/cpp/cpp_typecheck_constructor.cpp b/src/cpp/cpp_typecheck_constructor.cpp
index ba4f573c3a1..81fbd79b8ba 100644
--- a/src/cpp/cpp_typecheck_constructor.cpp
+++ b/src/cpp/cpp_typecheck_constructor.cpp
@@ -90,7 +90,7 @@ static void copy_array(
   exprt &block)
 {
   // Build the index expression
-  const exprt constant = from_integer(i, index_type());
+  const exprt constant = from_integer(i, c_index_type());
 
   const cpp_namet array(member_base_name, source_location);
 
diff --git a/src/cpp/cpp_typecheck_conversions.cpp b/src/cpp/cpp_typecheck_conversions.cpp
index d4b0db4fcd3..31b4b4a24cb 100644
--- a/src/cpp/cpp_typecheck_conversions.cpp
+++ b/src/cpp/cpp_typecheck_conversions.cpp
@@ -80,9 +80,7 @@ bool cpp_typecheckt::standard_conversion_array_to_pointer(
 {
   assert(expr.type().id()==ID_array);
 
-  index_exprt index(
-    expr,
-    from_integer(0, index_type()));
+  index_exprt index(expr, from_integer(0, c_index_type()));
 
   index.set(ID_C_lvalue, true);
 
diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp
index f1ef59af7ef..10d112a0508 100644
--- a/src/cpp/cpp_typecheck_expr.cpp
+++ b/src/cpp/cpp_typecheck_expr.cpp
@@ -256,9 +256,9 @@ void cpp_typecheckt::typecheck_expr_trinary(if_exprt &expr)
     {
       // array-to-pointer conversion
 
-      index_exprt index1(expr.op1(), from_integer(0, index_type()));
+      index_exprt index1(expr.op1(), from_integer(0, c_index_type()));
 
-      index_exprt index2(expr.op2(), from_integer(0, index_type()));
+      index_exprt index2(expr.op2(), from_integer(0, c_index_type()));
 
       address_of_exprt addr1(index1);
       address_of_exprt addr2(index2);
diff --git a/src/cpp/cpp_typecheck_initializer.cpp b/src/cpp/cpp_typecheck_initializer.cpp
index 61747c2763b..11b28bdbee1 100644
--- a/src/cpp/cpp_typecheck_initializer.cpp
+++ b/src/cpp/cpp_typecheck_initializer.cpp
@@ -244,7 +244,7 @@ void cpp_typecheckt::zero_initializer(
     for(mp_integer i=0; i<size; ++i)
     {
       index_exprt index(
-        object, from_integer(i, index_type()), array_type.subtype());
+        object, from_integer(i, c_index_type()), array_type.subtype());
       zero_initializer(index, array_type.subtype(), source_location, ops);
     }
   }
diff --git a/src/goto-instrument/function.cpp b/src/goto-instrument/function.cpp
index a1d8c853cfd..ba467dc96ff 100644
--- a/src/goto-instrument/function.cpp
+++ b/src/goto-instrument/function.cpp
@@ -67,7 +67,7 @@ code_function_callt function_to_call(
     symbol_exprt(s_it->second.name, s_it->second.type),
     {typecast_exprt(
       address_of_exprt(
-        index_exprt(function_id_string, from_integer(0, index_type()))),
+        index_exprt(function_id_string, from_integer(0, c_index_type()))),
       to_code_type(s_it->second.type).parameters()[0].type())});
 
   return call;
diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
index 699b1dc14eb..9c23afff440 100644
--- a/src/goto-programs/builtin_functions.cpp
+++ b/src/goto-programs/builtin_functions.cpp
@@ -260,7 +260,7 @@ void goto_convertt::do_scanf(
               const address_of_exprt rhs(
                 index_exprt(
                   tmp_symbol.symbol_expr(),
-                  from_integer(0, index_type())));
+                  from_integer(0, c_index_type())));
 
               // now use array copy
               codet array_copy_statement;
@@ -274,7 +274,7 @@ void goto_convertt::do_scanf(
               copy(array_copy_statement, OTHER, dest);
               #else
               const index_exprt new_lhs(
-                dereference_exprt{ptr}, from_integer(0, index_type()));
+                dereference_exprt{ptr}, from_integer(0, c_index_type()));
               const side_effect_expr_nondett rhs(
                 type->subtype(), function.source_location());
               code_assignt assign(new_lhs, rhs);
@@ -605,7 +605,7 @@ exprt make_va_list(const exprt &expr)
   while(result.type().id() == ID_array &&
         to_array_type(result.type()).size().is_one())
   {
-    result = index_exprt{result, from_integer(0, index_type())};
+    result = index_exprt{result, from_integer(0, c_index_type())};
   }
 
   return result;
@@ -704,8 +704,8 @@ void goto_convertt::do_havoc_slice(
 
   const symbolt &nondet_contents =
     new_tmp_symbol(array_type, "nondet_contents", dest, source_location, mode);
-  const exprt &nondet_contents_expr = address_of_exprt{
-    index_exprt{nondet_contents.symbol_expr(), from_integer(0, index_type())}};
+  const exprt &nondet_contents_expr = address_of_exprt{index_exprt{
+    nondet_contents.symbol_expr(), from_integer(0, c_index_type())}};
 
   const exprt &arg0 =
     typecast_exprt::conditional_cast(arguments[0], pointer_type(empty_typet{}));
diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp
index 8ed67d19b53..2fbc5d0d389 100644
--- a/src/goto-programs/goto_convert_side_effect.cpp
+++ b/src/goto-programs/goto_convert_side_effect.cpp
@@ -214,7 +214,7 @@ void goto_convertt::remove_pre(
   typet constant_type;
 
   if(op_type.id() == ID_pointer)
-    constant_type = index_type();
+    constant_type = c_index_type();
   else if(is_number(op_type))
     constant_type = op_type;
   else
@@ -300,7 +300,7 @@ void goto_convertt::remove_post(
   typet constant_type;
 
   if(op_type.id() == ID_pointer)
-    constant_type = index_type();
+    constant_type = c_index_type();
   else if(is_number(op_type))
     constant_type = op_type;
   else
diff --git a/src/goto-programs/goto_instruction_code.cpp b/src/goto-programs/goto_instruction_code.cpp
index bbd04cf5d33..4265d52e8dd 100644
--- a/src/goto-programs/goto_instruction_code.cpp
+++ b/src/goto-programs/goto_instruction_code.cpp
@@ -34,7 +34,7 @@ code_inputt::code_inputt(
   optionalt<source_locationt> location)
   : code_inputt{{address_of_exprt(index_exprt(
                    string_constantt(description),
-                   from_integer(0, index_type()))),
+                   from_integer(0, c_index_type()))),
                  std::move(expression)},
                 std::move(location)}
 {
@@ -62,7 +62,7 @@ code_outputt::code_outputt(
   optionalt<source_locationt> location)
   : code_outputt{{address_of_exprt(index_exprt(
                     string_constantt(description),
-                    from_integer(0, index_type()))),
+                    from_integer(0, c_index_type()))),
                   std::move(expression)},
                  std::move(location)}
 {
diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp
index d1da6257125..8eca747682a 100644
--- a/src/goto-programs/graphml_witness.cpp
+++ b/src/goto-programs/graphml_witness.cpp
@@ -109,9 +109,7 @@ std::string graphml_witnesst::convert_assign_rec(
     forall_operands(it, assign.rhs())
     {
       index_exprt index(
-        assign.lhs(),
-        from_integer(i++, index_type()),
-        type.subtype());
+        assign.lhs(), from_integer(i++, c_index_type()), type.subtype());
       if(!result.empty())
         result+=' ';
       result+=convert_assign_rec(identifier, code_assignt(index, *it));
diff --git a/src/goto-programs/rewrite_union.cpp b/src/goto-programs/rewrite_union.cpp
index 616f1a4c6a7..714c9568a0f 100644
--- a/src/goto-programs/rewrite_union.cpp
+++ b/src/goto-programs/rewrite_union.cpp
@@ -82,14 +82,14 @@ void rewrite_union(exprt &expr)
 
     if(op.type().id() == ID_union_tag || op.type().id() == ID_union)
     {
-      exprt offset=from_integer(0, index_type());
+      exprt offset = from_integer(0, c_index_type());
       expr = make_byte_extract(op, offset, expr.type());
     }
   }
   else if(expr.id()==ID_union)
   {
     const union_exprt &union_expr=to_union_expr(expr);
-    exprt offset=from_integer(0, index_type());
+    exprt offset = from_integer(0, c_index_type());
     side_effect_expr_nondett nondet(expr.type(), expr.source_location());
     expr = make_byte_update(nondet, offset, union_expr.op());
   }
diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp
index 27ca19d5ceb..07790127f2a 100644
--- a/src/goto-programs/string_abstraction.cpp
+++ b/src/goto-programs/string_abstraction.cpp
@@ -573,7 +573,7 @@ void string_abstractiont::abstract_function_call(
         str_args.back().type().subtype() == abstract_type.subtype(),
         "argument array type differs from formal parameter pointer type");
 
-      index_exprt idx(str_args.back(), from_integer(0, index_type()));
+      index_exprt idx(str_args.back(), from_integer(0, c_index_type()));
       // disable bounds check on that one
       idx.set(ID_C_bounds_check, false);
 
diff --git a/src/goto-programs/string_instrumentation.cpp b/src/goto-programs/string_instrumentation.cpp
index 8d4c2e87315..5a7718dc5b6 100644
--- a/src/goto-programs/string_instrumentation.cpp
+++ b/src/goto-programs/string_instrumentation.cpp
@@ -394,7 +394,7 @@ void string_instrumentationt::do_format_string_read(
 
           if(arg.type().id() != ID_pointer)
           {
-            index_exprt index(temp, from_integer(0, index_type()));
+            index_exprt index(temp, from_integer(0, c_index_type()));
             temp=address_of_exprt(index);
           }
 
@@ -437,7 +437,7 @@ void string_instrumentationt::do_format_string_read(
 
         if(arg.type().id() != ID_pointer)
         {
-          index_exprt index(temp, from_integer(0, index_type()));
+          index_exprt index(temp, from_integer(0, c_index_type()));
           temp=address_of_exprt(index);
         }
 
@@ -778,9 +778,7 @@ void string_instrumentationt::do_strerror(
 
   // return a pointer to some magic buffer
   index_exprt index(
-    symbol_buf.symbol_expr(),
-    from_integer(0, index_type()),
-    char_type());
+    symbol_buf.symbol_expr(), from_integer(0, c_index_type()), char_type());
 
   address_of_exprt ptr(index);
 
@@ -843,7 +841,7 @@ void string_instrumentationt::invalidate_buffer(
   else
   {
     index_exprt index(
-      buffer, from_integer(0, index_type()), buf_type.subtype());
+      buffer, from_integer(0, c_index_type()), buf_type.subtype());
     bufp=address_of_exprt(index);
   }
 
diff --git a/src/goto-symex/goto_symex.cpp b/src/goto-symex/goto_symex.cpp
index 979398c9193..ad49c2033ee 100644
--- a/src/goto-symex/goto_symex.cpp
+++ b/src/goto-symex/goto_symex.cpp
@@ -267,7 +267,7 @@ void goto_symext::assign_string_constant(
     "symbol shall have value derived from char array content");
 
   const address_of_exprt string_data(
-    index_exprt(aux_symbol.symbol_expr(), from_integer(0, index_type())));
+    index_exprt(aux_symbol.symbol_expr(), from_integer(0, c_index_type())));
 
   symex_assign.assign_symbol(char_array, expr_skeletont{}, string_data, {});
 
diff --git a/src/goto-symex/symex_clean_expr.cpp b/src/goto-symex/symex_clean_expr.cpp
index 11ba754185e..a991cb372a3 100644
--- a/src/goto-symex/symex_clean_expr.cpp
+++ b/src/goto-symex/symex_clean_expr.cpp
@@ -45,7 +45,7 @@ process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
     {
       byte_extract_exprt be = make_byte_extract(
         if_expr.false_case(),
-        from_integer(0, index_type()),
+        from_integer(0, c_index_type()),
         if_expr.true_case().type());
 
       if_expr.false_case().swap(be);
@@ -93,7 +93,7 @@ process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
           simplify(array_size.value(), ns);
         expr = make_byte_extract(
           expr,
-          from_integer(0, index_type()),
+          from_integer(0, c_index_type()),
           array_typet(char_type(), array_size.value()));
       }
 
diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp
index f98944d178a..9bff72fa76a 100644
--- a/src/goto-symex/symex_dereference.cpp
+++ b/src/goto-symex/symex_dereference.cpp
@@ -66,7 +66,7 @@ exprt goto_symext::address_arithmetic(
       for(const typet *t = &(a.type().subtype());
           t->id() == ID_array && expr.type() != *t;
           t = &(t->subtype()))
-        a.object()=index_exprt(a.object(), from_integer(0, index_type()));
+        a.object() = index_exprt(a.object(), from_integer(0, c_index_type()));
     }
 
     // do (expr.type() *)(((char *)op)+offset)
@@ -138,7 +138,7 @@ exprt goto_symext::address_arithmetic(
 
     // turn &array into &array[0]
     if(result.type().id() == ID_array && !keep_array)
-      result=index_exprt(result, from_integer(0, index_type()));
+      result = index_exprt(result, from_integer(0, c_index_type()));
 
     // handle field-sensitive SSA symbol
     mp_integer offset=0;
@@ -153,7 +153,7 @@ exprt goto_symext::address_arithmetic(
     {
       const byte_extract_exprt be = make_byte_extract(
         to_ssa_expr(expr).get_l1_object(),
-        from_integer(offset, index_type()),
+        from_integer(offset, c_index_type()),
         expr.type());
 
       result = address_arithmetic(be, state, keep_array);
@@ -404,11 +404,8 @@ void goto_symext::dereference_rec(
       expr.type() ==
         pointer_type(to_address_of_expr(tc_op).object().type().subtype()))
     {
-      expr=
-        address_of_exprt(
-          index_exprt(
-            to_address_of_expr(tc_op).object(),
-            from_integer(0, index_type())));
+      expr = address_of_exprt(index_exprt(
+        to_address_of_expr(tc_op).object(), from_integer(0, c_index_type())));
 
       dereference_rec(expr, state, write, is_in_quantifier);
     }
diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp
index 53f601e0b16..8ba98f69228 100644
--- a/src/goto-symex/symex_function_call.cpp
+++ b/src/goto-symex/symex_function_call.cpp
@@ -111,7 +111,7 @@ void goto_symext::parameter_assignments(
         // clang-format on
         {
           rhs = make_byte_extract(
-            rhs, from_integer(0, index_type()), parameter_type);
+            rhs, from_integer(0, c_index_type()), parameter_type);
         }
         else
         {
diff --git a/src/goto-symex/symex_other.cpp b/src/goto-symex/symex_other.cpp
index 43ba86510d0..3c3393ff2cd 100644
--- a/src/goto-symex/symex_other.cpp
+++ b/src/goto-symex/symex_other.cpp
@@ -146,14 +146,14 @@ void goto_symext::symex_other(
       if(statement==ID_array_copy)
       {
         src_array = make_byte_extract(
-          src_array, from_integer(0, index_type()), dest_array.type());
+          src_array, from_integer(0, c_index_type()), dest_array.type());
         do_simplify(src_array);
       }
       else
       {
         // ID_array_replace
         dest_array = make_byte_extract(
-          dest_array, from_integer(0, index_type()), src_array.type());
+          dest_array, from_integer(0, c_index_type()), src_array.type());
         do_simplify(dest_array);
       }
     }
@@ -191,7 +191,7 @@ void goto_symext::symex_other(
       do_simplify(array_size.value());
       array_expr = make_byte_extract(
         array_expr,
-        from_integer(0, index_type()),
+        from_integer(0, c_index_type()),
         array_typet(char_type(), array_size.value()));
     }
 
diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
index 0c083ee0627..1f13e71408b 100644
--- a/src/pointer-analysis/value_set.cpp
+++ b/src/pointer-analysis/value_set.cpp
@@ -227,7 +227,7 @@ exprt value_sett::to_expr(const object_map_dt::value_type &it) const
   od.object()=object;
 
   if(it.second)
-    od.offset() = from_integer(*it.second, index_type());
+    od.offset() = from_integer(*it.second, c_index_type());
 
   od.type()=od.object().type();
 
@@ -1117,7 +1117,7 @@ void value_sett::get_reference_set_rec(
       {
         const index_exprt deref_index_expr(
           typecast_exprt::conditional_cast(object, array_type),
-          from_integer(0, index_type()));
+          from_integer(0, c_index_type()));
 
         offsett o = a_it->second;
         const auto i = numeric_cast<mp_integer>(offset);
@@ -1265,7 +1265,7 @@ void value_sett::assign(
   else if(type.id()==ID_array)
   {
     const index_exprt lhs_index(
-      lhs, exprt(ID_unknown, index_type()), type.subtype());
+      lhs, exprt(ID_unknown, c_index_type()), type.subtype());
 
     if(rhs.id()==ID_unknown ||
        rhs.id()==ID_invalid)
@@ -1307,7 +1307,7 @@ void value_sett::assign(
       {
         const index_exprt op0_index(
           to_with_expr(rhs).old(),
-          exprt(ID_unknown, index_type()),
+          exprt(ID_unknown, c_index_type()),
           type.subtype());
 
         assign(lhs_index, op0_index, ns, is_simplified, add_to_sets);
@@ -1317,7 +1317,7 @@ void value_sett::assign(
       else
       {
         const index_exprt rhs_index(
-          rhs, exprt(ID_unknown, index_type()), type.subtype());
+          rhs, exprt(ID_unknown, c_index_type()), type.subtype());
         assign(lhs_index, rhs_index, ns, is_simplified, true);
       }
     }
diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp
index 66aab34b2a6..dd93280c2fa 100644
--- a/src/pointer-analysis/value_set_fi.cpp
+++ b/src/pointer-analysis/value_set_fi.cpp
@@ -229,7 +229,7 @@ exprt value_set_fit::to_expr(const object_map_dt::value_type &it) const
   od.object()=object;
 
   if(it.second)
-    od.offset() = from_integer(*it.second, index_type());
+    od.offset() = from_integer(*it.second, c_index_type());
 
   od.type()=od.object().type();
 
@@ -868,7 +868,7 @@ void value_set_fit::get_reference_set_sharing_rec(
       else
       {
         index_exprt index_expr(
-          object, from_integer(0, index_type()), expr.type());
+          object, from_integer(0, c_index_type()), expr.type());
 
         exprt casted_index;
 
@@ -1045,7 +1045,7 @@ void value_set_fit::assign(
   else if(type.id()==ID_array)
   {
     const index_exprt lhs_index(
-      lhs, exprt(ID_unknown, index_type()), type.subtype());
+      lhs, exprt(ID_unknown, c_index_type()), type.subtype());
 
     if(rhs.id()==ID_unknown ||
        rhs.id()==ID_invalid)
@@ -1079,7 +1079,7 @@ void value_set_fit::assign(
       {
         const index_exprt op0_index(
           to_with_expr(rhs).old(),
-          exprt(ID_unknown, index_type()),
+          exprt(ID_unknown, c_index_type()),
           type.subtype());
 
         assign(lhs_index, op0_index, ns);
@@ -1088,7 +1088,7 @@ void value_set_fit::assign(
       else
       {
         const index_exprt rhs_index(
-          rhs, exprt(ID_unknown, index_type()), type.subtype());
+          rhs, exprt(ID_unknown, c_index_type()), type.subtype());
         assign(lhs_index, rhs_index, ns);
       }
     }
diff --git a/src/solvers/lowering/byte_operators.cpp b/src/solvers/lowering/byte_operators.cpp
index 08af481e9a6..b8d7ea0b542 100644
--- a/src/solvers/lowering/byte_operators.cpp
+++ b/src/solvers/lowering/byte_operators.cpp
@@ -413,7 +413,7 @@ static exprt::operandst instantiate_byte_array(
   bytes.reserve(upper_bound - lower_bound);
   for(std::size_t i = lower_bound; i < upper_bound; ++i)
   {
-    const index_exprt idx{src, from_integer(i, index_type())};
+    const index_exprt idx{src, from_integer(i, c_index_type())};
     bytes.push_back(simplify_expr(idx, ns));
   }
   return bytes;
@@ -439,11 +439,11 @@ static exprt unpack_array_vector_no_known_bounds(
   symbol_exprt array_comprehension_index{
     "$array_comprehension_index_a_v" +
       std::to_string(array_comprehension_index_counter),
-    index_type()};
+    c_index_type()};
 
-  index_exprt element{
-    src,
-    div_exprt{array_comprehension_index, from_integer(el_bytes, index_type())}};
+  index_exprt element{src,
+                      div_exprt{array_comprehension_index,
+                                from_integer(el_bytes, c_index_type())}};
 
   exprt sub = unpack_rec(element, little_endian, {}, {}, ns, false);
   exprt::operandst sub_operands = instantiate_byte_array(sub, 0, el_bytes, ns);
@@ -552,7 +552,7 @@ static exprt unpack_array_vector(
     }
     else
     {
-      element = index_exprt(src_simp, from_integer(i, index_type()));
+      element = index_exprt(src_simp, from_integer(i, c_index_type()));
     }
 
     // recursively unpack each element so that we eventually just have an array
@@ -925,8 +925,8 @@ static exprt unpack_rec(
     {
       extractbits_exprt extractbits(
         src_as_bitvector,
-        from_integer(bit_offset + 7, index_type()),
-        from_integer(bit_offset, index_type()),
+        from_integer(bit_offset + 7, c_index_type()),
+        from_integer(bit_offset, c_index_type()),
         byte_type);
 
       // endianness_mapt should be the point of reference for mapping out
@@ -1007,7 +1007,7 @@ static exprt lower_byte_extract_array_vector(
   symbol_exprt array_comprehension_index{
     "$array_comprehension_index_a" +
       std::to_string(array_comprehension_index_counter),
-    index_type()};
+    c_index_type()};
 
   plus_exprt new_offset{
     unpacked.offset(),
@@ -1329,7 +1329,7 @@ static exprt lower_byte_update_byte_array_vector_non_const(
   symbol_exprt array_comprehension_index{
     "$array_comprehension_index_u_a_v" +
       std::to_string(array_comprehension_index_counter),
-    index_type()};
+    c_index_type()};
 
   binary_predicate_exprt lower_bound{
     typecast_exprt::conditional_cast(
@@ -1459,7 +1459,7 @@ static exprt lower_byte_update_array_vector_unbounded(
   symbol_exprt array_comprehension_index{
     "$array_comprehension_index_u_a_v_u" +
       std::to_string(array_comprehension_index_counter),
-    index_type()};
+    c_index_type()};
 
   // all arithmetic uses offset/index types
   PRECONDITION(subtype_size.type() == src.offset().type());
@@ -1760,7 +1760,7 @@ static exprt lower_byte_update_array_vector(
   std::size_t i = 0;
   // copy the prefix not affected by the update
   for(; i < num_elements && (i + 1) * *subtype_bits <= offset_bytes * 8; ++i)
-    elements.push_back(index_exprt{src.op(), from_integer(i, index_type())});
+    elements.push_back(index_exprt{src.op(), from_integer(i, c_index_type())});
 
   // the modified elements
   for(; i < num_elements &&
@@ -1795,7 +1795,7 @@ static exprt lower_byte_update_array_vector(
 
     const byte_update_exprt bu{
       src.id(),
-      index_exprt{src.op(), from_integer(i, index_type())},
+      index_exprt{src.op(), from_integer(i, c_index_type())},
       from_integer(update_offset < 0 ? 0 : update_offset, src.offset().type()),
       array_exprt{
         std::move(update_values),
@@ -1805,7 +1805,7 @@ static exprt lower_byte_update_array_vector(
 
   // copy the tail not affected by the update
   for(; i < num_elements; ++i)
-    elements.push_back(index_exprt{src.op(), from_integer(i, index_type())});
+    elements.push_back(index_exprt{src.op(), from_integer(i, c_index_type())});
 
   if(is_array)
     return simplify_expr(
diff --git a/src/util/c_types.cpp b/src/util/c_types.cpp
index a54ac084d44..15644fc42b0 100644
--- a/src/util/c_types.cpp
+++ b/src/util/c_types.cpp
@@ -13,20 +13,30 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "pointer_offset_size.h"
 #include "std_types.h"
 
-bitvector_typet index_type()
+bitvector_typet c_index_type()
 {
   // same as signed size type
   return signed_size_type();
 }
 
+bitvector_typet index_type()
+{
+  return c_index_type();
+}
+
 /// return type of enum constants
-bitvector_typet enum_constant_type()
+bitvector_typet c_enum_constant_type()
 {
   // usually same as 'int',
   // but might be unsigned, or shorter than 'int'
   return signed_int_type();
 }
 
+bitvector_typet enum_constant_type()
+{
+  return c_enum_constant_type();
+}
+
 signedbv_typet signed_int_type()
 {
   signedbv_typet result(config.ansi_c.int_width);
diff --git a/src/util/c_types.h b/src/util/c_types.h
index 037006a81ac..6eda9c9fd45 100644
--- a/src/util/c_types.h
+++ b/src/util/c_types.h
@@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_UTIL_C_TYPES_H
 #define CPROVER_UTIL_C_TYPES_H
 
+#include "deprecate.h"
 #include "pointer_expr.h"
 
 /// Type for C bit fields
@@ -403,8 +404,15 @@ inline code_with_contract_typet &to_code_with_contract_type(typet &type)
   return static_cast<code_with_contract_typet &>(type);
 }
 
+DEPRECATED(
+  SINCE(2022, 1, 13, "use c_index_type() or array_typet::index_type() instead"))
 bitvector_typet index_type();
+
+DEPRECATED(SINCE(2022, 1, 13, "use c_enum_constant_type() instead"))
 bitvector_typet enum_constant_type();
+
+bitvector_typet c_enum_constant_type();
+bitvector_typet c_index_type();
 signedbv_typet signed_int_type();
 unsignedbv_typet unsigned_int_type();
 signedbv_typet signed_long_int_type();
diff --git a/src/util/pointer_expr.cpp b/src/util/pointer_expr.cpp
index dcc6f319747..a26f6f74238 100644
--- a/src/util/pointer_expr.cpp
+++ b/src/util/pointer_expr.cpp
@@ -43,8 +43,8 @@ static void build_object_descriptor_rec(
     dest.offset() = plus_exprt(
       dest.offset(),
       mult_exprt(
-        typecast_exprt::conditional_cast(index.index(), index_type()),
-        typecast_exprt::conditional_cast(sub_size.value(), index_type())));
+        typecast_exprt::conditional_cast(index.index(), c_index_type()),
+        typecast_exprt::conditional_cast(sub_size.value(), c_index_type())));
   }
   else if(expr.id() == ID_member)
   {
@@ -58,7 +58,7 @@ static void build_object_descriptor_rec(
 
     dest.offset() = plus_exprt(
       dest.offset(),
-      typecast_exprt::conditional_cast(offset.value(), index_type()));
+      typecast_exprt::conditional_cast(offset.value(), c_index_type()));
   }
   else if(
     expr.id() == ID_byte_extract_little_endian ||
@@ -73,7 +73,7 @@ static void build_object_descriptor_rec(
     dest.offset() = plus_exprt(
       dest.offset(),
       typecast_exprt::conditional_cast(
-        to_byte_extract_expr(expr).offset(), index_type()));
+        to_byte_extract_expr(expr).offset(), c_index_type()));
   }
   else if(expr.id() == ID_typecast)
   {
@@ -110,7 +110,7 @@ void object_descriptor_exprt::build(const exprt &expr, const namespacet &ns)
   object() = expr;
 
   if(offset().id() == ID_unknown)
-    offset() = from_integer(0, index_type());
+    offset() = from_integer(0, c_index_type());
 
   build_object_descriptor_rec(ns, expr, *this);
   simplify(offset(), ns);
diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp
index 3abc5c4cd7e..d6be1f65240 100644
--- a/src/util/pointer_offset_size.cpp
+++ b/src/util/pointer_offset_size.cpp
@@ -707,7 +707,7 @@ optionalt<exprt> get_subexpression_at_offset(
   }
 
   return make_byte_extract(
-    expr, from_integer(offset_bytes, index_type()), target_type_raw);
+    expr, from_integer(offset_bytes, c_index_type()), target_type_raw);
 }
 
 optionalt<exprt> get_subexpression_at_offset(
diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp
index 87b566759d8..dab0e2acfbe 100644
--- a/src/util/simplify_expr_pointer.cpp
+++ b/src/util/simplify_expr_pointer.cpp
@@ -98,7 +98,7 @@ simplify_exprt::simplify_address_of_arg(const exprt &expr)
           pointer_type.subtype() = new_index_expr.type();
 
           typecast_exprt typecast_expr(
-            from_integer((*step_size) * (*index) + address, index_type()),
+            from_integer((*step_size) * (*index) + address, c_index_type()),
             pointer_type);
 
           return dereference_exprt{typecast_expr};
@@ -142,7 +142,7 @@ simplify_exprt::simplify_address_of_arg(const exprt &expr)
             to_dereference_expr(new_member_expr.struct_op()).pointer().type());
           pointer_type.subtype() = new_member_expr.type();
           typecast_exprt typecast_expr(
-            from_integer(address + *offset, index_type()), pointer_type);
+            from_integer(address + *offset, c_index_type()), pointer_type);
           return dereference_exprt{typecast_expr};
         }
       }
diff --git a/src/util/std_types.cpp b/src/util/std_types.cpp
index 526e2b4c56d..3e7ae8cd683 100644
--- a/src/util/std_types.cpp
+++ b/src/util/std_types.cpp
@@ -32,7 +32,7 @@ void array_typet::check(const typet &type, const validation_modet vm)
 typet array_typet::index_type() const
 {
   // we may wish to make the index type part of the array type
-  return ::index_type();
+  return c_index_type();
 }
 
 /// Return the sequence number of the component with given name.
@@ -246,7 +246,7 @@ vector_typet::vector_typet(const typet &_subtype, const constant_exprt &_size)
 typet vector_typet::index_type() const
 {
   // we may wish to make the index type part of the vector type
-  return ::index_type();
+  return c_index_type();
 }
 
 const constant_exprt &vector_typet::size() const
diff --git a/src/util/string_constant.cpp b/src/util/string_constant.cpp
index 15f61a0eeef..8b44cc1119f 100644
--- a/src/util/string_constant.cpp
+++ b/src/util/string_constant.cpp
@@ -20,7 +20,7 @@ string_constantt::string_constantt(const irep_idt &_value)
 
 void string_constantt::set_value(const irep_idt &value)
 {
-  exprt size_expr=from_integer(value.size()+1, index_type());
+  exprt size_expr = from_integer(value.size() + 1, c_index_type());
   type()=array_typet(char_type(), size_expr);
   set(ID_value, value);
 }
@@ -33,7 +33,7 @@ array_exprt string_constantt::to_array_expr() const
   const typet &char_type = to_array_type(type()).subtype();
   bool char_is_unsigned=char_type.id()==ID_unsignedbv;
 
-  exprt size=from_integer(string_size, index_type());
+  exprt size = from_integer(string_size, c_index_type());
 
   array_exprt dest({}, array_typet(char_type, size));
 
diff --git a/unit/solvers/lowering/byte_operators.cpp b/unit/solvers/lowering/byte_operators.cpp
index f9eba47c89b..2b5fba38f04 100644
--- a/unit/solvers/lowering/byte_operators.cpp
+++ b/unit/solvers/lowering/byte_operators.cpp
@@ -58,7 +58,7 @@ TEST_CASE("byte extract and bits", "[core][solvers][lowering][byte_extract]")
     const byte_extract_exprt be1{little_endian ? ID_byte_extract_little_endian
                                                : ID_byte_extract_big_endian,
                                  sixteen_bits,
-                                 from_integer(0, index_type()),
+                                 from_integer(0, c_index_type()),
                                  bit_array_type};
     const exprt lower_be1 = lower_byte_extract(be1, ns);
     REQUIRE(lower_be1 == *array_of_bits);
@@ -83,7 +83,7 @@ TEST_CASE("byte extract and bits", "[core][solvers][lowering][byte_extract]")
     const byte_extract_exprt be1{little_endian ? ID_byte_extract_little_endian
                                                : ID_byte_extract_big_endian,
                                  sixteen_bits,
-                                 from_integer(0, index_type()),
+                                 from_integer(0, c_index_type()),
                                  bit_array_type};
     const exprt lower_be1 = lower_byte_extract(be1, ns);
     REQUIRE(lower_be1 == *array_of_bits);
@@ -106,7 +106,7 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
     const byte_extract_exprt be1(
       ID_byte_extract_little_endian,
       deadbeef,
-      from_integer(1, index_type()),
+      from_integer(1, c_index_type()),
       signedbv_typet(8));
 
     THEN("byte_extract lowering yields the expected value")
@@ -135,7 +135,7 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
     const byte_extract_exprt be1(
       ID_byte_extract_little_endian,
       deadbeef,
-      from_integer(1, index_type()),
+      from_integer(1, c_index_type()),
       struct_typet(
         {{"unbounded_array",
           array_typet(
@@ -163,7 +163,7 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
     const byte_extract_exprt be1(
       ID_byte_extract_little_endian,
       deadbeef,
-      from_integer(1, index_type()),
+      from_integer(1, c_index_type()),
       union_typet(
         {{"unbounded_array",
           array_typet(
@@ -191,7 +191,7 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
     const byte_extract_exprt be1(
       ID_byte_extract_little_endian,
       deadbeef,
-      from_integer(1, index_type()),
+      from_integer(1, c_index_type()),
       union_typet{});
 
     THEN("byte_extract lowering does not raise an exception")
@@ -216,7 +216,7 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
     const byte_extract_exprt be1(
       ID_byte_extract_little_endian,
       s,
-      from_integer(1, index_type()),
+      from_integer(1, c_index_type()),
       unsignedbv_typet(16));
 
     THEN("byte_extract lowering yields the expected value")
@@ -331,7 +331,7 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
             REQUIRE(r.has_value());
 
             const byte_extract_exprt be(
-              endianness, *s, from_integer(2, index_type()), t2);
+              endianness, *s, from_integer(2, c_index_type()), t2);
 
             const exprt lower_be = lower_byte_extract(be, ns);
             const exprt lower_be_s = simplify_expr(lower_be, ns);
@@ -364,7 +364,7 @@ SCENARIO("byte_update_lowering", "[core][solvers][lowering][byte_update]")
     const byte_update_exprt bu1(
       ID_byte_update_little_endian,
       deadbeef,
-      from_integer(1, index_type()),
+      from_integer(1, c_index_type()),
       from_integer(0x42, unsignedbv_typet(8)));
 
     THEN("byte_update lowering yields the expected value")
@@ -484,7 +484,7 @@ SCENARIO("byte_update_lowering", "[core][solvers][lowering][byte_update]")
             REQUIRE(r.has_value());
 
             const byte_update_exprt bu(
-              endianness, *s, from_integer(2, index_type()), *u);
+              endianness, *s, from_integer(2, c_index_type()), *u);
 
             const exprt lower_bu = lower_byte_operators(bu, ns);
             const exprt lower_bu_s = simplify_expr(lower_bu, ns);
diff --git a/unit/util/pointer_offset_size.cpp b/unit/util/pointer_offset_size.cpp
index 3a1a5f8edd4..a091f1c7f42 100644
--- a/unit/util/pointer_offset_size.cpp
+++ b/unit/util/pointer_offset_size.cpp
@@ -35,24 +35,24 @@ TEST_CASE("Build subexpression to access element at offset into array")
 
   {
     const auto result = get_subexpression_at_offset(a, 0, t, ns);
-    REQUIRE(result.value() == index_exprt(a, from_integer(0, index_type())));
+    REQUIRE(result.value() == index_exprt(a, from_integer(0, c_index_type())));
   }
 
   {
     const auto result = get_subexpression_at_offset(a, 32 / 8, t, ns);
-    REQUIRE(result.value() == index_exprt(a, from_integer(1, index_type())));
+    REQUIRE(result.value() == index_exprt(a, from_integer(1, c_index_type())));
   }
 
   {
     const auto result =
       get_subexpression_at_offset(a, from_integer(0, size_type()), t, ns);
-    REQUIRE(result.value() == index_exprt(a, from_integer(0, index_type())));
+    REQUIRE(result.value() == index_exprt(a, from_integer(0, c_index_type())));
   }
 
   {
     const auto result =
       get_subexpression_at_offset(a, size_of_expr(t, ns).value(), t, ns);
-    REQUIRE(result.value() == index_exprt(a, from_integer(1, index_type())));
+    REQUIRE(result.value() == index_exprt(a, from_integer(1, c_index_type())));
   }
 
   {
@@ -60,8 +60,8 @@ TEST_CASE("Build subexpression to access element at offset into array")
     const auto result = get_subexpression_at_offset(a, 1, small_t, ns);
     REQUIRE(
       result.value() == make_byte_extract(
-                          index_exprt(a, from_integer(0, index_type())),
-                          from_integer(1, index_type()),
+                          index_exprt(a, from_integer(0, c_index_type())),
+                          from_integer(1, c_index_type()),
                           small_t));
   }
 
@@ -73,7 +73,7 @@ TEST_CASE("Build subexpression to access element at offset into array")
     // index_exprt.
     REQUIRE(
       result.value() ==
-      make_byte_extract(a, from_integer(3, index_type()), int16_t));
+      make_byte_extract(a, from_integer(3, c_index_type()), int16_t));
   }
 }
 
@@ -121,6 +121,6 @@ TEST_CASE("Build subexpression to access element at offset into struct")
     REQUIRE(
       result.value() ==
       make_byte_extract(
-        member_exprt(s, "foo", t), from_integer(1, index_type()), small_t));
+        member_exprt(s, "foo", t), from_integer(1, c_index_type()), small_t));
   }
 }
diff --git a/unit/util/simplify_expr.cpp b/unit/util/simplify_expr.cpp
index 0c830c84f69..dedebbe52b2 100644
--- a/unit/util/simplify_expr.cpp
+++ b/unit/util/simplify_expr.cpp
@@ -31,7 +31,7 @@ TEST_CASE("Simplify pointer_offset(address of array index)", "[core][util]")
 
   array_typet array_type(char_type(), from_integer(2, size_type()));
   symbol_exprt array("A", array_type);
-  index_exprt index(array, from_integer(1, index_type()));
+  index_exprt index(array, from_integer(1, c_index_type()));
   address_of_exprt address_of(index);
 
   exprt p_o=pointer_offset(address_of);
@@ -79,7 +79,7 @@ TEST_CASE("Simplify byte extract", "[core][util]")
   // object
   symbol_exprt s("foo", size_type());
   byte_extract_exprt be =
-    make_byte_extract(s, from_integer(0, index_type()), size_type());
+    make_byte_extract(s, from_integer(0, c_index_type()), size_type());
 
   exprt simp = simplify_expr(be, ns);
 
diff --git a/unit/util/std_expr.cpp b/unit/util/std_expr.cpp
index 51d5c68506b..b21425164c9 100644
--- a/unit/util/std_expr.cpp
+++ b/unit/util/std_expr.cpp
@@ -50,13 +50,13 @@ TEST_CASE("object descriptor expression", "[unit][util][std_expr]")
   {
     const symbol_exprt s("array", array_type);
     // s[1]
-    const index_exprt index(s, from_integer(1, index_type()));
+    const index_exprt index(s, from_integer(1, c_index_type()));
 
     object_descriptor_exprt ode;
     ode.build(index, ns);
     REQUIRE(ode.root_object() == s);
     // in LP64 a signed int is 4 bytes
-    REQUIRE(simplify_expr(ode.offset(), ns) == from_integer(4, index_type()));
+    REQUIRE(simplify_expr(ode.offset(), ns) == from_integer(4, c_index_type()));
   }
 
   SECTION("object descriptors of member expressions")
@@ -65,12 +65,12 @@ TEST_CASE("object descriptor expression", "[unit][util][std_expr]")
     // s.foo
     const member_exprt member(s, "foo", array_type);
     // s.foo[1]
-    const index_exprt index(member, from_integer(1, index_type()));
+    const index_exprt index(member, from_integer(1, c_index_type()));
 
     object_descriptor_exprt ode;
     ode.build(index, ns);
     REQUIRE(ode.root_object() == s);
     // in LP64 a signed int is 4 bytes
-    REQUIRE(simplify_expr(ode.offset(), ns) == from_integer(4, index_type()));
+    REQUIRE(simplify_expr(ode.offset(), ns) == from_integer(4, c_index_type()));
   }
 }