diff --git a/src/util/dstring.h b/src/util/dstring.h index d7b2c76409d..91c58a39f38 100644 --- a/src/util/dstring.h +++ b/src/util/dstring.h @@ -175,4 +175,18 @@ inline std::ostream &operator<<(std::ostream &out, const dstringt &a) return a.operator<<(out); } +// NOLINTNEXTLINE [allow specialisation within 'std'] +namespace std +{ +/// Default hash function of `dstringt` for use with STL containers. +template <> +struct hash // NOLINT(readability/identifiers) +{ + size_t operator()(const dstringt &dstring) const + { + return dstring.hash(); + } +}; +} + #endif // CPROVER_UTIL_DSTRING_H