diff --git a/src/util/journalling_symbol_table.h b/src/util/journalling_symbol_table.h
index 2b9893bb0b7..2fe3093d43d 100644
--- a/src/util/journalling_symbol_table.h
+++ b/src/util/journalling_symbol_table.h
@@ -124,6 +124,17 @@ class journalling_symbol_tablet : public symbol_table_baset
     base_symbol_table.clear();
   }
 
+  virtual iteratort begin() override
+  {
+    return iteratort(
+      base_symbol_table.begin(), [this](const irep_idt &id) { on_update(id); });
+  }
+  virtual iteratort end() override
+  {
+    return iteratort(
+      base_symbol_table.end(), [this](const irep_idt &id) { on_update(id); });
+  }
+
   const changesett &get_inserted() const
   {
     return inserted;
diff --git a/src/util/symbol_table.h b/src/util/symbol_table.h
index a9a083f5f4e..8bd7cf7d797 100644
--- a/src/util/symbol_table.h
+++ b/src/util/symbol_table.h
@@ -109,6 +109,15 @@ class symbol_tablet : public symbol_table_baset
     internal_symbol_base_map.clear();
     internal_symbol_module_map.clear();
   }
+
+  virtual iteratort begin() override
+  {
+    return iteratort(internal_symbols.begin());
+  }
+  virtual iteratort end() override
+  {
+    return iteratort(internal_symbols.end());
+  }
 };
 
 #endif // CPROVER_UTIL_SYMBOL_TABLE_H
diff --git a/src/util/symbol_table_base.h b/src/util/symbol_table_base.h
index 9b8327741e1..46ec91a061b 100644
--- a/src/util/symbol_table_base.h
+++ b/src/util/symbol_table_base.h
@@ -8,6 +8,7 @@
 #ifndef CPROVER_UTIL_SYMBOL_TABLE_BASE_H
 #define CPROVER_UTIL_SYMBOL_TABLE_BASE_H
 
+#include <functional>
 #include <iosfwd>
 #include <map>
 #include <unordered_map>
@@ -117,6 +118,78 @@ class symbol_table_baset
   virtual void clear() = 0;
 
   void show(std::ostream &out) const;
+
+  class iteratort
+  {
+  private:
+    symbolst::iterator it;
+    std::function<void(const irep_idt &id)> on_get_writeable;
+
+  public:
+    explicit iteratort(symbolst::iterator it) : it(std::move(it))
+    {
+    }
+
+    iteratort(
+        const iteratort &it,
+        std::function<void(const irep_idt &id)> on_get_writeable)
+      : it(it.it), on_get_writeable(std::move(on_get_writeable))
+    {
+    }
+
+    // The following typedefs are NOLINT as they are needed by the STL
+    typedef symbolst::iterator::difference_type difference_type;     // NOLINT
+    typedef symbolst::const_iterator::value_type value_type;         // NOLINT
+    typedef symbolst::const_iterator::pointer pointer;               // NOLINT
+    typedef symbolst::const_iterator::reference reference;           // NOLINT
+    typedef symbolst::iterator::iterator_category iterator_category; // NOLINT
+
+    bool operator==(const iteratort &other) const
+    {
+      return it == other.it;
+    }
+
+    /// Preincrement operator
+    /// Do not call on the end() iterator
+    iteratort &operator++()
+    {
+      ++it;
+      return *this;
+    }
+
+    /// Post-increment operator
+    /// \remarks Expensive copy. Avoid if possible.
+    iteratort operator++(int)
+    {
+      iteratort copy(*this);
+      this->operator++();
+      return copy;
+    }
+
+    /// Dereference operator
+    /// \remarks Dereferencing end() iterator is undefined behaviour
+    reference operator*() const
+    {
+      return *it;
+    }
+
+    /// Dereference operator (member access)
+    /// \remarks Dereferencing end() iterator is undefined behaviour
+    pointer operator->() const
+    {
+      return &**this;
+    }
+
+    symbolt &get_writeable_symbol(const irep_idt &identifier)
+    {
+      if(on_get_writeable)
+        on_get_writeable((*this)->first);
+      return it->second;
+    }
+  };
+
+  virtual iteratort begin() = 0;
+  virtual iteratort end() = 0;
 };
 
 std::ostream &