diff --git a/jbmc/src/java_bytecode/remove_exceptions.cpp b/jbmc/src/java_bytecode/remove_exceptions.cpp
index 4ac6aa5ae95..ce0b8277a35 100644
--- a/jbmc/src/java_bytecode/remove_exceptions.cpp
+++ b/jbmc/src/java_bytecode/remove_exceptions.cpp
@@ -89,10 +89,12 @@ class remove_exceptionst
     symbol_table_baset &_symbol_table,
     function_may_throwt _function_may_throw,
     bool remove_added_instanceof,
+    class_hierarchyt &class_hierarchy,
     message_handlert &message_handler)
     : symbol_table(_symbol_table),
       function_may_throw(_function_may_throw),
       remove_added_instanceof(remove_added_instanceof),
+      class_hierarchy(class_hierarchy),
       message_handler(message_handler)
   {
   }
@@ -104,6 +106,7 @@ class remove_exceptionst
   symbol_table_baset &symbol_table;
   function_may_throwt function_may_throw;
   bool remove_added_instanceof;
+  class_hierarchyt &class_hierarchy;
   message_handlert &message_handler;
 
   symbol_exprt get_inflight_exception_global();
@@ -345,7 +348,12 @@ void remove_exceptionst::add_exception_dispatch_sequence(
         t_exc->guard=check;
 
         if(remove_added_instanceof)
-          remove_instanceof(t_exc, goto_program, symbol_table, message_handler);
+          remove_instanceof(
+            t_exc,
+            goto_program,
+            symbol_table,
+            class_hierarchy,
+            message_handler);
       }
     }
   }
@@ -575,24 +583,26 @@ void remove_exceptionst::operator()(goto_programt &goto_program)
 
 /// removes throws/CATCH-POP/CATCH-PUSH
 void remove_exceptions(
-  symbol_table_baset &symbol_table,
-  goto_functionst &goto_functions,
+  goto_modelt &goto_model,
   message_handlert &message_handler,
   remove_exceptions_typest type)
 {
-  const namespacet ns(symbol_table);
+  const namespacet ns(goto_model.symbol_table);
   std::map<irep_idt, std::set<irep_idt>> exceptions_map;
-  uncaught_exceptions(goto_functions, ns, exceptions_map);
+  uncaught_exceptions(goto_model.goto_functions, ns, exceptions_map);
   remove_exceptionst::function_may_throwt function_may_throw =
     [&exceptions_map](const irep_idt &id) {
       return !exceptions_map[id].empty();
     };
+
   remove_exceptionst remove_exceptions(
-    symbol_table,
+    goto_model.symbol_table,
     function_may_throw,
     type == remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF,
+    goto_model.get_analysis_cache().get_or_create<class_hierarchyt>(
+      goto_model.symbol_table),
     message_handler);
-  remove_exceptions(goto_functions);
+  remove_exceptions(goto_model.goto_functions);
 }
 
 /// removes throws/CATCH-POP/CATCH-PUSH from a single GOTO program, replacing
@@ -601,37 +611,30 @@ void remove_exceptions(
 /// because we can't inspect other functions to determine whether they throw
 /// or not, and therefore must assume they do and always introduce post-call
 /// exception dispatch.
-/// \param goto_program: program to remove exceptions from
-/// \param symbol_table: global symbol table. The `@inflight_exception` global
-///   may be added if not already present. It will not be initialised; that is
-///   the caller's responsibility.
+/// \param goto_model_function: function to remove exceptions from.
+///   The `@inflight_exception` global may be added to its associated symbol
+///   table if not already present. It will not be initialised; that is the
+///   caller's responsibility.
 /// \param message_handler: logging output
 /// \param type: specifies whether instanceof operations generated by this pass
 ///   should be lowered to class-identifier comparisons (using
 ///   remove_instanceof).
 void remove_exceptions(
-  goto_programt &goto_program,
-  symbol_table_baset &symbol_table,
+  goto_model_functiont &goto_model_function,
   message_handlert &message_handler,
   remove_exceptions_typest type)
 {
   remove_exceptionst::function_may_throwt any_function_may_throw =
     [](const irep_idt &) { return true; };
 
+  auto &symbol_table = goto_model_function.get_symbol_table();
+
   remove_exceptionst remove_exceptions(
     symbol_table,
     any_function_may_throw,
     type == remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF,
+    goto_model_function.get_analysis_cache().get_or_create<class_hierarchyt>(
+      symbol_table),
     message_handler);
-  remove_exceptions(goto_program);
-}
-
-/// removes throws/CATCH-POP/CATCH-PUSH
-void remove_exceptions(
-  goto_modelt &goto_model,
-  message_handlert &message_handler,
-  remove_exceptions_typest type)
-{
-  remove_exceptions(
-    goto_model.symbol_table, goto_model.goto_functions, message_handler, type);
+  remove_exceptions(goto_model_function.get_goto_function().body);
 }
diff --git a/jbmc/src/java_bytecode/remove_exceptions.h b/jbmc/src/java_bytecode/remove_exceptions.h
index 7c0b364b67a..b18977dd162 100644
--- a/jbmc/src/java_bytecode/remove_exceptions.h
+++ b/jbmc/src/java_bytecode/remove_exceptions.h
@@ -32,8 +32,7 @@ enum class remove_exceptions_typest
 };
 
 void remove_exceptions(
-  goto_programt &goto_program,
-  symbol_table_baset &symbol_table,
+  goto_model_functiont &goto_model_function,
   message_handlert &message_handler,
   remove_exceptions_typest type =
     remove_exceptions_typest::DONT_REMOVE_INSTANCEOF);
diff --git a/jbmc/src/java_bytecode/remove_instanceof.cpp b/jbmc/src/java_bytecode/remove_instanceof.cpp
index dbacbac4a04..7b837afbf57 100644
--- a/jbmc/src/java_bytecode/remove_instanceof.cpp
+++ b/jbmc/src/java_bytecode/remove_instanceof.cpp
@@ -11,7 +11,6 @@ Author: Chris Smowton, chris.smowton@diffblue.com
 
 #include "remove_instanceof.h"
 
-#include <goto-programs/class_hierarchy.h>
 #include <goto-programs/class_identifier.h>
 #include <goto-programs/goto_convert.h>
 
@@ -24,12 +23,14 @@ class remove_instanceoft
 {
 public:
   remove_instanceoft(
-    symbol_table_baset &symbol_table, message_handlert &message_handler)
-    : symbol_table(symbol_table)
-    , ns(symbol_table)
-    , message_handler(message_handler)
+    symbol_table_baset &symbol_table,
+    const class_hierarchyt &class_hierarchy,
+    message_handlert &message_handler)
+    : symbol_table(symbol_table),
+      ns(symbol_table),
+      class_hierarchy(class_hierarchy),
+      message_handler(message_handler)
   {
-    class_hierarchy(symbol_table);
   }
 
   // Lower instanceof for a single function
@@ -41,7 +42,7 @@ class remove_instanceoft
 protected:
   symbol_table_baset &symbol_table;
   namespacet ns;
-  class_hierarchyt class_hierarchy;
+  const class_hierarchyt &class_hierarchy;
   message_handlert &message_handler;
 
   bool lower_instanceof(
@@ -245,44 +246,30 @@ void remove_instanceof(
   goto_programt::targett target,
   goto_programt &goto_program,
   symbol_table_baset &symbol_table,
+  const class_hierarchyt &class_hierarchy,
   message_handlert &message_handler)
 {
-  remove_instanceoft rem(symbol_table, message_handler);
+  remove_instanceoft rem(symbol_table, class_hierarchy, message_handler);
   rem.lower_instanceof(goto_program, target);
 }
 
 /// Replace every instanceof in the passed function with an explicit
 /// class-identifier test.
-/// \remarks Extra auxiliary variables may be introduced into symbol_table.
-/// \param function: The function to work on.
-/// \param symbol_table: The symbol table to add symbols to.
+/// \remarks Extra auxiliary variables may be introduced into
+///   goto_model_function's symbol_table.
+/// \param goto_model_function: The function to work on.
 /// \param message_handler: logging output
 void remove_instanceof(
-  goto_functionst::goto_functiont &function,
-  symbol_table_baset &symbol_table,
+  goto_model_functiont &goto_model_function,
   message_handlert &message_handler)
 {
-  remove_instanceoft rem(symbol_table, message_handler);
-  rem.lower_instanceof(function.body);
-}
+  symbol_table_baset &symbol_table = goto_model_function.get_symbol_table();
+  const class_hierarchyt &class_hierarchy(
+    goto_model_function.get_analysis_cache().get_or_create<class_hierarchyt>(
+      symbol_table));
 
-/// Replace every instanceof in every function with an explicit
-/// class-identifier test.
-/// \remarks Extra auxiliary variables may be introduced into symbol_table.
-/// \param goto_functions: The functions to work on.
-/// \param symbol_table: The symbol table to add symbols to.
-/// \param message_handler: logging output
-void remove_instanceof(
-  goto_functionst &goto_functions,
-  symbol_table_baset &symbol_table,
-  message_handlert &message_handler)
-{
-  remove_instanceoft rem(symbol_table, message_handler);
-  bool changed=false;
-  for(auto &f : goto_functions.function_map)
-    changed=rem.lower_instanceof(f.second.body) || changed;
-  if(changed)
-    goto_functions.compute_location_numbers();
+  remove_instanceoft rem(symbol_table, class_hierarchy, message_handler);
+  rem.lower_instanceof(goto_model_function.get_goto_function().body);
 }
 
 /// Replace every instanceof in every function with an explicit
@@ -295,6 +282,14 @@ void remove_instanceof(
   goto_modelt &goto_model,
   message_handlert &message_handler)
 {
-  remove_instanceof(
-    goto_model.goto_functions, goto_model.symbol_table, message_handler);
+  const class_hierarchyt &class_hierarchy(
+    goto_model.get_analysis_cache().get_or_create<class_hierarchyt>(
+      goto_model.symbol_table));
+  remove_instanceoft rem(
+    goto_model.symbol_table, class_hierarchy, message_handler);
+  bool changed=false;
+  for(auto &f : goto_model.goto_functions.function_map)
+    changed=rem.lower_instanceof(f.second.body) || changed;
+  if(changed)
+    goto_model.goto_functions.compute_location_numbers();
 }
diff --git a/jbmc/src/java_bytecode/remove_instanceof.h b/jbmc/src/java_bytecode/remove_instanceof.h
index f3a4c7f907e..dfc936a85a8 100644
--- a/jbmc/src/java_bytecode/remove_instanceof.h
+++ b/jbmc/src/java_bytecode/remove_instanceof.h
@@ -79,6 +79,7 @@ Author: Chris Smowton, chris.smowton@diffblue.com
 #ifndef CPROVER_JAVA_BYTECODE_REMOVE_INSTANCEOF_H
 #define CPROVER_JAVA_BYTECODE_REMOVE_INSTANCEOF_H
 
+#include <goto-programs/class_hierarchy.h>
 #include <goto-programs/goto_functions.h>
 #include <goto-programs/goto_model.h>
 
@@ -89,16 +90,15 @@ void remove_instanceof(
   goto_programt::targett target,
   goto_programt &goto_program,
   symbol_table_baset &symbol_table,
+  const class_hierarchyt &class_hierarchy,
   message_handlert &);
 
 void remove_instanceof(
-  goto_functionst::goto_functiont &function,
-  symbol_table_baset &symbol_table,
+  goto_model_functiont &goto_model_function,
   message_handlert &);
 
 void remove_instanceof(
-  goto_functionst &goto_functions,
-  symbol_table_baset &symbol_table,
+  goto_modelt &goto_model,
   message_handlert &);
 
 void remove_instanceof(goto_modelt &model, message_handlert &);
diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp
index 5a2a499eb07..35d79041fcb 100644
--- a/jbmc/src/jbmc/jbmc_parse_options.cpp
+++ b/jbmc/src/jbmc/jbmc_parse_options.cpp
@@ -702,7 +702,7 @@ void jbmc_parse_optionst::process_goto_function(
   try
   {
     // Removal of RTTI inspection:
-    remove_instanceof(goto_function, symbol_table, get_message_handler());
+    remove_instanceof(function, get_message_handler());
     // Java virtual functions -> explicit dispatch tables:
     remove_virtual_functions(function);
 
@@ -714,8 +714,7 @@ void jbmc_parse_optionst::process_goto_function(
       // the results are slightly worse than running it in whole-program mode
       // (e.g. dead catch sites will be retained)
       remove_exceptions(
-        goto_function.body,
-        symbol_table,
+        function,
         get_message_handler(),
         remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF);
     }
diff --git a/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp b/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp
index b5490499e3d..ca0912c4cf6 100644
--- a/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp
+++ b/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp
@@ -136,12 +136,17 @@ void load_and_test_method(
   goto_functionst::goto_functiont &goto_function =
     functions.function_map.at(function_name);
 
+  wrapper_goto_modelt goto_model(symbol_table, functions);
   goto_model_functiont model_function(
-    symbol_table, functions, function_name, goto_function);
+    symbol_table,
+    functions,
+    function_name,
+    goto_function,
+    goto_model.get_analysis_cache());
 
   // Emulate some of the passes that we'd normally do before replace_java_nondet
   // is called.
-  remove_instanceof(goto_function, symbol_table, null_message_handler);
+  remove_instanceof(model_function, null_message_handler);
 
   remove_virtual_functions(model_function);
 
@@ -292,4 +297,4 @@ SCENARIO(
     //      load_and_test_method("replaceNondetReturnUnboxed:()I", functions, symbol_table);
     //    }
   }
-}
\ No newline at end of file
+}
diff --git a/src/goto-programs/abstract_goto_model.h b/src/goto-programs/abstract_goto_model.h
index 6a244d837fe..eba5c9e45ca 100644
--- a/src/goto-programs/abstract_goto_model.h
+++ b/src/goto-programs/abstract_goto_model.h
@@ -13,6 +13,7 @@ Author: Diffblue Ltd.
 #define CPROVER_GOTO_PROGRAMS_ABSTRACT_GOTO_MODEL_H
 
 #include "goto_functions.h"
+#include <util/object_cache.h>
 #include <util/symbol_table.h>
 
 /// Abstract interface to eager or lazy GOTO models
@@ -49,6 +50,10 @@ class abstract_goto_modelt
   /// underneath them, so this should only be used to lend a reference to code
   /// that cannot also call get_goto_function.
   virtual const symbol_tablet &get_symbol_table() const = 0;
+
+  /// Accessor to get the analysis cache. Caches heavy-to-build data structures
+  /// in a place that can be accessible from any pass.
+  virtual object_cachet &get_analysis_cache() = 0;
 };
 
 #endif
diff --git a/src/goto-programs/class_hierarchy.h b/src/goto-programs/class_hierarchy.h
index ed4c25f4783..d17048c60d1 100644
--- a/src/goto-programs/class_hierarchy.h
+++ b/src/goto-programs/class_hierarchy.h
@@ -59,6 +59,13 @@ class class_hierarchyt
   class_hierarchyt() = default;
   class_hierarchyt(const class_hierarchyt &) = delete;
   class_hierarchyt &operator=(const class_hierarchyt &) = delete;
+  class_hierarchyt(class_hierarchyt &&) = default;
+  class_hierarchyt &operator=(class_hierarchyt &&) = default;
+
+  explicit class_hierarchyt(const symbol_tablet &symbol_table)
+  {
+    (*this)(symbol_table);
+  }
 
   // transitively gets all children
   idst get_children_trans(const irep_idt &id) const
diff --git a/src/goto-programs/goto_model.h b/src/goto-programs/goto_model.h
index aea03ae86da..172e8505173 100644
--- a/src/goto-programs/goto_model.h
+++ b/src/goto-programs/goto_model.h
@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/symbol_table.h>
 #include <util/journalling_symbol_table.h>
+#include <util/object_cache.h>
 
 #include "abstract_goto_model.h"
 #include "goto_functions.h"
@@ -31,6 +32,10 @@ class goto_modelt : public abstract_goto_modelt
   /// interface instead if possible.
   goto_functionst goto_functions;
 
+  // Object that holds all data that should be persistent between passes.
+  // Usually holds objects that are heavy to create but light to update.
+  object_cachet analysis_cache;
+
   void clear()
   {
     symbol_table.clear();
@@ -51,9 +56,10 @@ class goto_modelt : public abstract_goto_modelt
   //  explicitly (see https://msdn.microsoft.com/en-us/library/hh567368.aspx
   //  under "Defaulted and Deleted Functions")
 
-  goto_modelt(goto_modelt &&other):
-    symbol_table(std::move(other.symbol_table)),
-    goto_functions(std::move(other.goto_functions))
+  goto_modelt(goto_modelt &&other)
+    : symbol_table(std::move(other.symbol_table)),
+      goto_functions(std::move(other.goto_functions)),
+      analysis_cache(std::move(other.analysis_cache))
   {
   }
 
@@ -61,6 +67,7 @@ class goto_modelt : public abstract_goto_modelt
   {
     symbol_table=std::move(other.symbol_table);
     goto_functions=std::move(other.goto_functions);
+    analysis_cache = std::move(other.analysis_cache);
     return *this;
   }
 
@@ -78,6 +85,11 @@ class goto_modelt : public abstract_goto_modelt
     return symbol_table;
   }
 
+  object_cachet &get_analysis_cache() override
+  {
+    return analysis_cache;
+  }
+
   const goto_functionst::goto_functiont &get_goto_function(
     const irep_idt &id) override
   {
@@ -98,9 +110,10 @@ class wrapper_goto_modelt : public abstract_goto_modelt
 public:
   wrapper_goto_modelt(
     const symbol_tablet &symbol_table,
-    const goto_functionst &goto_functions) :
-    symbol_table(symbol_table),
-    goto_functions(goto_functions)
+    const goto_functionst &goto_functions)
+    : symbol_table(symbol_table),
+      goto_functions(goto_functions),
+      analysis_cache()
   {
   }
 
@@ -114,6 +127,11 @@ class wrapper_goto_modelt : public abstract_goto_modelt
     return symbol_table;
   }
 
+  object_cachet &get_analysis_cache() override
+  {
+    return analysis_cache;
+  }
+
   const goto_functionst::goto_functiont &get_goto_function(
     const irep_idt &id) override
   {
@@ -129,6 +147,7 @@ class wrapper_goto_modelt : public abstract_goto_modelt
 private:
   const symbol_tablet &symbol_table;
   const goto_functionst &goto_functions;
+  object_cachet analysis_cache;
 };
 
 /// Interface providing access to a single function in a GOTO model, plus its
@@ -150,11 +169,13 @@ class goto_model_functiont
     journalling_symbol_tablet &symbol_table,
     goto_functionst &goto_functions,
     const irep_idt &function_id,
-    goto_functionst::goto_functiont &goto_function):
-  symbol_table(symbol_table),
-  goto_functions(goto_functions),
-  function_id(function_id),
-  goto_function(goto_function)
+    goto_functionst::goto_functiont &goto_function,
+    object_cachet &analysis_cache)
+    : symbol_table(symbol_table),
+      goto_functions(goto_functions),
+      function_id(function_id),
+      goto_function(goto_function),
+      analysis_cache(analysis_cache)
   {
   }
 
@@ -196,11 +217,20 @@ class goto_model_functiont
     return function_id;
   }
 
+  /// Get the analysis_cache for the associated goto_model.
+  /// \return the pass manager used for all persistent data
+  ///   storage between passes.
+  object_cachet &get_analysis_cache()
+  {
+    return analysis_cache;
+  }
+
 private:
   journalling_symbol_tablet &symbol_table;
   goto_functionst &goto_functions;
   irep_idt function_id;
   goto_functionst::goto_functiont &goto_function;
+  object_cachet &analysis_cache;
 };
 
 #endif // CPROVER_GOTO_PROGRAMS_GOTO_MODEL_H
diff --git a/src/goto-programs/lazy_goto_model.cpp b/src/goto-programs/lazy_goto_model.cpp
index d2ccb487be6..c9179eee5d0 100644
--- a/src/goto-programs/lazy_goto_model.cpp
+++ b/src/goto-programs/lazy_goto_model.cpp
@@ -41,7 +41,8 @@ lazy_goto_modelt::lazy_goto_modelt(
           journalling_symbol_table,
           goto_model->goto_functions,
           function_name,
-          function);
+          function,
+          goto_model->analysis_cache);
         this->post_process_function(model_function, *this);
       },
       driver_program_can_generate_function_body,
@@ -74,7 +75,8 @@ lazy_goto_modelt::lazy_goto_modelt(lazy_goto_modelt &&other)
           journalling_symbol_table,
           goto_model->goto_functions,
           function_name,
-          function);
+          function,
+          goto_model->analysis_cache);
         this->post_process_function(model_function, *this);
       },
       other.driver_program_can_generate_function_body,
diff --git a/src/goto-programs/lazy_goto_model.h b/src/goto-programs/lazy_goto_model.h
index efba4c2dbce..45665a770a7 100644
--- a/src/goto-programs/lazy_goto_model.h
+++ b/src/goto-programs/lazy_goto_model.h
@@ -124,6 +124,11 @@ class lazy_goto_modelt : public abstract_goto_modelt
     return symbol_table;
   }
 
+  object_cachet &get_analysis_cache() override
+  {
+    return goto_model->analysis_cache;
+  }
+
   bool can_produce_function(const irep_idt &id) const override;
 
   const goto_functionst::goto_functiont &get_goto_function(const irep_idt &id)
diff --git a/src/util/object_cache.h b/src/util/object_cache.h
new file mode 100644
index 00000000000..e946b283ed6
--- /dev/null
+++ b/src/util/object_cache.h
@@ -0,0 +1,97 @@
+#ifndef CPROVER_GOTO_PROGRAMS_OBJECT_CACHE_H
+#define CPROVER_GOTO_PROGRAMS_OBJECT_CACHE_H
+
+#include <map>
+#include <memory>
+
+typedef void (*class_idt)();
+
+// This generates a static method for each template instantiation whose address
+// can be used as a unique key. We would use typeid(T) as such a key, but cbmc
+// may be built without RTTI.
+template <typename T>
+struct cached_type_idt
+{
+  static void id()
+  {
+  }
+};
+
+/// A cache of persistent objects.
+/// There can only be one instance of each type in the cache at a time.
+class object_cachet
+{
+public:
+  /// Retrives the current instance of the templated type if it exists in the cache,
+  /// creates it with the passed-in arguments and returns if not.
+  template <typename cached_type, typename... arguments>
+  cached_type &get_or_create(arguments &&... values)
+  {
+    // We're key'd off the current templates type.
+    const class_idt current_type_id = &cached_type_idt<cached_type>::id;
+    auto container_iterator = cache_map.find(current_type_id);
+    if(container_iterator == cache_map.end())
+    {
+      // This creates a new instance of the object we're caching, stores it in
+      // a container object in our map, then returns an iterator pointing at
+      // that element.
+      container_iterator =
+        cache_map
+          .emplace(
+            current_type_id,
+            std::unique_ptr<base_cache_containert>(
+              new cache_containert<cached_type>(
+                cached_type(std::forward<arguments>(values)...))))
+          .first;
+    }
+
+    return **static_cast<cache_containert<cached_type> *>(
+      container_iterator->second.get());
+  }
+
+  /// Erases the instance of the templated type from our cache.
+  template <typename cached_type>
+  void erase()
+  {
+    const class_idt current_type_id = &cached_type_idt<cached_type>::id;
+    cache_map.erase(current_type_id);
+  }
+
+  /// Clears the internal cache of all stored types.
+  void clear()
+  {
+    cache_map.clear();
+  }
+
+private:
+  /// Non-templated container base so we can have a map full of various
+  /// template instantiations.
+  class base_cache_containert
+  {
+  public:
+    virtual ~base_cache_containert() = default;
+  };
+
+  /// Templated container for persistent storage of heavy-to-create objects.
+  template <typename T>
+  class cache_containert : public base_cache_containert
+  {
+  private:
+    T cached_value;
+
+  public:
+    explicit cache_containert(T stored_value)
+      : cached_value(std::move(stored_value))
+    {
+    }
+
+    T &operator*()
+    {
+      return cached_value;
+    }
+  };
+
+  std::map<class_idt, std::unique_ptr<base_cache_containert>> cache_map;
+};
+
+#endif //CPROVER_GOTO_PROGRAMS_OBJECT_CACHE_H