diff --git a/regression/cbmc/Malloc25/main.c b/regression/cbmc/Malloc25/main.c
new file mode 100644
index 00000000000..e94a97528ba
--- /dev/null
+++ b/regression/cbmc/Malloc25/main.c
@@ -0,0 +1,7 @@
+#include <stdlib.h>
+
+int main(int argc, char *argv[])
+{
+  int *p = malloc((size_t)argc * (size_t)argc * sizeof(int));
+  return 0;
+}
diff --git a/regression/cbmc/Malloc25/test.desc b/regression/cbmc/Malloc25/test.desc
new file mode 100644
index 00000000000..9efefbc7362
--- /dev/null
+++ b/regression/cbmc/Malloc25/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 fcaeedbb2ed..02c51072899 100644
--- a/src/goto-symex/symex_builtin_functions.cpp
+++ b/src/goto-symex/symex_builtin_functions.cpp
@@ -102,7 +102,7 @@ void goto_symext::symex_allocate(
 
           object_type = array_typet(*tmp_type, s);
         }
-        else
+        else if(alloc_size.has_value())
         {
           if(*alloc_size == *elem_size)
             object_type = *tmp_type;