diff --git a/src/goto-symex/goto_state.cpp b/src/goto-symex/goto_state.cpp
index 82ca5b40463..2ef30164ad2 100644
--- a/src/goto-symex/goto_state.cpp
+++ b/src/goto-symex/goto_state.cpp
@@ -17,7 +17,10 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 /// because there aren't any current callers.
 void goto_statet::output_propagation_map(std::ostream &out)
 {
-  for(const auto &name_value : propagation)
+  sharing_mapt<irep_idt, exprt>::viewt view;
+  propagation.get_view(view);
+
+  for(const auto &name_value : view)
   {
     out << name_value.first << " <- " << format(name_value.second) << "\n";
   }
@@ -86,7 +89,11 @@ void goto_statet::apply_condition(
         increase_generation(
           l1_identifier, l1_lhs, previous_state.get_l2_name_provider());
 
-        propagation[l1_identifier] = rhs;
+        const auto propagation_entry = propagation.find(l1_identifier);
+        if(!propagation_entry.has_value())
+          propagation.insert(l1_identifier, rhs);
+        else if(propagation_entry->get() != rhs)
+          propagation.replace(l1_identifier, rhs);
 
         value_set.assign(l1_lhs, rhs, ns, true, false);
       }
diff --git a/src/goto-symex/goto_state.h b/src/goto-symex/goto_state.h
index 709d45e93ba..b9fea0528cc 100644
--- a/src/goto-symex/goto_state.h
+++ b/src/goto-symex/goto_state.h
@@ -12,6 +12,8 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 #ifndef CPROVER_GOTO_SYMEX_GOTO_STATE_H
 #define CPROVER_GOTO_SYMEX_GOTO_STATE_H
 
+#include <util/sharing_map.h>
+
 #include <analyses/guard.h>
 #include <analyses/local_safe_pointers.h>
 #include <pointer-analysis/value_set.h>
@@ -54,7 +56,7 @@ class goto_statet
   // "constants" can include symbols, but only in the context of an address-of
   // op (i.e. &x can be propagated), and an address-taken thing should only be
   // L1.
-  std::map<irep_idt, exprt> propagation;
+  sharing_mapt<irep_idt, exprt> propagation;
 
   void output_propagation_map(std::ostream &);
 
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index b4da35b1185..1a2d5c8eacc 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/src/goto-symex/goto_symex_state.cpp
@@ -201,8 +201,14 @@ void goto_symex_statet::assignment(
   // for value propagation -- the RHS is L2
 
   if(!is_shared && record_value && goto_symex_is_constantt()(rhs))
-    propagation[l1_identifier] = rhs;
-  else
+  {
+    const auto propagation_entry = propagation.find(l1_identifier);
+    if(!propagation_entry.has_value())
+      propagation.insert(l1_identifier, rhs);
+    else if(propagation_entry->get() != rhs)
+      propagation.replace(l1_identifier, rhs);
+  }
+  else if(propagation.has_key(l1_identifier))
     propagation.erase(l1_identifier);
 
   {
@@ -289,8 +295,8 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns)
         // L1 identifiers are used for propagation!
         auto p_it = propagation.find(ssa.get_identifier());
 
-        if(p_it != propagation.end())
-          expr=p_it->second; // already L2
+        if(p_it.has_value())
+          expr = *p_it; // already L2
         else
           ssa = set_indices<L2>(std::move(ssa), ns).get();
       }
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index 6ec66cba127..879827a3f1d 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -502,7 +502,7 @@ void goto_symext::symex_assign_symbol(
     // Erase the composite symbol from our working state. Note that we need to
     // have it in the propagation table and the value set while doing the field
     // assignments, thus we cannot skip putting it in there above.
-    state.propagation.erase(l1_lhs.get_identifier());
+    state.propagation.erase_if_exists(l1_lhs.get_identifier());
     state.value_set.erase_symbol(l1_lhs, ns);
   }
 
diff --git a/src/goto-symex/symex_dead.cpp b/src/goto-symex/symex_dead.cpp
index d563c16b4fc..28dfd6c2e04 100644
--- a/src/goto-symex/symex_dead.cpp
+++ b/src/goto-symex/symex_dead.cpp
@@ -34,9 +34,8 @@ void goto_symext::symex_dead(statet &state)
     // information is not local to a path, but removing it from the propagation
     // map and value-set is safe as 1) it is local to a path and 2) this
     // instance can no longer appear.
-    if(state.value_set.values.has_key(l1_identifier))
-      state.value_set.values.erase(l1_identifier);
-    state.propagation.erase(l1_identifier);
+    state.value_set.values.erase_if_exists(l1_identifier);
+    state.propagation.erase_if_exists(l1_identifier);
     // Remove from the local L2 renaming map; this means any reads from the dead
     // identifier will use generation 0 (e.g. x!N@M#0, where N and M are
     // positive integers), which is never defined by any write, and will be
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
index 55556d3d8df..4807fc6de6f 100644
--- a/src/goto-symex/symex_goto.cpp
+++ b/src/goto-symex/symex_goto.cpp
@@ -522,8 +522,8 @@ static void merge_names(
   {
     const auto p_it = goto_state.propagation.find(l1_identifier);
 
-    if(p_it != goto_state.propagation.end())
-      goto_state_rhs = p_it->second;
+    if(p_it.has_value())
+      goto_state_rhs = *p_it;
     else
       to_ssa_expr(goto_state_rhs).set_level_2(goto_count);
   }
@@ -531,8 +531,8 @@ static void merge_names(
   {
     const auto p_it = dest_state.propagation.find(l1_identifier);
 
-    if(p_it != dest_state.propagation.end())
-      dest_state_rhs = p_it->second;
+    if(p_it.has_value())
+      dest_state_rhs = *p_it;
     else
       to_ssa_expr(dest_state_rhs).set_level_2(dest_count);
   }