diff --git a/regression/cbmc-cpp/typedef1/main.cpp b/regression/cbmc-cpp/typedef1/main.cpp
new file mode 100644
index 00000000000..1a6da72613e
--- /dev/null
+++ b/regression/cbmc-cpp/typedef1/main.cpp
@@ -0,0 +1,7 @@
+typedef int XYZ;
+
+int main(int argc, char *argv[])
+{
+  XYZ a;
+  return a;
+}
diff --git a/regression/cbmc-cpp/typedef1/test.desc b/regression/cbmc-cpp/typedef1/test.desc
new file mode 100644
index 00000000000..2dd5f07359f
--- /dev/null
+++ b/regression/cbmc-cpp/typedef1/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.cpp
+--show-symbol-table
+activate-multi-line-match
+Symbol......: main::1::a\nPretty name.: main::1::a\nModule......: main\nBase name...: a\nMode........: cpp\nType........: XYZ\n
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/src/cpp/cpp_declarator_converter.cpp b/src/cpp/cpp_declarator_converter.cpp
index 82fee24d3ff..e6a8a7ca801 100644
--- a/src/cpp/cpp_declarator_converter.cpp
+++ b/src/cpp/cpp_declarator_converter.cpp
@@ -90,6 +90,9 @@ symbolt &cpp_declarator_convertert::convert(
 
   get_final_identifier();
 
+  if(is_typedef)
+    final_type.set(ID_C_typedef, final_identifier);
+
   // first see if it is a member
   if(scope->id_class == cpp_idt::id_classt::CLASS)
   {