diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp
index 8d1565db914..ff61e53b615 100644
--- a/src/goto-programs/interpreter.cpp
+++ b/src/goto-programs/interpreter.cpp
@@ -597,16 +597,25 @@ exprt interpretert::get_value(
     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());
-    mp_integer mp_count;
-    to_integer(size_expr, mp_count);
-    unsigned count=integer2unsigned(mp_count);
+    std::size_t 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);
+    }
 
     // Retrieve the value for each member in the array
     result.reserve_operands(count);
     for(unsigned i=0; i<count; i++)
     {
-      const exprt operand=get_value(type.subtype(),
-          offset+i*subtype_size);
+      const exprt operand=get_value(
+        type.subtype(),
+        offset+i*subtype_size);
       result.copy_to_operands(operand);
     }
     return result;
@@ -663,9 +672,17 @@ exprt interpretert::get_value(
 
     // Get size of array
     size_t subtype_size=get_size(type.subtype());
-    mp_integer mp_count;
-    to_integer(size_expr, mp_count);
-    unsigned count=integer2unsigned(mp_count);
+    unsigned 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);
+    }
 
     // Retrieve the value for each member in the array
     result.reserve_operands(count);
@@ -712,22 +729,24 @@ exprt interpretert::get_value(
     if(rhs[offset]<memory.size())
     {
       // We want the symbol pointed to
-      memory_cellt &cell=memory[integer2unsigned(rhs[offset])];
-      const typet type=get_type(cell.identifier);
+      std::size_t address=integer2size_t(rhs[offset]);
+      irep_idt identifier=address_to_identifier(address);
+      size_t offset=address_to_offset(address);
+      const typet type=get_type(identifier);
       exprt symbol_expr(ID_symbol, type);
-      symbol_expr.set(ID_identifier, cell.identifier);
+      symbol_expr.set(ID_identifier, identifier);
 
-      if(cell.offset==0)
+      if(offset==0)
         return address_of_exprt(symbol_expr);
       if(ns.follow(type).id()==ID_struct)
       {
-        irep_idt member_id=get_component_id(cell.identifier, cell.offset);
+        irep_idt member_id=get_component_id(identifier, offset);
         member_exprt member_expr(symbol_expr, member_id);
         return address_of_exprt(member_expr);
       }
       index_exprt index_expr(
         symbol_expr,
-        from_integer(cell.offset, integer_typet()));
+        from_integer(offset, integer_typet()));
       return index_expr;
     }
 
@@ -828,12 +847,13 @@ void interpretert::assign(
   {
     if((address+i)<memory.size())
     {
-      memory_cellt &cell=memory[integer2unsigned(address+i)];
+      std::size_t address_val=integer2size_t(address+i);
+      memory_cellt &cell=memory[address_val];
       if(show)
       {
         status() << total_steps << " ** assigning "
-                 << cell.identifier << "["
-                 << cell.offset << "]:=" << rhs[i]
+                 << address_to_identifier(address_val) << "["
+                 << address_to_offset(address_val) << "]:=" << rhs[i]
                  << "\n" << eom;
       }
       cell.value=rhs[i];
@@ -913,8 +933,11 @@ void interpretert::execute_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();
-  const memory_cellt &cell=memory[integer2size_t(a)];
-  const irep_idt &identifier=cell.identifier;
+  std::size_t address=integer2size_t(a);
+#if 0
+  const memory_cellt &cell=memory[address];
+#endif
+  const irep_idt &identifier=address_to_identifier(address);
   trace_step.identifier=identifier;
 
   const goto_functionst::function_mapt::const_iterator f_it=
@@ -1020,9 +1043,7 @@ void interpretert::build_memory_map()
 {
   // put in a dummy for NULL
   memory.resize(1);
-  memory[0].offset=0;
-  memory[0].identifier="NULL-OBJECT";
-  memory[0].initialized=0;
+  inverse_memory_map[0]="NULL-OBJECT";
 
   num_dynamic_objects=0;
   dynamic_types.clear();
@@ -1062,18 +1083,10 @@ void interpretert::build_memory_map(const symbolt &symbol)
 
   if(size!=0)
   {
-    unsigned address=memory.size();
+    std::size_t address=memory.size();
     memory.resize(address+size);
     memory_map[symbol.name]=address;
-
-    for(size_t i=0; i<size; i++)
-    {
-      memory_cellt &cell=memory[address+i];
-      cell.identifier=symbol.name;
-      cell.offset=i;
-      cell.value=0;
-      cell.initialized=0;
-    }
+    inverse_memory_map[address]=symbol.name;
   }
 }
 
@@ -1119,7 +1132,7 @@ Function: interpretert::build_memory_map
 
   Inputs:
 
- Outputs: Updtaes the memory map to include variable id if it does
+ Outputs: Updates the memory map to include variable id if it does
           not exist
 
  Purpose: Populates dynamic entries of the memory map
@@ -1136,12 +1149,10 @@ mp_integer interpretert::build_memory_map(
 
   if(it!=dynamic_types.end())
   {
-    unsigned offset=1;
-    unsigned address=memory_map[id];
-    while(memory[address+offset].offset>0) offset++;
-
+    std::size_t address=memory_map[id];
+    std::size_t current_size=base_address_to_alloc_size(address);
     // current size <= size already recorded
-    if(size<=offset)
+    if(size<=current_size)
       return memory_map[id];
   }
 
@@ -1151,20 +1162,32 @@ mp_integer interpretert::build_memory_map(
   if(size==0)
     size=1; // This is a hack to create existence
 
-  unsigned address=memory.size();
+  std::size_t address=memory.size();
   memory.resize(address+size);
   memory_map[id]=address;
+  inverse_memory_map[address]=id;
   dynamic_types.insert(std::pair<const irep_idt, typet>(id, alloc_type));
 
-  for(size_t i=0; i<size; i++)
+  return address;
+}
+
+bool interpretert::unbounded_size(const typet &type)
+{
+  if(type.id()==ID_array)
   {
-    memory_cellt &cell=memory[address+i];
-    cell.identifier=id;
-    cell.offset=i;
-    cell.value=0;
-    cell.initialized=0;
+    const exprt &size=to_array_type(type).size();
+    if(size.id()==ID_infinity)
+      return true;
+    return unbounded_size(type.subtype());
   }
-  return address;
+  else if(type.id()==ID_struct)
+  {
+    const auto &st=to_struct_type(type);
+    if(st.components().empty())
+      return false;
+    return unbounded_size(st.components().back().type());
+  }
+  return false;
 }
 
 /*******************************************************************\
@@ -1172,15 +1195,21 @@ mp_integer interpretert::build_memory_map(
 Function: interpretert::get_size
 
   Inputs:
+    type - a structured type
 
- Outputs:
+ Outputs: Size of the given type
 
- Purpose: Retrieves the actual size of the provided structured type
+ Purpose: Retrieves the actual size of the provided structured type.
+          Unbounded objects get allocated 2^32 address space each
+          (of a 2^64 sized space).
 
 \*******************************************************************/
 
 size_t interpretert::get_size(const typet &type)
 {
+  if(unbounded_size(type))
+    return 2ULL << 32ULL;
+
   if(type.id()==ID_struct)
   {
     const struct_typet::componentst &components=
@@ -1268,7 +1297,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, integer2unsigned(whole_lhs_object_address));
+  return get_value(get_type, integer2size_t(whole_lhs_object_address));
 }
 
 /*******************************************************************\
@@ -1310,10 +1339,13 @@ Function: interpretert::print_memory
 
 void interpretert::print_memory(bool input_flags)
 {
-  for(size_t i=0; i<memory.size(); i++)
+  for(const auto &cell_address : memory)
   {
-    memory_cellt &cell=memory[i];
-    debug() << cell.identifier << "[" << cell.offset << "]"
+    std::size_t 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);
+    debug() << identifier << "[" << offset << "]"
             << "=" << cell.value << eom;
     if(input_flags)
       debug() << "(" << static_cast<int>(cell.initialized) << ")"
diff --git a/src/goto-programs/interpreter_class.h b/src/goto-programs/interpreter_class.h
index 83836eea072..8ea3ad620b2 100644
--- a/src/goto-programs/interpreter_class.h
+++ b/src/goto-programs/interpreter_class.h
@@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <stack>
 
 #include <util/arith_tools.h>
+#include <util/sparse_vector.h>
 
 #include "goto_functions.h"
 #include "goto_trace.h"
@@ -68,6 +69,9 @@ class interpretert:public messaget
   // List of dynamically allocated symbols that are not in the symbol table
   typedef std::map<irep_idt, typet> dynamic_typest;
 
+  typedef std::map<irep_idt, function_assignmentst> output_valuest;
+  output_valuest output_values;
+
   // An assignment list annotated with the calling context.
   struct function_assignments_contextt
   {
@@ -103,27 +107,78 @@ class interpretert:public messaget
 
   const goto_functionst &goto_functions;
 
-  typedef std::unordered_map<irep_idt, unsigned, irep_id_hash> memory_mapt;
+  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;
   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
+  {
+    auto lower_bound=inverse_memory_map.lower_bound(address);
+    if(lower_bound->first!=address)
+    {
+      assert(lower_bound!=inverse_memory_map.begin());
+      --lower_bound;
+    }
+    return *lower_bound;
+  }
+
+  irep_idt address_to_identifier(std::size_t address) const
+  {
+    return address_to_object_record(address).second;
+  }
+
+  std::size_t address_to_offset(std::size_t address) const
+  {
+    return address-(address_to_object_record(address).first);
+  }
+
+  std::size_t base_address_to_alloc_size(std::size_t address) const
+  {
+    assert(address_to_offset(address)==0);
+    auto upper_bound=inverse_memory_map.upper_bound(address);
+    std::size_t 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
+  {
+    auto memory_iter=memory.find(address);
+    if(memory_iter==memory.end())
+      return 0;
+    std::size_t ret=0;
+    std::size_t alloc_size=base_address_to_alloc_size(address);
+    while(memory_iter!=memory.end() && ret<alloc_size)
+    {
+      ++ret;
+      ++memory_iter;
+    }
+    return ret;
+  }
 
   class memory_cellt
   {
   public:
-    irep_idt identifier;
-    unsigned offset;
+    memory_cellt() :
+    value(0),
+    initialized(0)
+    {}
     mp_integer value;
     // Initialized is annotated even during reads
     // Set to 1 when written-before-read, -1 when read-before-written
     mutable char initialized;
   };
 
-  typedef std::vector<memory_cellt> memoryt;
+  typedef sparse_vectort<memory_cellt> memoryt;
   typedef std::map<std::string, const irep_idt &> parameter_sett;
   // mapping <structure, field> -> value
   typedef std::pair<const irep_idt, const irep_idt> struct_member_idt;
   typedef std::map<struct_member_idt, const exprt> struct_valuest;
 
-
   //  The memory is being annotated/reshaped even during reads
   //  (ie to find a read-before-write location) thus memory
   //  properties need to be mutable to avoid making all calls nonconst
@@ -135,6 +190,7 @@ class interpretert:public messaget
   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);
 
   irep_idt get_component_id(const irep_idt &object, unsigned offset);
@@ -169,6 +225,10 @@ class interpretert:public messaget
     mp_integer address,
     mp_vectort &dest) const;
 
+  void read_unbounded(
+    mp_integer address,
+    mp_vectort &dest) const;
+
   virtual void command();
 
   class stack_framet
diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp
index 712d4b9d807..f285328aedd 100644
--- a/src/goto-programs/interpreter_evaluate.cpp
+++ b/src/goto-programs/interpreter_evaluate.cpp
@@ -54,6 +54,34 @@ void interpretert::read(
   }
 }
 
+void interpretert::read_unbounded(
+  mp_integer address,
+  mp_vectort &dest) const
+{
+  // 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=
+    base_address_to_actual_size(address_val-offset);
+  const std::size_t to_read=alloc_size-offset;
+  for(size_t i=0; i<to_read; i++)
+  {
+    mp_integer value;
+
+    if((address+i)<memory.size())
+    {
+      const memory_cellt &cell=memory[integer2size_t(address+i)];
+      value=cell.value;
+      if(cell.initialized==0)
+        cell.initialized=-1;
+    }
+    else
+      value=0;
+
+    dest.push_back(value);
+  }
+}
+
 /*******************************************************************\
 
 Function: interpretert::allocate
@@ -96,10 +124,10 @@ Function: interpretert::clear_input_flags
 
 void interpretert::clear_input_flags()
 {
-  for(const memory_cellt &cell : memory)
+  for(auto &cell : memory)
   {
-    if(cell.initialized>0)
-      cell.initialized=0;
+    if(cell.second.initialized>0)
+      cell.second.initialized=0;
   }
 }
 
@@ -441,7 +469,8 @@ void interpretert::evaluate(
   }
   else if(expr.id()==ID_struct)
   {
-    dest.reserve(get_size(expr.type()));
+    if(!unbounded_size(expr.type()))
+      dest.reserve(get_size(expr.type()));
     bool error=false;
 
     forall_operands(it, expr)
@@ -456,9 +485,9 @@ void interpretert::evaluate(
       mp_vectort tmp;
       evaluate(*it, tmp);
 
-      if(tmp.size()==sub_size)
+      if(unbounded_size(it->type()) || tmp.size()==sub_size)
       {
-        for(size_t i=0; i<sub_size; i++)
+        for(size_t i=0; i<tmp.size(); i++)
           dest.push_back(tmp[i]);
       }
       else
@@ -892,10 +921,10 @@ void interpretert::evaluate(
       mp_integer address=result[0];
       if(address>0 && address<memory.size())
       {
-        const auto &memory_record=memory[integer2unsigned(address)];
-        auto obj_type=get_type(memory_record.identifier);
+        std::size_t address_val=integer2size_t(address);
+        auto obj_type=get_type(address_to_identifier(address_val));
 
-        mp_integer offset=memory_record.offset;
+        mp_integer offset=address_to_offset(address_val);
         mp_integer byte_offset;
         if(!memory_offset_to_byte_offset(obj_type, offset, byte_offset))
           dest.push_back(byte_offset);
@@ -990,8 +1019,15 @@ void interpretert::evaluate(
     }
     else if(!address.is_zero())
     {
-      dest.resize(get_size(expr.type()));
-      read(address, dest);
+      if(!unbounded_size(expr.type()))
+      {
+        dest.resize(get_size(expr.type()));
+        read(address, dest);
+      }
+      else
+      {
+        read_unbounded(address, dest);
+      }
       return;
     }
   }
@@ -1033,7 +1069,7 @@ void interpretert::evaluate(
       }
     }
   }
-  else if((expr.id()==ID_array) || (expr.id()==ID_array_of))
+  else if(expr.id()==ID_array)
   {
     forall_operands(it, expr)
     {
@@ -1041,6 +1077,46 @@ void interpretert::evaluate(
     }
     return;
   }
+  else if(expr.id()==ID_array_of)
+  {
+    const auto &ty=to_array_type(expr.type());
+    std::vector<mp_integer> size;
+    if(ty.size().id()==ID_infinity)
+      size.push_back(0);
+    else
+      evaluate(ty.size(), size);
+    if(size.size()==1)
+    {
+      std::size_t size_int=integer2size_t(size[0]);
+      for(std::size_t i=0; i<size_int; ++i)
+        evaluate(expr.op0(), dest);
+      return;
+    }
+  }
+  else if(expr.id()==ID_with)
+  {
+    const auto &wexpr=to_with_expr(expr);
+    evaluate(wexpr.old(), dest);
+    std::vector<mp_integer> where;
+    std::vector<mp_integer> new_value;
+    evaluate(wexpr.where(), where);
+    evaluate(wexpr.new_value(), new_value);
+    const auto &subtype=expr.type().subtype();
+    if(!new_value.empty() && where.size()==1 && !unbounded_size(subtype))
+    {
+      // 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;
+      if(dest.size()<need_size)
+        dest.resize(need_size, 0);
+      for(std::size_t i=0; i<new_value.size(); ++i)
+        dest[(where_idx*subtype_size)+i]=new_value[i];
+      return;
+    }
+  }
   else if(expr.id()==ID_nil)
   {
     dest.push_back(0);
diff --git a/src/util/sparse_vector.h b/src/util/sparse_vector.h
new file mode 100644
index 00000000000..6c4e050b323
--- /dev/null
+++ b/src/util/sparse_vector.h
@@ -0,0 +1,60 @@
+/*******************************************************************\
+
+Module: Sparse Vectors
+
+Author: Romain Brenguier
+
+\*******************************************************************/
+
+#ifndef CPROVER_UTIL_SPARSE_VECTOR_H
+#define CPROVER_UTIL_SPARSE_VECTOR_H
+
+#include<cstdint>
+
+template<class T> class sparse_vectort
+{
+protected:
+  typedef std::map<uint64_t, T> underlyingt;
+  underlyingt underlying;
+  uint64_t _size;
+
+public:
+  sparse_vectort() :
+    _size(0) {}
+
+  const T &operator[](uint64_t idx) const
+  {
+    assert(idx<_size && "index out of range");
+    return underlying[idx];
+  }
+
+  T &operator[](uint64_t idx)
+  {
+    assert(idx<_size && "index out of range");
+    return underlying[idx];
+  }
+
+  uint64_t size() const
+  {
+    return _size;
+  }
+
+  void resize(uint64_t new_size)
+  {
+    assert(new_size>=_size && "sparse vector can't be shrunk (yet)");
+    _size=new_size;
+  }
+
+  typedef typename underlyingt::iterator iteratort;
+  typedef typename underlyingt::const_iterator const_iteratort;
+
+  iteratort begin() { return underlying.begin(); }
+  const_iteratort begin() const { return underlying.begin(); }
+
+  iteratort end() { return underlying.end(); }
+  const_iteratort end() const { return underlying.end(); }
+
+  const_iteratort find(uint64_t idx) { return underlying.find(idx); }
+};
+
+#endif // CPROVER_UTIL_SPARSE_VECTOR_H