summaryrefslogtreecommitdiff
path: root/src/theory/term_registration_visitor.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/term_registration_visitor.h')
-rw-r--r--src/theory/term_registration_visitor.h4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/term_registration_visitor.h b/src/theory/term_registration_visitor.h
index 39cce27f9..2a84a7995 100644
--- a/src/theory/term_registration_visitor.h
+++ b/src/theory/term_registration_visitor.h
@@ -20,7 +20,7 @@
#include "context/context.h"
#include "theory/shared_terms_database.h"
-#include <ext/hash_map>
+#include <unordered_map>
namespace CVC4 {
@@ -105,7 +105,7 @@ class SharedTermsVisitor {
/**
* Cache from preprocessing of atoms.
*/
- typedef std::hash_map<TNode, theory::Theory::Set, TNodeHashFunction> TNodeVisitedMap;
+ typedef std::unordered_map<TNode, theory::Theory::Set, TNodeHashFunction> TNodeVisitedMap;
TNodeVisitedMap d_visited;
/**
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback