diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp
index 5c2135e8afe..d97a769d59f 100644
--- a/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -21,6 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/ieee_float.h>
+#include <util/invariant.h>
 #include <util/namespace.h>
 #include <util/prefix.h>
 #include <util/simplify_expr.h>
@@ -163,9 +164,11 @@ const exprt java_bytecode_convert_methodt::variable(
   size_t address,
   java_bytecode_convert_methodt::variable_cast_argumentt do_cast)
 {
-  irep_idt number=to_constant_expr(arg).get_value();
+  mp_integer number;
+  bool ret=to_integer(to_constant_expr(arg), number);
+  CHECK_RETURN(!ret);
 
-  std::size_t number_int=safe_string2size_t(id2string(number));
+  std::size_t number_int=integer2size_t(number);
   typet t=java_type_from_char(type_char);
   variablest &var_list=variables[number_int];
 
@@ -176,7 +179,7 @@ const exprt java_bytecode_convert_methodt::variable(
   if(var.symbol_expr.get_identifier().empty())
   {
     // an unnamed local variable
-    irep_idt base_name="anonlocal::"+id2string(number)+type_char;
+    irep_idt base_name="anonlocal::"+std::to_string(number_int)+type_char;
     irep_idt identifier=id2string(current_method)+"::"+id2string(base_name);
 
     symbol_exprt result(identifier, t);
@@ -848,8 +851,9 @@ codet java_bytecode_convert_methodt::convert_instructions(
     {
       assert(!i_it->args.empty());
 
-      const unsigned target=safe_string2unsigned(
-        id2string(to_constant_expr(i_it->args[0]).get_value()));
+      unsigned target;
+      bool ret=to_unsigned_integer(to_constant_expr(i_it->args[0]), target);
+      DATA_INVARIANT(!ret, "target expected to be unsigned integer");
       targets.insert(target);
 
       a_entry.first->second.successors.push_back(target);
@@ -873,8 +877,9 @@ codet java_bytecode_convert_methodt::convert_instructions(
       {
         if(is_label)
         {
-          const unsigned target=safe_string2unsigned(
-            id2string(to_constant_expr(arg).get_value()));
+          unsigned target;
+          bool ret=to_unsigned_integer(to_constant_expr(arg), target);
+          DATA_INVARIANT(!ret, "target expected to be unsigned integer");
           targets.insert(target);
           a_entry.first->second.successors.push_back(target);
         }
@@ -955,9 +960,11 @@ codet java_bytecode_convert_methodt::convert_instructions(
        statement[statement.size()-2]=='_' &&
        isdigit(statement[statement.size()-1]))
     {
-      arg0=constant_exprt(
-        std::string(id2string(statement), statement.size()-1, 1),
-        integer_typet());
+      arg0=
+        from_integer(
+          string2integer(
+            std::string(id2string(statement), statement.size()-1, 1)),
+          java_int_type());
       statement=std::string(id2string(statement), 0, statement.size()-2);
     }
 
@@ -1353,16 +1360,20 @@ codet java_bytecode_convert_methodt::convert_instructions(
     else if(statement=="goto" || statement=="goto_w")
     {
       assert(op.empty() && results.empty());
-      irep_idt number=to_constant_expr(arg0).get_value();
-      code_gotot code_goto(label(number));
+      mp_integer number;
+      bool ret=to_integer(to_constant_expr(arg0), number);
+      INVARIANT(!ret, "goto argument should be an integer");
+      code_gotot code_goto(label(integer2string(number)));
       c=code_goto;
     }
     else if(statement=="jsr" || statement=="jsr_w")
     {
       // As 'goto', except we must also push the subroutine return address:
       assert(op.empty() && results.size()==1);
-      irep_idt number=to_constant_expr(arg0).get_value();
-      code_gotot code_goto(label(number));
+      mp_integer number;
+      bool ret=to_integer(to_constant_expr(arg0), number);
+      INVARIANT(!ret, "jsr argument should be an integer");
+      code_gotot code_goto(label(integer2string(number)));
       c=code_goto;
       results[0]=
         from_integer(
@@ -1422,9 +1433,13 @@ codet java_bytecode_convert_methodt::convert_instructions(
           ieee_float_spect::double_precision());
 
         ieee_floatt value(spec);
-        const typet &arg_type(arg0.type());
-        if(ID_integer==arg_type.id())
-          value.from_integer(arg0.get_int(ID_value));
+        if(arg0.type().id()!=ID_floatbv)
+        {
+          mp_integer number;
+          bool ret=to_integer(to_constant_expr(arg0), number);
+          DATA_INVARIANT(!ret, "failed to convert constant");
+          value.from_integer(number);
+        }
         else
           value.from_expr(to_constant_expr(arg0));
 
@@ -1432,23 +1447,29 @@ codet java_bytecode_convert_methodt::convert_instructions(
       }
       else
       {
-        const unsigned value(arg0.get_unsigned_int(ID_value));
+        mp_integer value;
+        bool ret=to_integer(to_constant_expr(arg0), value);
+        DATA_INVARIANT(!ret, "failed to convert constant");
         const typet type=java_type_from_char(statement[0]);
         results[0]=from_integer(value, type);
       }
     }
     else if(statement==patternt("?ipush"))
     {
-      assert(results.size()==1);
-      mp_integer int_value;
-      bool ret=to_integer(to_constant_expr(arg0), int_value);
-      INVARIANT(!ret, "?ipush argument should be an integer");
-      results[0]=from_integer(int_value, java_int_type());
+      PRECONDITION(results.size()==1);
+      DATA_INVARIANT(
+        arg0.id()==ID_constant,
+        "ipush argument expected to be constant");
+      results[0]=arg0;
+      if(arg0.type()!=java_int_type())
+        results[0].make_typecast(java_int_type());
     }
     else if(statement==patternt("if_?cmp??"))
     {
-      irep_idt number=to_constant_expr(arg0).get_value();
       assert(op.size()==2 && results.empty());
+      mp_integer number;
+      bool ret=to_integer(to_constant_expr(arg0), number);
+      INVARIANT(!ret, "if_?cmp?? argument should be an integer");
 
       code_ifthenelset code_branch;
       const irep_idt cmp_op=get_if_cmp_operator(statement);
@@ -1463,7 +1484,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
 
       code_branch.cond()=condition;
       code_branch.cond().add_source_location()=i_it->source_location;
-      code_branch.then_case()=code_gotot(label(number));
+      code_branch.then_case()=code_gotot(label(integer2string(number)));
       code_branch.then_case().add_source_location()=i_it->source_location;
       code_branch.add_source_location()=i_it->source_location;
 
@@ -1480,15 +1501,17 @@ codet java_bytecode_convert_methodt::convert_instructions(
         statement=="ifle"?ID_le:
         (assert(false), "");
 
-      irep_idt number=to_constant_expr(arg0).get_value();
       assert(op.size()==1 && results.empty());
+      mp_integer number;
+      bool ret=to_integer(to_constant_expr(arg0), number);
+      INVARIANT(!ret, "if?? argument should be an integer");
 
       code_ifthenelset code_branch;
       code_branch.cond()=
         binary_relation_exprt(op[0], id, from_integer(0, op[0].type()));
       code_branch.cond().add_source_location()=i_it->source_location;
       code_branch.cond().add_source_location().set_function(method_id);
-      code_branch.then_case()=code_gotot(label(number));
+      code_branch.then_case()=code_gotot(label(integer2string(number)));
       code_branch.then_case().add_source_location()=i_it->source_location;
       code_branch.then_case().add_source_location().set_function(method_id);
       code_branch.add_source_location()=i_it->source_location;
@@ -1498,13 +1521,15 @@ codet java_bytecode_convert_methodt::convert_instructions(
     }
     else if(statement==patternt("ifnonnull"))
     {
-      irep_idt number=to_constant_expr(arg0).get_value();
       assert(op.size()==1 && results.empty());
+      mp_integer number;
+      bool ret=to_integer(to_constant_expr(arg0), number);
+      INVARIANT(!ret, "ifnonnull argument should be an integer");
       code_ifthenelset code_branch;
       const typecast_exprt lhs(op[0], java_reference_type(empty_typet()));
       const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type())));
       code_branch.cond()=binary_relation_exprt(lhs, ID_notequal, rhs);
-      code_branch.then_case()=code_gotot(label(number));
+      code_branch.then_case()=code_gotot(label(integer2string(number)));
       code_branch.then_case().add_source_location()=i_it->source_location;
       code_branch.add_source_location()=i_it->source_location;
 
@@ -1513,12 +1538,14 @@ codet java_bytecode_convert_methodt::convert_instructions(
     else if(statement==patternt("ifnull"))
     {
       assert(op.size()==1 && results.empty());
-      irep_idt number=to_constant_expr(arg0).get_value();
+      mp_integer number;
+      bool ret=to_integer(to_constant_expr(arg0), number);
+      INVARIANT(!ret, "ifnull argument should be an integer");
       code_ifthenelset code_branch;
       const typecast_exprt lhs(op[0], java_reference_type(empty_typet()));
       const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type())));
       code_branch.cond()=binary_relation_exprt(lhs, ID_equal, rhs);
-      code_branch.then_case()=code_gotot(label(number));
+      code_branch.then_case()=code_gotot(label(integer2string(number)));
       code_branch.then_case().add_source_location()=i_it->source_location;
       code_branch.add_source_location()=i_it->source_location;
 
@@ -1540,9 +1567,12 @@ codet java_bytecode_convert_methodt::convert_instructions(
       code_assignt code_assign;
       code_assign.lhs()=
         variable(arg0, 'i', i_it->address, NO_CAST);
+      exprt arg1_int_type=arg1;
+      if(arg1.type()!=java_int_type())
+        arg1_int_type.make_typecast(java_int_type());
       code_assign.rhs()=plus_exprt(
         variable(arg0, 'i', i_it->address, CAST_AS_NEEDED),
-        typecast_exprt(arg1, java_int_type()));
+        arg1_int_type);
       block.copy_to_operands(code_assign);
       c=block;
     }
@@ -1579,10 +1609,16 @@ codet java_bytecode_convert_methodt::convert_instructions(
       const std::size_t width=type.get_size_t(ID_width);
       typet target=unsignedbv_typet(width);
 
-      const typecast_exprt lhs(op[0], target);
-      const typecast_exprt rhs(op[1], target);
+      exprt lhs=op[0];
+      if(lhs.type()!=target)
+        lhs.make_typecast(target);
+      exprt rhs=op[1];
+      if(rhs.type()!=target)
+        rhs.make_typecast(target);
 
-      results[0]=typecast_exprt(lshr_exprt(lhs, rhs), op[0].type());
+      results[0]=lshr_exprt(lhs, rhs);
+      if(results[0].type()!=op[0].type())
+        results[0].make_typecast(op[0].type());
     }
     else if(statement==patternt("?add"))
     {
@@ -1815,7 +1851,10 @@ codet java_bytecode_convert_methodt::convert_instructions(
     else if(statement==patternt("?2?")) // i2c etc.
     {
       assert(op.size()==1 && results.size()==1);
-      results[0]=typecast_exprt(op[0], java_type_from_char(statement[2]));
+      typet type=java_type_from_char(statement[2]);
+      results[0]=op[0];
+      if(results[0].type()!=type)
+        results[0].make_typecast(type);
     }
     else if(statement=="new")
     {
@@ -1901,8 +1940,10 @@ codet java_bytecode_convert_methodt::convert_instructions(
     {
       // The first argument is the type, the second argument is the number of
       // dimensions.  The size of each dimension is on the stack.
-      irep_idt number=to_constant_expr(arg1).get_value();
-      std::size_t dimension=safe_string2size_t(id2string(number));
+      mp_integer number;
+      bool ret=to_integer(to_constant_expr(arg1), number);
+      INVARIANT(!ret, "multianewarray argument should be an integer");
+      std::size_t dimension=integer2size_t(number);
 
       op=pop(dimension);
       assert(results.size()==1);
@@ -1976,8 +2017,10 @@ codet java_bytecode_convert_methodt::convert_instructions(
           code_switch_caset code_case;
           code_case.add_source_location()=i_it->source_location;
 
-          irep_idt number=to_constant_expr(*a_it).get_value();
-          code_case.code()=code_gotot(label(number));
+          mp_integer number;
+          bool ret=to_integer(to_constant_expr(*a_it), number);
+          DATA_INVARIANT(!ret, "case label expected to be integer");
+          code_case.code()=code_gotot(label(integer2string(number)));
           code_case.code().add_source_location()=i_it->source_location;
 
           if(a_it==i_it->args.begin())
@@ -1986,7 +2029,9 @@ codet java_bytecode_convert_methodt::convert_instructions(
           {
             instructiont::argst::const_iterator prev=a_it;
             prev--;
-            code_case.case_op()=typecast_exprt(*prev, op[0].type());
+            code_case.case_op()=*prev;
+            if(code_case.case_op().type()!=op[0].type())
+              code_case.case_op().make_typecast(op[0].type());
             code_case.case_op().add_source_location()=i_it->source_location;
           }
 
diff --git a/src/java_bytecode/java_bytecode_parser.cpp b/src/java_bytecode/java_bytecode_parser.cpp
index d24141b76da..f93818eb274 100644
--- a/src/java_bytecode/java_bytecode_parser.cpp
+++ b/src/java_bytecode/java_bytecode_parser.cpp
@@ -703,7 +703,7 @@ void java_bytecode_parsert::rbytecode(
     case 'b': // a signed byte
       {
         s1 c=read_u1();
-        instruction.args.push_back(from_integer(c, integer_typet()));
+        instruction.args.push_back(from_integer(c, signedbv_typet(8)));
       }
       address+=1;
 
@@ -712,8 +712,8 @@ void java_bytecode_parsert::rbytecode(
     case 'o': // two byte branch offset, signed
       {
         s2 offset=read_u2();
-        instruction
-          .args.push_back(from_integer(address+offset, integer_typet()));
+        instruction.args.push_back(
+          from_integer(address+offset, signedbv_typet(16)));
       }
       address+=2;
       break;
@@ -721,8 +721,8 @@ void java_bytecode_parsert::rbytecode(
     case 'O': // four byte branch offset, signed
       {
         s4 offset=read_u4();
-        instruction
-          .args.push_back(from_integer(address+offset, integer_typet()));
+        instruction.args.push_back(
+          from_integer(address+offset, signedbv_typet(32)));
       }
       address+=4;
       break;
@@ -730,7 +730,7 @@ void java_bytecode_parsert::rbytecode(
     case 'v': // local variable index (one byte)
       {
         u1 v=read_u1();
-        instruction.args.push_back(from_integer(v, integer_typet()));
+        instruction.args.push_back(from_integer(v, unsignedbv_typet(8)));
       }
       address+=1;
       break;
@@ -740,17 +740,17 @@ void java_bytecode_parsert::rbytecode(
       if(wide_instruction)
       {
         u2 v=read_u2();
-        instruction.args.push_back(from_integer(v, integer_typet()));
+        instruction.args.push_back(from_integer(v, unsignedbv_typet(16)));
         s2 c=read_u2();
-        instruction.args.push_back(from_integer(c, integer_typet()));
+        instruction.args.push_back(from_integer(c, signedbv_typet(16)));
         address+=4;
       }
       else // local variable index (one byte) plus one signed byte
       {
         u1 v=read_u1();
-        instruction.args.push_back(from_integer(v, integer_typet()));
+        instruction.args.push_back(from_integer(v, unsignedbv_typet(8)));
         s1 c=read_u1();
-        instruction.args.push_back(from_integer(c, integer_typet()));
+        instruction.args.push_back(from_integer(c, signedbv_typet(8)));
         address+=2;
       }
       break;
@@ -760,9 +760,9 @@ void java_bytecode_parsert::rbytecode(
         u2 c=read_u2();
         instruction.args.push_back(constant(c));
         u1 b1=read_u1();
-        instruction.args.push_back(from_integer(b1, integer_typet()));
+        instruction.args.push_back(from_integer(b1, unsignedbv_typet(8)));
         u1 b2=read_u1();
-        instruction.args.push_back(from_integer(b2, integer_typet()));
+        instruction.args.push_back(from_integer(b2, unsignedbv_typet(8)));
       }
       address+=4;
       break;
@@ -776,8 +776,8 @@ void java_bytecode_parsert::rbytecode(
 
         // now default value
         s4 default_value=read_u4();
-        instruction.args
-          .push_back(from_integer(base_offset+default_value, integer_typet()));
+        instruction.args.push_back(
+          from_integer(base_offset+default_value, signedbv_typet(32)));
         address+=4;
 
         // number of pairs
@@ -788,9 +788,10 @@ void java_bytecode_parsert::rbytecode(
         {
           s4 match=read_u4();
           s4 offset=read_u4();
-          instruction.args.push_back(from_integer(match, integer_typet()));
-          instruction.args
-            .push_back(from_integer(base_offset+offset, integer_typet()));
+          instruction.args.push_back(
+            from_integer(match, signedbv_typet(32)));
+          instruction.args.push_back(
+            from_integer(base_offset+offset, signedbv_typet(32)));
           address+=8;
         }
       }
@@ -805,8 +806,8 @@ void java_bytecode_parsert::rbytecode(
 
         // now default value
         s4 default_value=read_u4();
-        instruction.args
-          .push_back(from_integer(base_offset+default_value, integer_typet()));
+        instruction.args.push_back(
+          from_integer(base_offset+default_value, signedbv_typet(32)));
         address+=4;
 
         // now low value
@@ -821,9 +822,9 @@ void java_bytecode_parsert::rbytecode(
         for(s4 i=low_value; i<=high_value; i++)
         {
           s4 offset=read_u4();
-          instruction.args.push_back(from_integer(i, integer_typet()));
-          instruction.args
-            .push_back(from_integer(base_offset+offset, integer_typet()));
+          instruction.args.push_back(from_integer(i, signedbv_typet(32)));
+          instruction.args.push_back(
+            from_integer(base_offset+offset, signedbv_typet(32)));
           address+=4;
         }
       }
@@ -834,7 +835,8 @@ void java_bytecode_parsert::rbytecode(
         u2 c=read_u2(); // constant-pool index
         instruction.args.push_back(constant(c));
         u1 dimensions=read_u1(); // number of dimensions
-        instruction.args.push_back(from_integer(dimensions, integer_typet()));
+        instruction.args.push_back(
+          from_integer(dimensions, unsignedbv_typet(8)));
         address+=3;
       }
       break;
@@ -862,7 +864,7 @@ void java_bytecode_parsert::rbytecode(
     case 's': // a signed short
       {
         s2 s=read_u2();
-        instruction.args.push_back(from_integer(s, integer_typet()));
+        instruction.args.push_back(from_integer(s, signedbv_typet(16)));
       }
       address+=2;
       break;
diff --git a/src/java_bytecode/java_local_variable_table.cpp b/src/java_bytecode/java_local_variable_table.cpp
index 94d5062fb24..70b2568476a 100644
--- a/src/java_bytecode/java_local_variable_table.cpp
+++ b/src/java_bytecode/java_local_variable_table.cpp
@@ -13,6 +13,8 @@ Author: Chris Smowton, chris.smowton@diffblue.com
 
 #include "java_types.h"
 
+#include <util/arith_tools.h>
+#include <util/invariant.h>
 #include <util/string2int.h>
 
 #include <climits>
@@ -177,21 +179,22 @@ static bool is_store_to_slot(
   if(!(prevstatement.size()>=1 && prevstatement.substr(1, 5)=="store"))
     return false;
 
-  std::string storeslot;
+  unsigned storeslotidx;
   if(inst.args.size()==1)
   {
     // Store with an argument:
     const auto &arg=inst.args[0];
-    storeslot=id2string(to_constant_expr(arg).get_value());
+    bool ret=to_unsigned_integer(to_constant_expr(arg), storeslotidx);
+    CHECK_RETURN(!ret);
   }
   else
   {
     // Store shorthands, like "store_0", "store_1"
     assert(prevstatement[6]=='_' && prevstatement.size()==8);
-    storeslot=prevstatement[7];
+    std::string storeslot(1, prevstatement[7]);
     assert(isdigit(storeslot[0]));
+    storeslotidx=safe_string2unsigned(storeslot);
   }
-  auto storeslotidx=safe_string2unsigned(storeslot);
   return storeslotidx==slotidx;
 }
 
diff --git a/src/solvers/flattening/boolbv_member.cpp b/src/solvers/flattening/boolbv_member.cpp
index 448e80f5653..0f01e2be959 100644
--- a/src/solvers/flattening/boolbv_member.cpp
+++ b/src/solvers/flattening/boolbv_member.cpp
@@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/base_type.h>
 #include <util/byte_operators.h>
 #include <util/arith_tools.h>
+#include <util/c_types.h>
 
 bvt boolbvt::convert_member(const member_exprt &expr)
 {
@@ -24,7 +25,7 @@ bvt boolbvt::convert_member(const member_exprt &expr)
     return convert_bv(
       byte_extract_exprt(byte_extract_id(),
                          struct_op,
-                         from_integer(0, integer_typet()),
+                         from_integer(0, index_type()),
                          expr.type()));
   }
   else if(struct_op_type.id()==ID_struct)
diff --git a/src/solvers/flattening/pointer_logic.cpp b/src/solvers/flattening/pointer_logic.cpp
index 3f1ffd47798..1018dfca2b7 100644
--- a/src/solvers/flattening/pointer_logic.cpp
+++ b/src/solvers/flattening/pointer_logic.cpp
@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <cassert>
 
 #include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/std_expr.h>
 #include <util/prefix.h>
 #include <util/pointer_offset_size.h>
@@ -87,7 +88,7 @@ exprt pointer_logict::pointer_expr(
       constant_exprt null(type);
       null.set_value(ID_NULL);
       return plus_exprt(null,
-        from_integer(pointer.offset, integer_typet()));
+        from_integer(pointer.offset, pointer_diff_type()));
     }
   }
   else if(pointer.object==invalid_object) // INVALID?
diff --git a/src/util/std_expr.cpp b/src/util/std_expr.cpp
index cef9446e2e1..f57f4979630 100644
--- a/src/util/std_expr.cpp
+++ b/src/util/std_expr.cpp
@@ -135,7 +135,7 @@ void object_descriptor_exprt::build(
   assert(root_object().type().id()!=ID_empty);
 }
 
-constant_exprt constant_exprt::integer_constant(unsigned v)
+static constant_exprt integer_constant(unsigned v)
 {
   return constant_exprt(std::to_string(v), integer_typet());
 }
@@ -144,7 +144,7 @@ shift_exprt::shift_exprt(
   const exprt &_src,
   const irep_idt &_id,
   const std::size_t _distance):
-  binary_exprt(_src, _id, constant_exprt::integer_constant(_distance))
+  binary_exprt(_src, _id, integer_constant(_distance))
 {
 }
 
@@ -152,7 +152,7 @@ extractbit_exprt::extractbit_exprt(
   const exprt &_src,
   const std::size_t _index):
   binary_predicate_exprt(
-    _src, ID_extractbit, constant_exprt::integer_constant(_index))
+    _src, ID_extractbit, integer_constant(_index))
 {
 }
 
@@ -166,8 +166,8 @@ extractbits_exprt::extractbits_exprt(
   assert(_upper>=_lower);
   operands().resize(3);
   src()=_src;
-  upper()=constant_exprt::integer_constant(_upper);
-  lower()=constant_exprt::integer_constant(_lower);
+  upper()=integer_constant(_upper);
+  lower()=integer_constant(_lower);
 }
 
 /*******************************************************************\
diff --git a/src/util/std_expr.h b/src/util/std_expr.h
index c4837be001a..a47c3afd684 100644
--- a/src/util/std_expr.h
+++ b/src/util/std_expr.h
@@ -3710,8 +3710,6 @@ class constant_exprt:public exprt
   }
 
   bool value_is_zero_string() const;
-
-  static constant_exprt integer_constant(unsigned);
 };
 
 /*! \brief Cast a generic exprt to a \ref constant_exprt
diff --git a/unit/analyses/ai/ai_simplify_lhs.cpp b/unit/analyses/ai/ai_simplify_lhs.cpp
index 2d276fdbbd8..d161df0bffb 100644
--- a/unit/analyses/ai/ai_simplify_lhs.cpp
+++ b/unit/analyses/ai/ai_simplify_lhs.cpp
@@ -16,6 +16,7 @@
 #include <ansi-c/ansi_c_language.h>
 
 #include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/config.h>
 #include <util/namespace.h>
 #include <util/ui_message.h>
@@ -73,7 +74,7 @@ SCENARIO("ai_domain_baset::ai_simplify_lhs",
 
     const unsigned int array_size=5;
     array_typet array_type(
-      signedbv_typet(32), constant_exprt::integer_constant(array_size));
+      signedbv_typet(32), from_integer(array_size, size_type()));
 
     // Verify the results of the setup
     REQUIRE_FALSE(compile_failed);\
@@ -137,7 +138,7 @@ SCENARIO("ai_domain_baset::ai_simplify_lhs",
       {
         REQUIRE(constant_array.operands().size()==i);
         constant_array.operands().push_back(
-          constant_exprt::integer_constant(i));
+          from_integer(i, signedbv_typet(32)));
       }
 
       const index_exprt &index_expr=