diff --git a/regression/cbmc-concurrency/malloc2/main.c b/regression/cbmc-concurrency/malloc2/main.c
new file mode 100644
index 00000000000..8634e886ccf
--- /dev/null
+++ b/regression/cbmc-concurrency/malloc2/main.c
@@ -0,0 +1,21 @@
+#include <stdlib.h>
+#include <pthread.h>
+
+_Bool set_done;
+int *ptr;
+
+void *set_x(void *arg)
+{
+  *(int *)arg = 10;
+  set_done = 1;
+}
+
+int main(int argc, char *argv[])
+{
+  __CPROVER_assume(argc >= sizeof(int));
+  ptr = malloc(argc);
+  __CPROVER_ASYNC_1: set_x(ptr);
+  __CPROVER_assume(set_done);
+  assert(*ptr == 10);
+  return 0;
+}
diff --git a/regression/cbmc-concurrency/malloc2/test.desc b/regression/cbmc-concurrency/malloc2/test.desc
new file mode 100644
index 00000000000..9efefbc7362
--- /dev/null
+++ b/regression/cbmc-concurrency/malloc2/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp
index 1a7ba984e82..6294e47b3a1 100644
--- a/src/goto-symex/symex_builtin_functions.cpp
+++ b/src/goto-symex/symex_builtin_functions.cpp
@@ -138,14 +138,15 @@ void goto_symext::symex_allocate(
     {
       exprt &size=to_array_type(object_type).size();
 
-      symbolt size_symbol;
+      auxiliary_symbolt size_symbol;
 
       size_symbol.base_name=
         "dynamic_object_size"+std::to_string(dynamic_counter);
       size_symbol.name="symex_dynamic::"+id2string(size_symbol.base_name);
-      size_symbol.is_lvalue=true;
       size_symbol.type=tmp_size.type();
       size_symbol.mode = mode;
+      size_symbol.type.set(ID_C_constant, true);
+      size_symbol.value = size;
 
       state.symbol_table.add(size_symbol);