diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp
index 280635aed60..5cf742502a0 100644
--- a/src/goto-programs/interpreter.cpp
+++ b/src/goto-programs/interpreter.cpp
@@ -30,7 +30,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "interpreter_class.h"
 #include "remove_returns.h"
 
-const size_t interpretert::npos=std::numeric_limits<size_t>::max();
+const std::size_t interpretert::npos=std::numeric_limits<size_t>::max();
 
 void interpretert::operator()()
 {
@@ -392,7 +392,7 @@ void interpretert::execute_other()
     mp_vectort tmp, rhs;
     evaluate(pc->code.op1(), tmp);
     mp_integer address=evaluate_address(pc->code.op0());
-    size_t size=get_size(pc->code.op0().type());
+    mp_integer size=get_size(pc->code.op0().type());
     while(rhs.size()<size) rhs.insert(rhs.end(), tmp.begin(), tmp.end());
     if(size!=rhs.size())
       error() << "!! failed to obtain rhs (" << rhs.size() << " vs. "
@@ -419,7 +419,7 @@ void interpretert::execute_decl()
 /// \par parameters: an object and a memory offset
 struct_typet::componentt interpretert::get_component(
   const irep_idt &object,
-  unsigned offset)
+  const mp_integer &offset)
 {
   const symbolt &symbol=ns.lookup(object);
   const typet real_type=ns.follow(symbol.type);
@@ -429,12 +429,14 @@ struct_typet::componentt interpretert::get_component(
   const struct_typet &struct_type=to_struct_type(real_type);
   const struct_typet::componentst &components=struct_type.components();
 
+  mp_integer tmp_offset=offset;
+
   for(const auto &c : components)
   {
-    if(offset<=0)
+    if(tmp_offset<=0)
       return c;
 
-    offset-=get_size(c.type());
+    tmp_offset-=get_size(c.type());
   }
 
   throw "access out of struct bounds";
@@ -453,7 +455,7 @@ typet interpretert::get_type(const irep_idt &id) const
 /// type
 exprt interpretert::get_value(
   const typet &type,
-  std::size_t offset,
+  const mp_integer &offset,
   bool use_non_det)
 {
   const typet real_type=ns.follow(type);
@@ -465,14 +467,17 @@ exprt interpretert::get_value(
 
     // Retrieve the values for the individual members
     result.reserve_operands(components.size());
-    for(struct_typet::componentst::const_iterator it=components.begin();
-        it!=components.end(); it++)
+
+    mp_integer tmp_offset=offset;
+
+    for(const auto &c : components)
     {
-      size_t size=get_size(it->type());
-      const exprt operand=get_value(it->type(), offset);
-      offset+=size;
+      mp_integer size=get_size(c.type());
+      const exprt operand=get_value(c.type(), tmp_offset);
+      tmp_offset+=size;
       result.copy_to_operands(operand);
     }
+
     return result;
   }
   else if(real_type.id()==ID_array)
@@ -480,22 +485,20 @@ exprt interpretert::get_value(
     // Get size of array
     exprt result=array_exprt(to_array_type(real_type));
     const exprt &size_expr=static_cast<const exprt &>(type.find(ID_size));
-    size_t subtype_size=get_size(type.subtype());
-    std::size_t count;
+    mp_integer subtype_size=get_size(type.subtype());
+    mp_integer count;
     if(size_expr.id()!=ID_constant)
     {
       count=base_address_to_actual_size(offset)/subtype_size;
     }
     else
     {
-      mp_integer mp_count;
-      to_integer(size_expr, mp_count);
-      count=integer2size_t(mp_count);
+      to_integer(size_expr, count);
     }
 
     // Retrieve the value for each member in the array
-    result.reserve_operands(count);
-    for(unsigned i=0; i<count; i++)
+    result.reserve_operands(integer2size_t(count));
+    for(mp_integer i=0; i<count; ++i)
     {
       const exprt operand=get_value(
         type.subtype(),
@@ -505,11 +508,11 @@ exprt interpretert::get_value(
     return result;
   }
   if(use_non_det &&
-     memory[offset].initialized!=
+     memory[integer2ulong(offset)].initialized!=
      memory_cellt::initializedt::WRITTEN_BEFORE_READ)
     return side_effect_expr_nondett(type);
   mp_vectort rhs;
-  rhs.push_back(memory[offset].value);
+  rhs.push_back(memory[integer2ulong(offset)].value);
   return get_value(type, rhs);
 }
 
@@ -518,7 +521,7 @@ exprt interpretert::get_value(
 exprt interpretert::get_value(
   const typet &type,
   mp_vectort &rhs,
-  std::size_t offset)
+  const mp_integer &offset)
 {
   const typet real_type=ns.follow(type);
   PRECONDITION(!rhs.empty());
@@ -531,11 +534,13 @@ exprt interpretert::get_value(
 
     // Retrieve the values for the individual members
     result.reserve_operands(components.size());
+    mp_integer tmp_offset=offset;
+
     for(const struct_union_typet::componentt &expr : components)
     {
-      size_t size=get_size(expr.type());
-      const exprt operand=get_value(expr.type(), rhs, offset);
-      offset+=size;
+      mp_integer size=get_size(expr.type());
+      const exprt operand=get_value(expr.type(), rhs, tmp_offset);
+      tmp_offset+=size;
       result.copy_to_operands(operand);
     }
     return result;
@@ -546,22 +551,21 @@ exprt interpretert::get_value(
     const exprt &size_expr=static_cast<const exprt &>(type.find(ID_size));
 
     // Get size of array
-    size_t subtype_size=get_size(type.subtype());
-    unsigned count;
+    mp_integer subtype_size=get_size(type.subtype());
+
+    mp_integer count;
     if(unbounded_size(type))
     {
       count=base_address_to_actual_size(offset)/subtype_size;
     }
     else
     {
-      mp_integer mp_count;
-      to_integer(size_expr, mp_count);
-      count=integer2unsigned(mp_count);
+      to_integer(size_expr, count);
     }
 
     // Retrieve the value for each member in the array
-    result.reserve_operands(count);
-    for(unsigned i=0; i<count; i++)
+    result.reserve_operands(integer2size_t(count));
+    for(mp_integer i=0; i<count; ++i)
     {
       const exprt operand=get_value(type.subtype(), rhs,
           offset+i*subtype_size);
@@ -572,29 +576,29 @@ exprt interpretert::get_value(
   else if(real_type.id()==ID_floatbv)
   {
     ieee_floatt f(to_floatbv_type(type));
-    f.unpack(rhs[offset]);
+    f.unpack(rhs[integer2size_t(offset)]);
     return f.to_expr();
   }
   else if(real_type.id()==ID_fixedbv)
   {
     fixedbvt f;
-    f.from_integer(rhs[offset]);
+    f.from_integer(rhs[integer2size_t(offset)]);
     return f.to_expr();
   }
   else if(real_type.id()==ID_bool)
   {
-    if(rhs[offset]!=0)
+    if(rhs[integer2size_t(offset)]!=0)
       return true_exprt();
     else
       false_exprt();
   }
   else if(real_type.id()==ID_c_bool)
   {
-    return from_integer(rhs[offset]!=0?1:0, type);
+    return from_integer(rhs[integer2size_t(offset)]!=0?1:0, type);
   }
   else if((real_type.id()==ID_pointer) || (real_type.id()==ID_address_of))
   {
-    if(rhs[offset]==0)
+    if(rhs[integer2size_t(offset)]==0)
     {
       // NULL pointer
       constant_exprt result(type);
@@ -602,12 +606,12 @@ exprt interpretert::get_value(
       return result;
     }
 
-    if(rhs[offset]<memory.size())
+    if(rhs[integer2size_t(offset)]<memory.size())
     {
       // We want the symbol pointed to
-      std::size_t address=integer2size_t(rhs[offset]);
+      mp_integer address=rhs[integer2size_t(offset)];
       irep_idt identifier=address_to_identifier(address);
-      size_t offset=address_to_offset(address);
+      mp_integer offset=address_to_offset(address);
       const typet type=get_type(identifier);
       exprt symbol_expr(ID_symbol, type);
       symbol_expr.set(ID_identifier, identifier);
@@ -629,19 +633,21 @@ exprt interpretert::get_value(
       return index_expr;
     }
 
-    error() << "interpreter: invalid pointer " << rhs[offset]
+    error() << "interpreter: invalid pointer " << rhs[integer2size_t(offset)]
             << " > object count " << memory.size() << eom;
+
     throw "interpreter: reading from invalid pointer";
   }
   else if(real_type.id()==ID_string)
   {
     // Strings are currently encoded by their irep_idt ID.
     return constant_exprt(
-      irep_idt::make_from_table_index(rhs[offset].to_long()),
+      irep_idt::make_from_table_index(rhs[integer2size_t(offset)].to_long()),
       type);
   }
+
   // Retrieve value of basic data type
-  return from_integer(rhs[offset], type);
+  return from_integer(rhs[integer2ulong(offset)], type);
 }
 
 /// executes the assign statement at the current pc value
@@ -656,7 +662,7 @@ void interpretert::execute_assign()
   if(!rhs.empty())
   {
     mp_integer address=evaluate_address(code_assign.lhs());
-    size_t size=get_size(code_assign.lhs().type());
+    mp_integer size=get_size(code_assign.lhs().type());
 
     if(size!=rhs.size())
       error() << "!! failed to obtain rhs ("
@@ -684,11 +690,15 @@ void interpretert::execute_assign()
     side_effect_exprt side_effect=to_side_effect_expr(code_assign.rhs());
     if(side_effect.get_statement()==ID_nondet)
     {
-      unsigned address=integer2unsigned(evaluate_address(code_assign.lhs()));
-      size_t size=get_size(code_assign.lhs().type());
-      for(size_t i=0; i<size; i++)
+      mp_integer address=
+        integer2size_t(evaluate_address(code_assign.lhs()));
+
+      mp_integer size=
+        get_size(code_assign.lhs().type());
+
+      for(mp_integer i=0; i<size; ++i)
       {
-        memory[address+i].initialized=
+        memory[integer2ulong(address+i)].initialized=
           memory_cellt::initializedt::READ_BEFORE_WRITTEN;
       }
     }
@@ -700,20 +710,21 @@ void interpretert::assign(
   const mp_integer &address,
   const mp_vectort &rhs)
 {
-  for(size_t i=0; i<rhs.size(); i++)
+  for(mp_integer i=0; i<rhs.size(); ++i)
   {
     if((address+i)<memory.size())
     {
-      std::size_t address_val=integer2size_t(address+i);
-      memory_cellt &cell=memory[address_val];
+      mp_integer address_val=address+i;
+      memory_cellt &cell=memory[integer2ulong(address_val)];
       if(show)
       {
         status() << total_steps << " ** assigning "
                  << address_to_identifier(address_val) << "["
-                 << address_to_offset(address_val) << "]:=" << rhs[i]
+                 << address_to_offset(address_val) << "]:="
+                 << rhs[integer2size_t(i)]
                  << "\n" << eom;
       }
-      cell.value=rhs[i];
+      cell.value=rhs[integer2size_t(i)];
       if(cell.initialized==memory_cellt::initializedt::UNKNOWN)
         cell.initialized=memory_cellt::initializedt::WRITTEN_BEFORE_READ;
     }
@@ -744,17 +755,16 @@ void interpretert::execute_function_call()
     to_code_function_call(pc->code);
 
   // function to be called
-  mp_integer a=evaluate_address(function_call.function());
+  mp_integer address=evaluate_address(function_call.function());
 
-  if(a==0)
+  if(address==0)
     throw "function call to NULL";
-  else if(a>=memory.size())
+  else if(address>=memory.size())
     throw "out-of-range function call";
 
   // Retrieve the empty last trace step struct we pushed for this step
   // of the interpreter run to fill it with the corresponding data
   goto_trace_stept &trace_step=steps.get_last_step();
-  std::size_t address=integer2size_t(a);
 #if 0
   const memory_cellt &cell=memory[address];
 #endif
@@ -803,7 +813,7 @@ void interpretert::execute_function_call()
     for(const auto &id : locals)
     {
       const symbolt &symbol=ns.lookup(id);
-      frame.local_map[id]=integer2unsigned(build_memory_map(id, symbol.type));
+      frame.local_map[id]=build_memory_map(id, symbol.type);
     }
 
     // assign the arguments
@@ -813,7 +823,7 @@ void interpretert::execute_function_call()
     if(argument_values.size()<parameters.size())
       throw "not enough arguments";
 
-    for(size_t i=0; i<parameters.size(); i++)
+    for(std::size_t i=0; i<parameters.size(); i++)
     {
       const code_typet::parametert &a=parameters[i];
       exprt symbol_expr(ID_symbol, a.type());
@@ -867,7 +877,7 @@ void interpretert::build_memory_map()
 
 void interpretert::build_memory_map(const symbolt &symbol)
 {
-  size_t size=0;
+  mp_integer size=0;
 
   if(symbol.type.id()==ID_code)
   {
@@ -880,8 +890,8 @@ void interpretert::build_memory_map(const symbolt &symbol)
 
   if(size!=0)
   {
-    std::size_t address=memory.size();
-    memory.resize(address+size);
+    mp_integer address=memory.size();
+    memory.resize(integer2ulong(address+size));
     memory_map[symbol.name]=address;
     inverse_memory_map[address]=symbol.name;
   }
@@ -920,13 +930,13 @@ mp_integer interpretert::build_memory_map(
   const typet &type)
 {
   typet alloc_type=concretize_type(type);
-  size_t size=get_size(alloc_type);
+  mp_integer size=get_size(alloc_type);
   auto it=dynamic_types.find(id);
 
   if(it!=dynamic_types.end())
   {
-    std::size_t address=memory_map[id];
-    std::size_t current_size=base_address_to_alloc_size(address);
+    mp_integer address=memory_map[id];
+    mp_integer current_size=base_address_to_alloc_size(address);
     // current size <= size already recorded
     if(size<=current_size)
       return memory_map[id];
@@ -938,8 +948,8 @@ mp_integer interpretert::build_memory_map(
   if(size==0)
     size=1; // This is a hack to create existence
 
-  std::size_t address=memory.size();
-  memory.resize(address+size);
+  mp_integer address=memory.size();
+  memory.resize(integer2ulong(address+size));
   memory_map[id]=address;
   inverse_memory_map[address]=id;
   dynamic_types.insert(std::pair<const irep_idt, typet>(id, alloc_type));
@@ -970,17 +980,17 @@ bool interpretert::unbounded_size(const typet &type)
 /// get allocated 2^32 address space each (of a 2^64 sized space).
 /// \param type: a structured type
 /// \return Size of the given type
-size_t interpretert::get_size(const typet &type)
+mp_integer interpretert::get_size(const typet &type)
 {
   if(unbounded_size(type))
-    return 2ULL << 32ULL;
+    return mp_integer(2) << 32;
 
   if(type.id()==ID_struct)
   {
     const struct_typet::componentst &components=
       to_struct_type(type).components();
 
-    unsigned sum=0;
+    mp_integer sum=0;
 
     for(const auto &comp : components)
     {
@@ -997,7 +1007,7 @@ size_t interpretert::get_size(const typet &type)
     const union_typet::componentst &components=
       to_union_type(type).components();
 
-    size_t max_size=0;
+    mp_integer max_size=0;
 
     for(const auto &comp : components)
     {
@@ -1013,7 +1023,7 @@ size_t interpretert::get_size(const typet &type)
   {
     const exprt &size_expr=static_cast<const exprt &>(type.find(ID_size));
 
-    size_t subtype_size=get_size(type.subtype());
+    mp_integer subtype_size=get_size(type.subtype());
 
     mp_vectort i;
     evaluate(size_expr, i);
@@ -1025,7 +1035,7 @@ size_t interpretert::get_size(const typet &type)
       mp_integer size_mp;
       bool ret=to_integer(size_const, size_mp);
       CHECK_RETURN(!ret);
-      return subtype_size*integer2unsigned(size_mp);
+      return subtype_size*size_mp;
     }
     return subtype_size;
   }
@@ -1051,7 +1061,7 @@ exprt interpretert::get_value(const irep_idt &id)
   symbol_exprt symbol_expr(id, get_type);
   mp_integer whole_lhs_object_address=evaluate_address(symbol_expr);
 
-  return get_value(get_type, integer2size_t(whole_lhs_object_address));
+  return get_value(get_type, whole_lhs_object_address);
 }
 
 /// Prints the current state of the memory map Since messaget mdofifies class
@@ -1060,7 +1070,7 @@ void interpretert::print_memory(bool input_flags)
 {
   for(const auto &cell_address : memory)
   {
-    std::size_t i=cell_address.first;
+    mp_integer i=cell_address.first;
     const memory_cellt &cell=cell_address.second;
     const auto identifier=address_to_identifier(i);
     const auto offset=address_to_offset(i);
diff --git a/src/goto-programs/interpreter_class.h b/src/goto-programs/interpreter_class.h
index e26d4911b02..a3dbd316f9b 100644
--- a/src/goto-programs/interpreter_class.h
+++ b/src/goto-programs/interpreter_class.h
@@ -104,13 +104,13 @@ class interpretert:public messaget
 
   const goto_functionst &goto_functions;
 
-  typedef std::unordered_map<irep_idt, std::size_t, irep_id_hash> memory_mapt;
-  typedef std::map<std::size_t, irep_idt> inverse_memory_mapt;
+  typedef std::unordered_map<irep_idt, mp_integer, irep_id_hash> memory_mapt;
+  typedef std::map<mp_integer, irep_idt> inverse_memory_mapt;
   memory_mapt memory_map;
   inverse_memory_mapt inverse_memory_map;
 
   const inverse_memory_mapt::value_type &address_to_object_record(
-    std::size_t address) const
+    const mp_integer &address) const
   {
     auto lower_bound=inverse_memory_map.lower_bound(address);
     if(lower_bound->first!=address)
@@ -121,34 +121,34 @@ class interpretert:public messaget
     return *lower_bound;
   }
 
-  irep_idt address_to_identifier(std::size_t address) const
+  irep_idt address_to_identifier(const mp_integer &address) const
   {
     return address_to_object_record(address).second;
   }
 
-  std::size_t address_to_offset(std::size_t address) const
+  mp_integer address_to_offset(const mp_integer &address) const
   {
     return address-(address_to_object_record(address).first);
   }
 
-  std::size_t base_address_to_alloc_size(std::size_t address) const
+  mp_integer base_address_to_alloc_size(const mp_integer &address) const
   {
     PRECONDITION(address_to_offset(address)==0);
     auto upper_bound=inverse_memory_map.upper_bound(address);
-    std::size_t next_alloc_address=
+    mp_integer next_alloc_address=
       upper_bound==inverse_memory_map.end() ?
       memory.size() :
       upper_bound->first;
     return next_alloc_address-address;
   }
 
-  std::size_t base_address_to_actual_size(std::size_t address) const
+  mp_integer base_address_to_actual_size(const mp_integer &address) const
   {
-    auto memory_iter=memory.find(address);
+    auto memory_iter=memory.find(integer2ulong(address));
     if(memory_iter==memory.end())
       return 0;
-    std::size_t ret=0;
-    std::size_t alloc_size=base_address_to_alloc_size(address);
+    mp_integer ret=0;
+    mp_integer alloc_size=base_address_to_alloc_size(address);
     while(memory_iter!=memory.end() && memory_iter->first<(address+alloc_size))
     {
       ++ret;
@@ -187,25 +187,31 @@ class interpretert:public messaget
   //  properties need to be mutable to avoid making all calls nonconst
   mutable memoryt memory;
 
-  std::size_t stack_pointer;
+  mp_integer stack_pointer;
 
   void build_memory_map();
   void build_memory_map(const symbolt &symbol);
   mp_integer build_memory_map(const irep_idt &id, const typet &type);
   typet concretize_type(const typet &type);
   bool unbounded_size(const typet &);
-  size_t get_size(const typet &type);
+  mp_integer get_size(const typet &type);
 
   struct_typet::componentt get_component(
     const irep_idt &object,
-    unsigned offset);
+    const mp_integer &offset);
 
   typet get_type(const irep_idt &id) const;
+
   exprt get_value(
     const typet &type,
-    std::size_t offset=0,
+    const mp_integer &offset=0,
     bool use_non_det=false);
-  exprt get_value(const typet &type, mp_vectort &rhs, std::size_t offset=0);
+
+  exprt get_value(
+    const typet &type,
+    mp_vectort &rhs,
+    const mp_integer &offset=0);
+
   exprt get_value(const irep_idt &id);
 
   void step();
@@ -221,7 +227,7 @@ class interpretert:public messaget
 
   void allocate(
     const mp_integer &address,
-    size_t size);
+    const mp_integer &size);
 
   void assign(
     const mp_integer &address,
@@ -244,7 +250,7 @@ class interpretert:public messaget
     goto_functionst::function_mapt::const_iterator return_function;
     mp_integer return_value_address;
     memory_mapt local_map;
-    unsigned old_stack_pointer;
+    mp_integer old_stack_pointer;
   };
 
   typedef std::stack<stack_framet> call_stackt;
@@ -265,7 +271,7 @@ class interpretert:public messaget
 
   dynamic_typest dynamic_types;
   int num_dynamic_objects;
-  size_t stack_depth;
+  mp_integer stack_depth;
   int thread_id;
 
   bool evaluate_boolean(const exprt &expr)
diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp
index 81d3fd33527..72c1429d2aa 100644
--- a/src/goto-programs/interpreter_evaluate.cpp
+++ b/src/goto-programs/interpreter_evaluate.cpp
@@ -28,13 +28,13 @@ void interpretert::read(
   mp_vectort &dest) const
 {
   // copy memory region
-  for(size_t i=0; i<dest.size(); i++)
+  for(std::size_t i=0; i<dest.size(); ++i)
   {
     mp_integer value;
 
     if((address+i)<memory.size())
     {
-      const memory_cellt &cell=memory[integer2size_t(address+i)];
+      const memory_cellt &cell=memory[integer2ulong(address+i)];
       value=cell.value;
       if(cell.initialized==memory_cellt::initializedt::UNKNOWN)
         cell.initialized=memory_cellt::initializedt::READ_BEFORE_WRITTEN;
@@ -52,10 +52,10 @@ void interpretert::read_unbounded(
 {
   // copy memory region
   std::size_t address_val=integer2size_t(address);
-  const std::size_t offset=address_to_offset(address_val);
-  const std::size_t alloc_size=
+  const mp_integer offset=address_to_offset(address_val);
+  const mp_integer alloc_size=
     base_address_to_actual_size(address_val-offset);
-  const std::size_t to_read=alloc_size-offset;
+  const mp_integer to_read=alloc_size-offset;
   for(size_t i=0; i<to_read; i++)
   {
     mp_integer value;
@@ -77,14 +77,14 @@ void interpretert::read_unbounded(
 /// reserves memory block of size at address
 void interpretert::allocate(
   const mp_integer &address,
-  size_t size)
+  const mp_integer &size)
 {
   // clear memory region
-  for(size_t i=0; i<size; i++)
+  for(mp_integer i=0; i<size; ++i)
   {
     if((address+i)<memory.size())
     {
-      memory_cellt &cell=memory[integer2size_t(address+i)];
+      memory_cellt &cell=memory[integer2ulong(address+i)];
       cell.value=0;
       cell.initialized=memory_cellt::initializedt::UNKNOWN;
     }
@@ -307,7 +307,7 @@ void interpretert::evaluate(
   {
     if(expr.type().id()==ID_struct)
     {
-      dest.reserve(get_size(expr.type()));
+      dest.reserve(integer2size_t(get_size(expr.type())));
       bool error=false;
 
       forall_operands(it, expr)
@@ -315,7 +315,7 @@ void interpretert::evaluate(
         if(it->type().id()==ID_code)
           continue;
 
-        size_t sub_size=get_size(it->type());
+        mp_integer sub_size=get_size(it->type());
         if(sub_size==0)
           continue;
 
@@ -324,7 +324,7 @@ void interpretert::evaluate(
 
         if(tmp.size()==sub_size)
         {
-          for(size_t i=0; i<sub_size; i++)
+          for(std::size_t i=0; i<tmp.size(); ++i)
             dest.push_back(tmp[i]);
         }
         else
@@ -380,7 +380,7 @@ void interpretert::evaluate(
     {
       irep_idt value=to_constant_expr(expr).get_value();
       const char *str=value.c_str();
-      size_t length=strlen(str)+1;
+      std::size_t length=strlen(str)+1;
       if(show)
         warning() << "string decoding not fully implemented "
                   << length << eom;
@@ -401,7 +401,8 @@ void interpretert::evaluate(
   else if(expr.id()==ID_struct)
   {
     if(!unbounded_size(expr.type()))
-      dest.reserve(get_size(expr.type()));
+      dest.reserve(integer2size_t(get_size(expr.type())));
+
     bool error=false;
 
     forall_operands(it, expr)
@@ -409,7 +410,7 @@ void interpretert::evaluate(
       if(it->type().id()==ID_code)
         continue;
 
-      size_t sub_size=get_size(it->type());
+      mp_integer sub_size=get_size(it->type());
       if(sub_size==0)
         continue;
 
@@ -418,7 +419,7 @@ void interpretert::evaluate(
 
       if(unbounded_size(it->type()) || tmp.size()==sub_size)
       {
-        for(size_t i=0; i<tmp.size(); i++)
+        for(std::size_t i=0; i<tmp.size(); i++)
           dest.push_back(tmp[i]);
       }
       else
@@ -852,10 +853,9 @@ void interpretert::evaluate(
       mp_integer address=result[0];
       if(address>0 && address<memory.size())
       {
-        std::size_t address_val=integer2size_t(address);
-        auto obj_type=get_type(address_to_identifier(address_val));
+        auto obj_type=get_type(address_to_identifier(address));
 
-        mp_integer offset=address_to_offset(address_val);
+        mp_integer offset=address_to_offset(address);
         mp_integer byte_offset;
         if(!memory_offset_to_byte_offset(obj_type, offset, byte_offset))
           dest.push_back(byte_offset);
@@ -954,7 +954,7 @@ void interpretert::evaluate(
     {
       if(!unbounded_size(expr.type()))
       {
-        dest.resize(get_size(expr.type()));
+        dest.resize(integer2size_t(get_size(expr.type())));
         read(address, dest);
       }
       else
@@ -1018,6 +1018,7 @@ void interpretert::evaluate(
       size.push_back(0);
     else
       evaluate(ty.size(), size);
+
     if(size.size()==1)
     {
       std::size_t size_int=integer2size_t(size[0]);
@@ -1040,13 +1041,17 @@ void interpretert::evaluate(
       // Ignore indices < 0, which the string solver sometimes produces
       if(where[0]<0)
         return;
-      std::size_t where_idx=integer2size_t(where[0]);
-      std::size_t subtype_size=get_size(subtype);
-      std::size_t need_size=(where_idx+1)*subtype_size;
+
+      mp_integer where_idx=where[0];
+      mp_integer subtype_size=get_size(subtype);
+      mp_integer need_size=(where_idx+1)*subtype_size;
+
       if(dest.size()<need_size)
-        dest.resize(need_size, 0);
+        dest.resize(integer2size_t(need_size), 0);
+
       for(std::size_t i=0; i<new_value.size(); ++i)
-        dest[(where_idx*subtype_size)+i]=new_value[i];
+        dest[integer2size_t((where_idx*subtype_size)+i)]=new_value[i];
+
       return;
     }
   }
@@ -1135,7 +1140,7 @@ mp_integer interpretert::evaluate_address(
     const irep_idt &component_name=
       to_member_expr(expr).get_component_name();
 
-    unsigned offset=0;
+    mp_integer offset=0;
 
     for(const auto &comp : struct_type.components())
     {