diff options
| author | Dejan Jovanović <dejan@cs.nyu.edu> | 2013-03-23 00:27:42 -0400 |
|---|---|---|
| committer | Dejan Jovanović <dejan@cs.nyu.edu> | 2013-03-23 00:27:42 -0400 |
| commit | 54b7a17226dd71f25b9f4b0f315ccdb53c1c0292 (patch) | |
| tree | f13d53d9442a23dbf664696a45eb04caaed7dc7e /src/util/hash.h | |
| parent | 17921b8fabea67fffd7d6a2a4b476dba06f3cb0c (diff) | |
changing string hash function to use the gnu namespace
due to namesapce resolution std namespace was used instead, which hashes the string pointers leading to mayhem
Diffstat (limited to 'src/util/hash.h')
| -rw-r--r-- | src/util/hash.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/util/hash.h b/src/util/hash.h index 4d4094143..913358512 100644 --- a/src/util/hash.h +++ b/src/util/hash.h @@ -48,7 +48,7 @@ namespace CVC4 { struct StringHashFunction { size_t operator()(const std::string& str) const { - return std::hash<const char*>()(str.c_str()); + return __gnu_cxx::hash<const char*>()(str.c_str()); } };/* struct StringHashFunction */ |