diff --git a/regression/goto-cc-cbmc/tmp_post_with_name/main.c b/regression/goto-cc-cbmc/tmp_post_with_name/main.c
new file mode 100644
index 00000000000..704cce41787
--- /dev/null
+++ b/regression/goto-cc-cbmc/tmp_post_with_name/main.c
@@ -0,0 +1,10 @@
+#include <assert.h>
+
+int main(int argc, char **argv)
+{
+  char *ptr;
+  ptr = malloc(2);
+  ptr += 2;
+  char c = *ptr++;
+  return 0;
+}
diff --git a/regression/goto-cc-cbmc/tmp_post_with_name/test.desc b/regression/goto-cc-cbmc/tmp_post_with_name/test.desc
new file mode 100644
index 00000000000..f9cbe51a11c
--- /dev/null
+++ b/regression/goto-cc-cbmc/tmp_post_with_name/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^\[main\.pointer_dereference\.5\] line 8 dereference failure: pointer outside object bounds in \*tmp_post_ptr: FAILURE
+\*\* 1 of [0-9]* failed 
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp
index dd24393cbe6..fbd99e6dbbb 100644
--- a/src/goto-programs/goto_convert_side_effect.cpp
+++ b/src/goto-programs/goto_convert_side_effect.cpp
@@ -314,7 +314,14 @@ void goto_convertt::remove_post(
   if(result_is_used)
   {
     exprt tmp = op;
-    make_temp_symbol(tmp, "post", dest, mode);
+    std::string suffix = "post";
+    if(auto sym_expr = expr_try_dynamic_cast<symbol_exprt>(tmp))
+    {
+      const irep_idt &base_name = ns.lookup(*sym_expr).base_name;
+      suffix += "_" + id2string(base_name);
+    }
+
+    make_temp_symbol(tmp, suffix, dest, mode);
     expr.swap(tmp);
   }
   else