diff --git a/src/goto-instrument/wmm/shared_buffers.cpp b/src/goto-instrument/wmm/shared_buffers.cpp
index e575f613d9c..e64b50d4321 100644
--- a/src/goto-instrument/wmm/shared_buffers.cpp
+++ b/src/goto-instrument/wmm/shared_buffers.cpp
@@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "shared_buffers.h"
 
 #include <util/c_types.h>
+#include <util/fresh_symbol.h>
 
 #include <linking/static_lifetime_init.h>
 
@@ -88,21 +89,22 @@ irep_idt shared_bufferst::add(
   const typet &type,
   bool instrument)
 {
-  const irep_idt identifier=id2string(object)+suffix;
+  const namespacet ns(symbol_table);
 
-  symbolt new_symbol;
-  new_symbol.name=identifier;
-  new_symbol.base_name=id2string(base_name)+suffix;
-  new_symbol.type=type;
+  symbolt &new_symbol = get_fresh_aux_symbol(
+    type,
+    id2string(object) + suffix,
+    id2string(base_name) + suffix,
+    ns.lookup(object).location,
+    ns.lookup(object).mode,
+    symbol_table);
   new_symbol.is_static_lifetime=true;
   new_symbol.value.make_nil();
 
   if(instrument)
-    instrumentations.insert(identifier);
+    instrumentations.insert(new_symbol.name);
 
-  symbolt *symbol_ptr;
-  symbol_table.move(new_symbol, symbol_ptr);
-  return identifier;
+  return new_symbol.name;
 }
 
 void shared_bufferst::add_initialization(goto_programt &goto_program)
diff --git a/src/goto-instrument/wmm/weak_memory.cpp b/src/goto-instrument/wmm/weak_memory.cpp
index 243119cc916..f3f3b24fff1 100644
--- a/src/goto-instrument/wmm/weak_memory.cpp
+++ b/src/goto-instrument/wmm/weak_memory.cpp
@@ -23,6 +23,8 @@ Date: September 2011
 
 #include <set>
 
+#include <util/fresh_symbol.h>
+
 #include <goto-programs/remove_skip.h>
 
 #include <linking/static_lifetime_init.h>
@@ -44,7 +46,6 @@ void introduce_temporaries(
   messaget &message)
 {
   namespacet ns(symbol_table);
-  unsigned tmp_counter=0;
 
 #ifdef LOCAL_MAY
   local_may_aliast local_may(goto_function);
@@ -73,20 +74,19 @@ void introduce_temporaries(
       if(rw_set.empty())
         continue;
 
-      symbolt new_symbol;
-      new_symbol.base_name="$tmp_guard";
-      new_symbol.name =
-        id2string(function_id) + "$tmp_guard" + std::to_string(tmp_counter++);
-      new_symbol.type=bool_typet();
+      symbolt &new_symbol = get_fresh_aux_symbol(
+        bool_typet(),
+        id2string(function_id),
+        "$tmp_guard",
+        instruction.source_location,
+        ns.lookup(function_id).mode,
+        symbol_table);
       new_symbol.is_static_lifetime=true;
       new_symbol.is_thread_local=true;
       new_symbol.value.make_nil();
 
       symbol_exprt symbol_expr=new_symbol.symbol_expr();
 
-      symbolt *symbol_ptr;
-      symbol_table.move(new_symbol, symbol_ptr);
-
       goto_programt::instructiont new_i;
       new_i.make_assignment();
       new_i.code=code_assignt(symbol_expr, instruction.guard);