diff --git a/src/util/dstring.h b/src/util/dstring.h
index 36ae8ec2783..33230bb235c 100644
--- a/src/util/dstring.h
+++ b/src/util/dstring.h
@@ -21,7 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 /// \ref dstringt has one field, an unsigned integer \ref no which is an index
 /// into a static table of strings. This makes it expensive to create a new
-/// string(because you have to look through the whole table to see if it is
+/// string (because you have to look through the whole table to see if it is
 /// already there, and add it if it isn't) but very cheap to compare strings
 /// (just compare the two integers). It also means that when you have lots of
 /// copies of the same string you only have to store the whole string once,
@@ -30,10 +30,7 @@ Author: Daniel Kroening, kroening@kroening.com
 /// `irep_idt` and `irep_namet` are typedef-ed to \ref dstringt in irep.h unless
 /// `USE_STD_STRING` is set.
 ///
-///
-/// Note: Marked final to disable inheritance. No virtual destructor, so
-/// runtime-polymorphic use would be unsafe.
-class dstringt final
+class dstringt
 {
 public:
   // this is safe for static objects
@@ -183,8 +180,8 @@ class dstringt final
     return as_string().end();
   }
 
-private:
-  #ifdef __GNUC__
+protected:
+#ifdef __GNUC__
   constexpr
   #endif
   explicit dstringt(unsigned _no):no(_no)
diff --git a/src/util/irep.h b/src/util/irep.h
index 2e2dacf91c0..a3f924a723a 100644
--- a/src/util/irep.h
+++ b/src/util/irep.h
@@ -29,8 +29,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #endif
 
 #ifdef USE_DSTRING
-typedef dstringt irep_idt;
-typedef dstringt irep_namet;
+typedef irep_idt irep_namet;
 // NOLINTNEXTLINE(readability/identifiers)
 typedef dstring_hash irep_id_hash;
 #else
diff --git a/src/util/irep_ids.cpp b/src/util/irep_ids.cpp
index 5a6bc4e525d..a5964272a19 100644
--- a/src/util/irep_ids.cpp
+++ b/src/util/irep_ids.cpp
@@ -27,30 +27,15 @@ const char *irep_ids_table[]=
 
 #ifdef USE_DSTRING
 
-enum class idt:unsigned
-{
-#define IREP_ID_ONE(the_id) id_##the_id,
-#define IREP_ID_TWO(the_id, str) id_##the_id,
-
-#include "irep_ids.def" // NOLINT(build/include)
-};
-
-#define IREP_ID_ONE(the_id)                                                    \
-  const dstringt ID_##the_id=dstringt::make_from_table_index(                  \
-      static_cast<unsigned>(idt::id_##the_id));
-#define IREP_ID_TWO(the_id, str)                                               \
-  const dstringt ID_##the_id=dstringt::make_from_table_index(                  \
-      static_cast<unsigned>(idt::id_##the_id));
-
 #else
 
 #define IREP_ID_ONE(the_id) const std::string ID_##the_id(#the_id);
 #define IREP_ID_TWO(the_id, str) const std::string ID_##the_id(#the_id);
 
-#endif
-
 #include "irep_ids.def" // NOLINT(build/include)
 
+#endif
+
 string_containert::string_containert()
 {
   // pre-allocate empty string -- this gets index 0
diff --git a/src/util/irep_ids.h b/src/util/irep_ids.h
index b96ff929f25..5f5e5b0f0a1 100644
--- a/src/util/irep_ids.h
+++ b/src/util/irep_ids.h
@@ -36,8 +36,115 @@ Author: Reuben Thomas, reuben.thomas@me.com
 
 #ifdef USE_DSTRING
 
-#define IREP_ID_ONE(the_id) extern const dstringt ID_##the_id;
-#define IREP_ID_TWO(the_id, str) extern const dstringt ID_##the_id;
+enum class idt : unsigned
+{
+#define IREP_ID_ONE(the_id) id_##the_id,
+#define IREP_ID_TWO(the_id, str) id_##the_id,
+
+#include "irep_ids.def" // NOLINT(build/include)
+};
+
+class irep_idt final : public dstringt
+{
+public:
+// this is safe for static objects
+#ifdef __GNUC__
+  constexpr
+#endif
+    irep_idt()
+    : dstringt()
+  {
+  }
+
+// this is safe for static objects
+#ifdef __GNUC__
+  constexpr
+#endif
+    static irep_idt
+    make_from_table_index(unsigned no)
+  {
+    return irep_idt(no);
+  }
+
+#ifdef __GNUC__
+  // This conversion allows the use of irep_idts
+  // in switch ... case statements.
+  constexpr operator idt() const
+  {
+    return static_cast<idt>(no);
+  }
+#endif
+
+  // this one is safe for static objects
+#ifdef __GNUC__
+  constexpr
+#endif
+    // NOLINTNEXTLINE(runtime/explicit)
+    irep_idt(dstringt s)
+    : dstringt(s)
+  {
+  }
+
+  // this one is not safe for static objects
+  // NOLINTNEXTLINE(runtime/explicit)
+  irep_idt(const char *s) : dstringt(s)
+  {
+  }
+
+  // this one is not safe for static objects
+  // NOLINTNEXTLINE(runtime/explicit)
+  irep_idt(const std::string &s) : dstringt(s)
+  {
+  }
+
+protected:
+#ifdef __GNUC__
+  constexpr
+#endif
+    explicit irep_idt(unsigned _no)
+    : dstringt(_no)
+  {
+  }
+};
+
+// NOLINTNEXTLINE [allow specialisation within 'std']
+namespace std
+{
+/// Default hash function of `dstringt` for use with STL containers.
+template <>
+struct hash<irep_idt> // NOLINT(readability/identifiers)
+{
+  size_t operator()(const irep_idt &irep_id) const
+  {
+    return irep_id.hash();
+  }
+};
+} // namespace std
+
+#ifdef __GNUC__
+#define IREP_ID_ONE(the_id)                                                    \
+  constexpr irep_idt ID_##the_id =                                             \
+    irep_idt::make_from_table_index(static_cast<unsigned>(idt::id_##the_id));
+#define IREP_ID_TWO(the_id, str)                                               \
+  constexpr irep_idt ID_##the_id =                                             \
+    irep_idt::make_from_table_index(static_cast<unsigned>(idt::id_##the_id));
+#else
+#define IREP_ID_ONE(the_id)                                                    \
+  const irep_idt ID_##the_id =                                                 \
+    irep_idt::make_from_table_index(static_cast<unsigned>(idt::id_##the_id));
+#define IREP_ID_TWO(the_id, str)                                               \
+  const const irep_idt ID_##the_id =                                           \
+    irep_idt::make_from_table_index(static_cast<unsigned>(idt::id_##the_id));
+#endif
+
+template <>
+struct diagnostics_helpert<irep_idt>
+{
+  static std::string diagnostics_as_string(const irep_idt &irep_id)
+  {
+    return as_string(irep_id);
+  }
+};
 
 #else