Merge branch 'master' into cleanup-regexp

123 files changed, 711 insertions, 1130 deletions

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 2757e3dbe..ffb299394 100644
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -21,7 +21,6 @@
 #include <iosfwd>
 #include <iterator>
 #include <sstream>
-#include <string>
 
 #include "base/exception.h"
 #include "base/output.h"
@@ -33,9 +32,6 @@
 #include "parser/parser_builder.h"
 #include "smt/command.h"
 #include "util/bitvector.h"
-#include "util/hash.h"
-#include "util/integer.h"
-#include "util/rational.h"
 #include "util/sexpr.h"
 #include "util/subrange_bound.h"
 
@@ -60,22 +56,22 @@ namespace CVC3 {
 // ExprManager-to-ExprManager import).
 static std::map<CVC4::ExprManager*, ValidityChecker*> s_validityCheckers;
 
-static std::hash_map<Type, Expr, CVC4::TypeHashFunction> s_typeToExpr;
-static std::hash_map<Expr, Type, CVC4::ExprHashFunction> s_exprToType;
+static std::unordered_map<Type, Expr, CVC4::TypeHashFunction> s_typeToExpr;
+static std::unordered_map<Expr, Type, CVC4::ExprHashFunction> s_exprToType;
 
 static bool typeHasExpr(const Type& t) {
-  std::hash_map<Type, Expr, CVC4::TypeHashFunction>::const_iterator i = s_typeToExpr.find(t);
+  std::unordered_map<Type, Expr, CVC4::TypeHashFunction>::const_iterator i = s_typeToExpr.find(t);
   return i != s_typeToExpr.end();
 }
 
 static Expr typeToExpr(const Type& t) {
-  std::hash_map<Type, Expr, CVC4::TypeHashFunction>::const_iterator i = s_typeToExpr.find(t);
+  std::unordered_map<Type, Expr, CVC4::TypeHashFunction>::const_iterator i = s_typeToExpr.find(t);
   assert(i != s_typeToExpr.end());
   return (*i).second;
 }
 
 static Type exprToType(const Expr& e) {
-  std::hash_map<Expr, Type, CVC4::ExprHashFunction>::const_iterator i = s_exprToType.find(e);
+  std::unordered_map<Expr, Type, CVC4::ExprHashFunction>::const_iterator i = s_exprToType.find(e);
   assert(i != s_exprToType.end());
   return (*i).second;
 }
@@ -311,8 +307,8 @@ Expr Expr::substExpr(const std::vector<Expr>& oldTerms,
 }
 
 Expr Expr::substExpr(const ExprHashMap<Expr>& oldToNew) const {
-  const hash_map<CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction>& o2n =
-    *reinterpret_cast<const hash_map<CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction>*>(&oldToNew);
+  const unordered_map<CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction>& o2n =
+    *reinterpret_cast<const unordered_map<CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction>*>(&oldToNew);
 
   return Expr(substitute(o2n));
 }
@@ -924,13 +920,16 @@ void CLFlags::setFlag(const std::string& name,
 }
 
 void ValidityChecker::setUpOptions(CVC4::Options& options, const CLFlags& clflags) {
+  // Note: SIMPLIFICATION_MODE_INCREMENTAL, which was used
+  // for CVC3 compatibility, is not supported by CVC4
+  // anymore.
+
   // always incremental and model-producing in CVC3 compatibility mode
   // also incrementally-simplifying and interactive
   d_smt->setOption("incremental", string("true"));
   // disable this option by default for now, because datatype models
   // are broken [MGD 10/4/2012]
   //d_smt->setOption("produce-models", string("true"));
-  d_smt->setOption("simplification-mode", string("incremental"));
   d_smt->setOption("interactive-mode", string("true"));// support SmtEngine::getAssertions()
 
   d_smt->setOption("statistics", string(clflags["stats"].getBool() ? "true" : "false"));
diff --git a/src/compat/cvc3_compat.h b/src/compat/cvc3_compat.h
index be0dc3393..25e3ae32f 100644
--- a/src/compat/cvc3_compat.h
+++ b/src/compat/cvc3_compat.h
@@ -49,7 +49,10 @@
 #define _cvc3__include__formula_value_h_
 
 #include <stdlib.h>
+
 #include <map>
+#include <string>
+#include <unordered_map>
 #include <utility>
 
 #include "base/exception.h"
@@ -58,7 +61,6 @@
 #include "expr/type.h"
 #include "parser/parser.h"
 #include "smt/smt_engine.h"
-#include "util/hash.h"
 #include "util/integer.h"
 #include "util/rational.h"
 
@@ -267,7 +269,7 @@ class CVC4_PUBLIC ExprMap : public std::map<Expr, T> {
 };/* class ExprMap<T> */
 
 template <class T>
-class CVC4_PUBLIC ExprHashMap : public std::hash_map<Expr, T, CVC4::ExprHashFunction> {
+class CVC4_PUBLIC ExprHashMap : public std::unordered_map<Expr, T, CVC4::ExprHashFunction> {
 public:
   void insert(Expr a, Expr b);
 };/* class ExprHashMap<T> */
@@ -521,8 +523,8 @@ class CVC4_PUBLIC ValidityChecker {
 
   friend class Type; // to reach in to d_exprTypeMapRemove
 
-  typedef std::hash_map<std::string, const CVC4::Datatype*, CVC4::StringHashFunction> ConstructorMap;
-  typedef std::hash_map<std::string, std::pair<const CVC4::Datatype*, std::string>, CVC4::StringHashFunction> SelectorMap;
+  typedef std::unordered_map<std::string, const CVC4::Datatype*> ConstructorMap;
+  typedef std::unordered_map<std::string, std::pair<const CVC4::Datatype*, std::string>> SelectorMap;
 
   ConstructorMap d_constructors;
   SelectorMap d_selectors;
diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h
index 86a7cb141..b6024b65d 100644
--- a/src/context/cdhashmap.h
+++ b/src/context/cdhashmap.h
@@ -15,7 +15,7 @@
  ** which must be saved and restored as contexts are pushed and
  ** popped.  Requires that operator= be defined for the data class,
  ** and operator== for the key class.  For key types that don't have a
- ** __gnu_cxx::hash<>, you should provide an explicit HashFcn.
+ ** std::hash<>, you should provide an explicit HashFcn.
  **
  ** See also:
  **  CDInsertHashMap : An "insert-once" CD hash map.
@@ -58,36 +58,23 @@
  **     its CDOhash_map object memory freed.  Here, the CDOhash_map is restored
  **     to a "NULL-map" state (see above), signaling it to remove
  **     itself from the map completely and put itself on a "trash
- **     list" for the map.
+ **     list" for its scope.
  **
- **     Third, you might obliterate() the key.  This calls the CDOhash_map
- **     destructor, which calls destroy(), which does a successive
- **     restore() until level 0.  If the key was in the map since
- **     level 0, the restore() won't remove it, so in that case
- **     obliterate() removes it from the map and frees the CDOhash_map's
- **     memory.
- **
- **     Fourth, you might delete the cdhashmap(calling CDHashMap::~CDHashMap()).
+ **     Third, you might delete the cdhashmap(calling CDHashMap::~CDHashMap()).
  **     This first calls destroy(), as per ContextObj contract, but
  **     cdhashmapdoesn't save/restore itself, so that does nothing at the
- **     CDHashMap-level.  Then it empties the trash.  Then, for each
- **     element in the map, it marks it as being "part of a complete
- **     map destruction", which essentially short-circuits
+ **     CDHashMap-level. Then, for each element in the map, it marks it as being
+ **     "part of a complete map destruction", which essentially short-circuits
  **     CDOhash_map::restore() (see CDOhash_map::restore()), then deallocates
- **     it.  Finally it asserts that the trash is empty (which it
- **     should be, since restore() was short-circuited).
+ **     it.
  **
- **     Fifth, you might clear() the CDHashMap.  This does exactly the
+ **     Fourth, you might clear() the CDHashMap.  This does exactly the
  **     same as CDHashMap::~CDHashMap(), except that it doesn't call destroy()
  **     on itself.
  **
- **     CDHashMap::emptyTrash() simply goes through and calls
- **     ->deleteSelf() on all elements in the trash.
  **     ContextObj::deleteSelf() calls the CDOhash_map destructor, then
  **     frees the memory associated to the CDOhash_map.  CDOhash_map::~CDOhash_map()
- **     calls destroy(), which restores as much as possible.  (Note,
- **     though, that since objects placed on the trash have already
- **     restored to the fullest extent possible, it does nothing.)
+ **     calls destroy(), which restores as much as possible.
  **/
 
 #include "cvc4_private.h"
@@ -95,8 +82,9 @@
 #ifndef __CVC4__CONTEXT__CDHASHMAP_H
 #define __CVC4__CONTEXT__CDHASHMAP_H
 
-#include <ext/hash_map>
+#include <functional>
 #include <iterator>
+#include <unordered_map>
 #include <vector>
 
 #include "base/cvc4_assert.h"
@@ -108,7 +96,7 @@ namespace context {
 
 // Auxiliary class: almost the same as CDO (see cdo.h)
 
-template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
+template <class Key, class Data, class HashFcn = std::hash<Key> >
 class CDOhash_map : public ContextObj {
   friend class CDHashMap<Key, Data, HashFcn>;
 
@@ -157,7 +145,7 @@ class CDOhash_map : public ContextObj {
         } else {
           Debug("gc") << "CDHashMap<> trash push_back " << this << std::endl;
           //this->deleteSelf();
-          d_map->d_trash.push_back(this);
+          enqueueToGarbageCollect();
         }
       } else {
         d_data = p->d_data;
@@ -281,7 +269,7 @@ template <class Key, class Data, class HashFcn>
 class CDHashMap : public ContextObj {
 
   typedef CDOhash_map<Key, Data, HashFcn> Element;
-  typedef __gnu_cxx::hash_map<Key, Element*, HashFcn> table_type;
+  typedef std::unordered_map<Key, Element*, HashFcn> table_type;
 
   friend class CDOhash_map<Key, Data, HashFcn>;
 
@@ -290,8 +278,6 @@ class CDHashMap : public ContextObj {
   Element* d_first;
   Context* d_context;
 
-  std::vector<Element*> d_trash;
-
   // Nothing to save; the elements take care of themselves
   virtual ContextObj* save(ContextMemoryManager* pCMM) {
     Unreachable();
@@ -302,75 +288,38 @@ class CDHashMap : public ContextObj {
     Unreachable();
   }
 
-  void emptyTrash() {
-    //FIXME multithreading
-    for(typename std::vector<Element*>::iterator i = d_trash.begin();
-        i != d_trash.end();
-        ++i) {
-      Debug("gc") << "emptyTrash(): " << *i << std::endl;
-      (*i)->deleteSelf();
-    }
-    d_trash.clear();
-  }
-
   // no copy or assignment
   CDHashMap(const CDHashMap&) CVC4_UNDEFINED;
   CDHashMap& operator=(const CDHashMap&) CVC4_UNDEFINED;
 
 public:
-
-  CDHashMap(Context* context) :
-    ContextObj(context),
-    d_map(),
-    d_first(NULL),
-    d_context(context),
-    d_trash() {
-  }
+  CDHashMap(Context* context)
+    : ContextObj(context), d_map(), d_first(NULL), d_context(context) {}
 
   ~CDHashMap() {
-    Debug("gc") << "cdhashmap" << this
-                << " disappearing, destroying..." << std::endl;
+    Debug("gc") << "cdhashmap" << this << " disappearing, destroying..."
+                << std::endl;
     destroy();
-    Debug("gc") << "cdhashmap" << this
-                << " disappearing, done destroying" << std::endl;
-
-    Debug("gc") << "cdhashmap" << this << " gone, emptying trash" << std::endl;
-    emptyTrash();
-    Debug("gc") << "done emptying trash for " << this << std::endl;
-
-    for(typename table_type::iterator i = d_map.begin();
-        i != d_map.end();
-        ++i) {
-      // mark it as being a destruction (short-circuit restore())
-      (*i).second->d_map = NULL;
-      if(!(*i).second->d_noTrash) {
-        (*i).second->deleteSelf();
-      }
-    }
-    d_map.clear();
-    d_first = NULL;
-
-    Assert(d_trash.empty());
+    Debug("gc") << "cdhashmap" << this << " disappearing, done destroying"
+                << std::endl;
+    clear();
   }
 
-  void clear() throw(AssertionException) {
-    Debug("gc") << "clearing cdhashmap" << this << ", emptying trash" << std::endl;
-    emptyTrash();
+  void clear() {
+    Debug("gc") << "clearing cdhashmap" << this << ", emptying trash"
+                << std::endl;
     Debug("gc") << "done emptying trash for " << this << std::endl;
 
-    for(typename table_type::iterator i = d_map.begin();
-        i != d_map.end();
-        ++i) {
+    for (auto& key_element_pair : d_map) {
       // mark it as being a destruction (short-circuit restore())
-      (*i).second->d_map = NULL;
-      if(!(*i).second->d_noTrash) {
-        (*i).second->deleteSelf();
+      Element* element = key_element_pair.second;
+      element->d_map = nullptr;
+      if (!element->d_noTrash) {
+        element->deleteSelf();
       }
     }
     d_map.clear();
-    d_first = NULL;
-
-    Assert(d_trash.empty());
+    d_first = nullptr;
   }
 
   // The usual operators of map
@@ -389,8 +338,6 @@ public:
 
   // If a key is not present, a new object is created and inserted
   Element& operator[](const Key& k) {
-    emptyTrash();
-
     typename table_type::iterator i = d_map.find(k);
 
     Element* obj;
@@ -404,8 +351,6 @@ public:
   }
 
   bool insert(const Key& k, const Data& d) {
-    emptyTrash();
-
     typename table_type::iterator i = d_map.find(k);
 
     if(i == d_map.end()) {// create new object
@@ -443,8 +388,6 @@ public:
    * insertAtContextLevelZero() a key that already is in the map.
    */
   void insertAtContextLevelZero(const Key& k, const Data& d) {
-    emptyTrash();
-
     AlwaysAssert(d_map.find(k) == d_map.end());
 
     Element* obj = new(true) Element(d_context, this, k, d,
@@ -454,43 +397,6 @@ public:
 
   // FIXME: no erase(), too much hassle to implement efficiently...
 
-  /**
-   * "Obliterating" is kind of like erasing, except it's not
-   * backtrackable; the key is permanently removed from the map.
-   * (Naturally, it can be re-added as a new element.)
-   */
-  void obliterate(const Key& k) {
-    typename table_type::iterator i = d_map.find(k);
-    if(i != d_map.end()) {
-      Debug("gc") << "key " << k << " obliterated" << std::endl;
-      // Restore this object to level 0.  If it was inserted after level 0,
-      // nothing else to do as restore will put it in the trash.
-      (*i).second->destroy();
-
-      // Check if object was inserted at level 0: in that case, still have
-      // to do some work.
-      typename table_type::iterator j = d_map.find(k);
-      if(j != d_map.end()) {
-        Element* elt = (*j).second;
-        if(d_first == elt) {
-          if(elt->d_next == elt) {
-            Assert(elt->d_prev == elt);
-            d_first = NULL;
-          } else {
-            d_first = elt->d_next;
-          }
-        }
-        elt->d_prev->d_next = elt->d_next;
-        elt->d_next->d_prev = elt->d_prev;
-        d_map.erase(j);//FIXME multithreading
-        Debug("gc") << "key " << k << " obliterated zero-scope: " << elt << std::endl;
-        if(!elt->d_noTrash) {
-          elt->deleteSelf();
-        }
-      }
-    }
-  }
-
   class iterator {
     const Element* d_it;
 
@@ -566,10 +472,6 @@ public:
     }
   }
 
-  iterator find(const Key& k) {
-    emptyTrash();
-    return const_cast<const CDHashMap*>(this)->find(k);
-  }
 
 };/* class CDHashMap<> */
 
diff --git a/src/context/cdhashmap_forward.h b/src/context/cdhashmap_forward.h
index e099f612e..a8fbc5ee2 100644
--- a/src/context/cdhashmap_forward.h
+++ b/src/context/cdhashmap_forward.h
@@ -26,15 +26,14 @@
 #ifndef __CVC4__CONTEXT__CDHASHMAP_FORWARD_H
 #define __CVC4__CONTEXT__CDHASHMAP_FORWARD_H
 
+#include <functional>
+
 /// \cond internals
 
-namespace __gnu_cxx {
-  template <class Key> struct hash;
-}/* __gnu_cxx namespace */
 
 namespace CVC4 {
   namespace context {
-    template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
+    template <class Key, class Data, class HashFcn = std::hash<Key> >
     class CDHashMap;
   }/* CVC4::context namespace */
 }/* CVC4 namespace */
diff --git a/src/context/cdinsert_hashmap.h b/src/context/cdinsert_hashmap.h
index ef8f661fa..db679c1f7 100644
--- a/src/context/cdinsert_hashmap.h
+++ b/src/context/cdinsert_hashmap.h
@@ -34,7 +34,8 @@
 #include "cvc4_private.h"
 
 #include <deque>
-#include <ext/hash_map>
+#include <functional>
+#include <unordered_map>
 #include <utility>
 
 #include "base/cvc4_assert.h"
@@ -50,14 +51,14 @@ namespace CVC4 {
 namespace context {
 
 
-template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
+template <class Key, class Data, class HashFcn = std::hash<Key> >
 class InsertHashMap {
 private:
   typedef std::deque<Key> KeyVec;
   /** A list of the keys in the map maintained as a stack. */
   KeyVec d_keys;
 
-  typedef __gnu_cxx::hash_map<Key, Data, HashFcn> HashMap;
+  typedef std::unordered_map<Key, Data, HashFcn> HashMap;
   /** The hash_map used for element lookup. */
   HashMap d_hashMap;
 
diff --git a/src/context/cdtrail_hashmap.h b/src/context/cdtrail_hashmap.h
index 0d265271d..e64c51c65 100644
--- a/src/context/cdtrail_hashmap.h
+++ b/src/context/cdtrail_hashmap.h
@@ -44,8 +44,9 @@
 
 #pragma once
 
-#include <ext/hash_map>
 #include <deque>
+#include <functional>
+#include <unordered_map>
 #include <utility>
 
 #include "base/cvc4_assert.h"
@@ -58,7 +59,7 @@ namespace CVC4 {
 namespace context {
 
 
-template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
+template <class Key, class Data, class HashFcn = std::hash<Key> >
 class TrailHashMap {
 public:
   /** A pair of Key and Data that mirrors hash_map::value_type. */
@@ -92,7 +93,7 @@ private:
   KDTVec d_kdts;
 
 
-  typedef __gnu_cxx::hash_map<Key, size_t, HashFcn> PositionMap;
+  typedef std::unordered_map<Key, size_t, HashFcn> PositionMap;
   typedef typename PositionMap::iterator PM_iterator;
   typedef typename PositionMap::const_iterator PM_const_iterator;
 
diff --git a/src/context/cdtrail_hashmap_forward.h b/src/context/cdtrail_hashmap_forward.h
index b2beb83bc..970f2758c 100644
--- a/src/context/cdtrail_hashmap_forward.h
+++ b/src/context/cdtrail_hashmap_forward.h
@@ -25,14 +25,11 @@
 
 #pragma once
 
-namespace __gnu_cxx {
-  template <class Key> struct hash;
-}/* __gnu_cxx namespace */
+#include <functional>
 
 namespace CVC4 {
   namespace context {
-    template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
+    template <class Key, class Data, class HashFcn = std::hash<Key> >
     class CDTrailHashMap;
   }/* CVC4::context namespace */
 }/* CVC4 namespace */
-
diff --git a/src/context/context.cpp b/src/context/context.cpp
index 2b781b95c..66d6a6542 100644
--- a/src/context/context.cpp
+++ b/src/context/context.cpp
@@ -296,6 +296,10 @@ ContextObj::ContextObj(bool allocatedInCMM, Context* pContext) :
   d_pScope->addToChain(this);
 }
 
+void ContextObj::enqueueToGarbageCollect() {
+  Assert(d_pScope != NULL);
+  d_pScope->enqueueToGarbageCollect(this);
+}
 
 ContextNotifyObj::ContextNotifyObj(Context* pContext, bool preNotify) {
   if(preNotify) {
@@ -354,6 +358,29 @@ std::ostream& operator<<(std::ostream& out,
   return out << " --> NULL";
 }
 
+Scope::~Scope() {
+  // Call restore() method on each ContextObj object in the list.
+  // Note that it is the responsibility of restore() to return the
+  // next item in the list.
+  while (d_pContextObjList != NULL) {
+    d_pContextObjList = d_pContextObjList->restoreAndContinue();
+  }
+
+  if (d_garbage) {
+    while (!d_garbage->empty()) {
+      ContextObj* obj = d_garbage->back();
+      d_garbage->pop_back();
+      obj->deleteSelf();
+    }
+  }
+}
+
+void Scope::enqueueToGarbageCollect(ContextObj* obj) {
+  if (!d_garbage) {
+    d_garbage.reset(new std::vector<ContextObj*>);
+  }
+  d_garbage->push_back(obj);
+}
 
 } /* CVC4::context namespace */
 } /* CVC4 namespace */
diff --git a/src/context/context.h b/src/context/context.h
index 9b3f57a5d..92eb10441 100644
--- a/src/context/context.h
+++ b/src/context/context.h
@@ -19,12 +19,13 @@
 #ifndef __CVC4__CONTEXT__CONTEXT_H
 #define __CVC4__CONTEXT__CONTEXT_H
 
-#include <iostream>
 #include <cstdlib>
 #include <cstring>
-#include <vector>
+#include <iostream>
+#include <memory>
 #include <new>
 #include <typeinfo>
+#include <vector>
 
 #include "base/cvc4_assert.h"
 #include "base/output.h"
@@ -257,6 +258,14 @@ class Scope {
    */
   ContextObj* d_pContextObjList;
 
+  /**
+   * A list of ContextObj to be garbage collected before the destruction of this
+   * scope. deleteSelf() will be called on each element during ~Scope().
+   *
+   * This is either nullptr or list owned by this scope.
+   */
+  std::unique_ptr<std::vector<ContextObj*>> d_garbage;
+
   friend std::ostream&
   operator<<(std::ostream&, const Scope&) throw(AssertionException);
 
@@ -266,54 +275,60 @@ public:
    * Constructor: Create a new Scope; set the level and the previous Scope
    * if any.
    */
-  Scope(Context* pContext, ContextMemoryManager* pCMM, int level) throw() :
-    d_pContext(pContext),
-    d_pCMM(pCMM),
-    d_level(level),
-    d_pContextObjList(NULL) {
+ Scope(Context* pContext, ContextMemoryManager* pCMM, int level) throw()
+     : d_pContext(pContext),
+       d_pCMM(pCMM),
+       d_level(level),
+       d_pContextObjList(nullptr),
+       d_garbage() {}
+
+ /**
+  * Destructor: Clears out all of the garbage and restore all of the objects
+  * in ContextObjList.
+  */
+ ~Scope();
+
+ /**
+  * Get the Context for this Scope
+  */
+ Context* getContext() const throw() { return d_pContext; }
+
+ /**
+  * Get the ContextMemoryManager for this Scope
+  */
+ ContextMemoryManager* getCMM() const throw() { return d_pCMM; }
+
+ /**
+  * Get the level of the current Scope
+  */
+ int getLevel() const throw() { return d_level; }
+
+ /**
+  * Return true iff this Scope is the current top Scope
+  */
+ bool isCurrent() const throw() { return this == d_pContext->getTopScope(); }
+
+ /**
+  * When a ContextObj object is modified for the first time in this
+  * Scope, it should call this method to add itself to the list of
+  * objects that will need to be restored.  Defined inline below.
+  */
+ void addToChain(ContextObj* pContextObj) throw(AssertionException);
+
+ /**
+  * Overload operator new for use with ContextMemoryManager to allow
+  * creation of new Scope objects in the current memory region.
+  */
+ static void* operator new(size_t size, ContextMemoryManager* pCMM) {
+   Trace("context_mm") << "Scope::new " << size << " in " << pCMM << std::endl;
+   return pCMM->newData(size);
   }
 
   /**
-   * Destructor: Restore all of the objects in ContextObjList.  Defined inline
-   * below.
-   */
-  ~Scope();
-
-  /**
-   * Get the Context for this Scope
-   */
-  Context* getContext() const throw() { return d_pContext; }
-
-  /**
-   * Get the ContextMemoryManager for this Scope
+   * Enqueues a ContextObj to be garbage collected via a call to deleteSelf()
+   * during the destruction of this scope.
    */
-  ContextMemoryManager* getCMM() const throw() { return d_pCMM; }
-
-  /**
-   * Get the level of the current Scope
-   */
-  int getLevel() const throw() { return d_level; }
-
-  /**
-   * Return true iff this Scope is the current top Scope
-   */
-  bool isCurrent() const throw() { return this == d_pContext->getTopScope(); }
-
-  /**
-   * When a ContextObj object is modified for the first time in this
-   * Scope, it should call this method to add itself to the list of
-   * objects that will need to be restored.  Defined inline below.
-   */
-  void addToChain(ContextObj* pContextObj) throw(AssertionException);
-
-  /**
-   * Overload operator new for use with ContextMemoryManager to allow
-   * creation of new Scope objects in the current memory region.
-   */
-  static void* operator new(size_t size, ContextMemoryManager* pCMM) {
-    Trace("context_mm") << "Scope::new " << size << " in " << pCMM << std::endl;
-    return pCMM->newData(size);
-  }
+  void enqueueToGarbageCollect(ContextObj* obj);
 
   /**
    * Overload operator delete for Scope objects allocated using
@@ -647,6 +662,12 @@ public:
     ::operator delete(this);
   }
 
+  /**
+   * Use this to enqueue calling deleteSelf() at the time of the destruction of
+   * the enclosing Scope.
+   */
+  void enqueueToGarbageCollect();
+
 };/* class ContextObj */
 
 /**
@@ -725,15 +746,6 @@ inline void ContextObj::makeSaveRestorePoint() throw(AssertionException) {
   update();
 }
 
-inline Scope::~Scope() {
-  // Call restore() method on each ContextObj object in the list.
-  // Note that it is the responsibility of restore() to return the
-  // next item in the list.
-  while(d_pContextObjList != NULL) {
-    d_pContextObjList = d_pContextObjList->restoreAndContinue();
-  }
-}
-
 inline void
 Scope::addToChain(ContextObj* pContextObj) throw(AssertionException) {
   if(d_pContextObjList != NULL) {
diff --git a/src/cvc4.i b/src/cvc4.i
index 5f90fdb7d..4768e2344 100644
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -11,7 +11,7 @@ namespace std {
   class istream;
   class ostream;
   template <class T> class set {};
-  template <class K, class V, class H> class hash_map {};
+  template <class K, class V, class H> class unordered_map {};
 }
 
 %{
@@ -41,7 +41,7 @@ namespace CVC4 {}
 using namespace CVC4;
 
 #include <cassert>
-#include <ext/hash_map>
+#include <unordered_map>
 #include <iosfwd>
 #include <set>
 #include <string>
@@ -86,7 +86,7 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
 %template(vectorPairStringType) std::vector< std::pair< std::string, CVC4::Type > >;
 %template(pairStringType) std::pair< std::string, CVC4::Type >;
 %template(setOfType) std::set< CVC4::Type >;
-%template(hashmapExpr) std::hash_map< CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction >;
+%template(hashmapExpr) std::unordered_map< CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction >;
 
 // This is unfortunate, but seems to be necessary; if we leave NULL
 // defined, swig will expand it to "(void*) 0", and some of swig's
diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
index 4c60f94fd..70fecb871 100644
--- a/src/decision/justification_heuristic.h
+++ b/src/decision/justification_heuristic.h
@@ -23,6 +23,8 @@
 #ifndef __CVC4__DECISION__JUSTIFICATION_HEURISTIC
 #define __CVC4__DECISION__JUSTIFICATION_HEURISTIC
 
+#include <unordered_set>
+
 #include "context/cdhashmap.h"
 #include "context/cdhashset.h"
 #include "context/cdlist.h"
@@ -78,13 +80,13 @@ class JustificationHeuristic : public ITEDecisionStrategy {
    * splitter. Can happen when exploring assertion corresponding to a
    * term-ITE.
    */
-  hash_set<TNode,TNodeHashFunction> d_visited;
+  std::unordered_set<TNode,TNodeHashFunction> d_visited;
 
   /**
    * Set to track visited nodes in a dfs search done in computeITE
    * function
    */
-  hash_set<TNode,TNodeHashFunction> d_visitedComputeITE;
+  std::unordered_set<TNode,TNodeHashFunction> d_visitedComputeITE;
 
   /** current decision for the recursive call */
   SatLiteral d_curDecision;
@@ -177,7 +179,6 @@ private:
 };/* class JustificationHeuristic */
 
 }/* namespace decision */
-
 }/* namespace CVC4 */
 
 #endif /* __CVC4__DECISION__JUSTIFICATION_HEURISTIC */
diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp
index 2f938736e..f221c7c7e 100644
--- a/src/expr/attribute.cpp
+++ b/src/expr/attribute.cpp
@@ -13,12 +13,12 @@
  **
  ** AttributeManager implementation.
  **/
+#include "expr/attribute.h"
+
 #include <utility>
 
 #include "base/output.h"
-#include "expr/attribute.h"
 #include "expr/node_value.h"
-#include "smt/smt_engine.h"
 
 using namespace std;
 
@@ -26,15 +26,6 @@ namespace CVC4 {
 namespace expr {
 namespace attr {
 
-SmtAttributes::SmtAttributes(context::Context* ctxt) :
-  d_cdbools(ctxt),
-  d_cdints(ctxt),
-  d_cdtnodes(ctxt),
-  d_cdnodes(ctxt),
-  d_cdstrings(ctxt),
-  d_cdptrs(ctxt) {
-}
-
 AttributeManager::AttributeManager() :
   d_inGarbageCollection(false)
 {}
@@ -43,15 +34,6 @@ bool AttributeManager::inGarbageCollection() const {
   return d_inGarbageCollection;
 }
 
-SmtAttributes& AttributeManager::getSmtAttributes(SmtEngine* smt) {
-  Assert(smt != NULL);
-  return *smt->d_smtAttributes;
-}
-
-const SmtAttributes& AttributeManager::getSmtAttributes(SmtEngine* smt) const {
-  return *smt->d_smtAttributes;
-}
-
 void AttributeManager::debugHook(int debugFlag) {
   /* DO NOT CHECK IN ANY CODE INTO THE DEBUG HOOKS!
    * debugHook() is an empty function for the purpose of debugging
@@ -71,17 +53,6 @@ void AttributeManager::deleteAllAttributes(NodeValue* nv) {
   deleteFromTable(d_ptrs, nv);
 }
 
-void SmtAttributes::deleteAllAttributes(TNode n) {
-  NodeValue* nv = n.d_nv;
-
-  d_cdbools.erase(nv);
-  deleteFromTable(d_cdints, nv);
-  deleteFromTable(d_cdtnodes, nv);
-  deleteFromTable(d_cdnodes, nv);
-  deleteFromTable(d_cdstrings, nv);
-  deleteFromTable(d_cdptrs, nv);
-}
-
 void AttributeManager::deleteAllAttributes() {
   d_bools.clear();
   deleteAllFromTable(d_ints);
diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index b5897ac51..5aea4a4d1 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -20,7 +20,6 @@
  * attributes and nodes due to template use */
 #include "expr/node.h"
 #include "expr/type_node.h"
-#include "context/context.h"
 
 #ifndef __CVC4__EXPR__ATTRIBUTE_H
 #define __CVC4__EXPR__ATTRIBUTE_H
@@ -35,45 +34,11 @@
 #undef CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H
 
 namespace CVC4 {
-
-class SmtEngine;
-
-namespace smt {
-  extern CVC4_THREADLOCAL(SmtEngine*) s_smtEngine_current;
-}/* CVC4::smt namespace */
-
 namespace expr {
 namespace attr {
 
 // ATTRIBUTE MANAGER ===========================================================
 
-struct SmtAttributes {
-  SmtAttributes(context::Context*);
-
-  // IF YOU ADD ANY TABLES, don't forget to add them also to the
-  // implementation of deleteAllAttributes().
-
-  /** Underlying hash table for context-dependent boolean-valued attributes */
-  CDAttrHash<bool> d_cdbools;
-  /** Underlying hash table for context-dependent integral-valued attributes */
-  CDAttrHash<uint64_t> d_cdints;
-  /** Underlying hash table for context-dependent node-valued attributes */
-  CDAttrHash<TNode> d_cdtnodes;
-  /** Underlying hash table for context-dependent node-valued attributes */
-  CDAttrHash<Node> d_cdnodes;
-  /** Underlying hash table for context-dependent string-valued attributes */
-  CDAttrHash<std::string> d_cdstrings;
-  /** Underlying hash table for context-dependent pointer-valued attributes */
-  CDAttrHash<void*> d_cdptrs;
-
-  /** Delete all attributes of given node */
-  void deleteAllAttributes(TNode n);
-
-  template <class T>
-  void deleteFromTable(CDAttrHash<T>& table, NodeValue* nv);
-
-};/* struct SmtAttributes */
-
 /**
  * A container for the main attribute tables of the system.  There's a
  * one-to-one NodeManager : AttributeManager correspondence.
@@ -103,9 +68,6 @@ class AttributeManager {
 
   void clearDeleteAllAttributesBuffer();
 
-  SmtAttributes& getSmtAttributes(SmtEngine*);
-  const SmtAttributes& getSmtAttributes(SmtEngine*) const;
-
 public:
 
   /** Construct an attribute manager. */
@@ -239,10 +201,10 @@ template <>
 struct getTable<bool, false> {
   static const AttrTableId id = AttrTableBool;
   typedef AttrHash<bool> table_type;
-  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
+  static inline table_type& get(AttributeManager& am) {
     return am.d_bools;
   }
-  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
+  static inline const table_type& get(const AttributeManager& am) {
     return am.d_bools;
   }
 };
@@ -252,10 +214,10 @@ template <>
 struct getTable<uint64_t, false> {
   static const AttrTableId id = AttrTableUInt64;
   typedef AttrHash<uint64_t> table_type;
-  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
+  static inline table_type& get(AttributeManager& am) {
     return am.d_ints;
   }
-  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
+  static inline const table_type& get(const AttributeManager& am) {
     return am.d_ints;
   }
 };
@@ -265,10 +227,10 @@ template <>
 struct getTable<TNode, false> {
   static const AttrTableId id = AttrTableTNode;
   typedef AttrHash<TNode> table_type;
-  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
+  static inline table_type& get(AttributeManager& am) {
     return am.d_tnodes;
   }
-  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
+  static inline const table_type& get(const AttributeManager& am) {
     return am.d_tnodes;
   }
 };
@@ -278,10 +240,10 @@ template <>
 struct getTable<Node, false> {
   static const AttrTableId id = AttrTableNode;
   typedef AttrHash<Node> table_type;
-  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
+  static inline table_type& get(AttributeManager& am) {
     return am.d_nodes;
   }
-  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
+  static inline const table_type& get(const AttributeManager& am) {
     return am.d_nodes;
   }
 };
@@ -291,10 +253,10 @@ template <>
 struct getTable<TypeNode, false> {
   static const AttrTableId id = AttrTableTypeNode;
   typedef AttrHash<TypeNode> table_type;
-  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
+  static inline table_type& get(AttributeManager& am) {
     return am.d_types;
   }
-  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
+  static inline const table_type& get(const AttributeManager& am) {
     return am.d_types;
   }
 };
@@ -304,10 +266,10 @@ template <>
 struct getTable<std::string, false> {
   static const AttrTableId id = AttrTableString;
   typedef AttrHash<std::string> table_type;
-  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
+  static inline table_type& get(AttributeManager& am) {
     return am.d_strings;
   }
-  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
+  static inline const table_type& get(const AttributeManager& am) {
     return am.d_strings;
   }
 };
@@ -317,10 +279,10 @@ template <class T>
 struct getTable<T*, false> {
   static const AttrTableId id = AttrTablePointer;
   typedef AttrHash<void*> table_type;
-  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
+  static inline table_type& get(AttributeManager& am) {
     return am.d_ptrs;
   }
-  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
+  static inline const table_type& get(const AttributeManager& am) {
     return am.d_ptrs;
   }
 };
@@ -330,105 +292,14 @@ template <class T>
 struct getTable<const T*, false> {
   static const AttrTableId id = AttrTablePointer;
   typedef AttrHash<void*> table_type;
-  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
+  static inline table_type& get(AttributeManager& am) {
     return am.d_ptrs;
   }
-  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
+  static inline const table_type& get(const AttributeManager& am) {
     return am.d_ptrs;
   }
 };
 
-/** Access the "d_cdbools" member of AttributeManager. */
-template <>
-struct getTable<bool, true> {
-  static const AttrTableId id = AttrTableCDBool;
-  typedef CDAttrHash<bool> table_type;
-  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
-    return am.getSmtAttributes(smt).d_cdbools;
-  }
-  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
-    return am.getSmtAttributes(smt).d_cdbools;
-  }
-};
-
-/** Access the "d_cdints" member of AttributeManager. */
-template <>
-struct getTable<uint64_t, true> {
-  static const AttrTableId id = AttrTableCDUInt64;
-  typedef CDAttrHash<uint64_t> table_type;
-  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
-    return am.getSmtAttributes(smt).d_cdints;
-  }
-  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
-    return am.getSmtAttributes(smt).d_cdints;
-  }
-};
-
-/** Access the "d_tnodes" member of AttributeManager. */
-template <>
-struct getTable<TNode, true> {
-  static const AttrTableId id = AttrTableCDTNode;
-  typedef CDAttrHash<TNode> table_type;
-  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
-    return am.getSmtAttributes(smt).d_cdtnodes;
-  }
-  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
-    return am.getSmtAttributes(smt).d_cdtnodes;
-  }
-};
-
-/** Access the "d_cdnodes" member of AttributeManager. */
-template <>
-struct getTable<Node, true> {
-  static const AttrTableId id = AttrTableCDNode;
-  typedef CDAttrHash<Node> table_type;
-  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
-    return am.getSmtAttributes(smt).d_cdnodes;
-  }
-  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
-    return am.getSmtAttributes(smt).d_cdnodes;
-  }
-};
-
-/** Access the "d_cdstrings" member of AttributeManager. */
-template <>
-struct getTable<std::string, true> {
-  static const AttrTableId id = AttrTableCDString;
-  typedef CDAttrHash<std::string> table_type;
-  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
-    return am.getSmtAttributes(smt).d_cdstrings;
-  }
-  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
-    return am.getSmtAttributes(smt).d_cdstrings;
-  }
-};
-
-/** Access the "d_cdptrs" member of AttributeManager. */
-template <class T>
-struct getTable<T*, true> {
-  static const AttrTableId id = AttrTableCDPointer;
-  typedef CDAttrHash<void*> table_type;
-  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
-    return am.getSmtAttributes(smt).d_cdptrs;
-  }
-  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
-    return am.getSmtAttributes(smt).d_cdptrs;
-  }
-};
-
-/** Access the "d_cdptrs" member of AttributeManager. */
-template <class T>
-struct getTable<const T*, true> {
-  static const AttrTableId id = AttrTableCDPointer;
-  typedef CDAttrHash<void*> table_type;
-  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
-    return am.getSmtAttributes(smt).d_cdptrs;
-  }
-  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
-    return am.getSmtAttributes(smt).d_cdptrs;
-  }
-};
-
 }/* CVC4::expr::attr namespace */
 
 // ATTRIBUTE MANAGER IMPLEMENTATIONS ===========================================
@@ -445,7 +316,7 @@ AttributeManager::getAttribute(NodeValue* nv, const AttrKind&) const {
             table_type table_type;
 
   const table_type& ah =
-    getTable<value_type, AttrKind::context_dependent>::get(*this, smt::s_smtEngine_current);
+    getTable<value_type, AttrKind::context_dependent>::get(*this);
   typename table_type::const_iterator i =
     ah.find(std::make_pair(AttrKind::getId(), nv));
 
@@ -488,7 +359,7 @@ struct HasAttribute<true, AttrKind> {
       table_type;
 
     const table_type& ah =
-      getTable<value_type, AttrKind::context_dependent>::get(*am, smt::s_smtEngine_current);
+      getTable<value_type, AttrKind::context_dependent>::get(*am);
     typename table_type::const_iterator i =
       ah.find(std::make_pair(AttrKind::getId(), nv));
 
@@ -516,7 +387,7 @@ struct HasAttribute<false, AttrKind> {
               table_type table_type;
 
     const table_type& ah =
-      getTable<value_type, AttrKind::context_dependent>::get(*am, smt::s_smtEngine_current);
+      getTable<value_type, AttrKind::context_dependent>::get(*am);
     typename table_type::const_iterator i =
       ah.find(std::make_pair(AttrKind::getId(), nv));
 
@@ -536,7 +407,7 @@ struct HasAttribute<false, AttrKind> {
               table_type table_type;
 
     const table_type& ah =
-      getTable<value_type, AttrKind::context_dependent>::get(*am, smt::s_smtEngine_current);
+      getTable<value_type, AttrKind::context_dependent>::get(*am);
     typename table_type::const_iterator i =
       ah.find(std::make_pair(AttrKind::getId(), nv));
 
@@ -576,7 +447,7 @@ AttributeManager::setAttribute(NodeValue* nv,
             table_type table_type;
 
   table_type& ah =
-    getTable<value_type, AttrKind::context_dependent>::get(*this, smt::s_smtEngine_current);
+      getTable<value_type, AttrKind::context_dependent>::get(*this);
   ah[std::make_pair(AttrKind::getId(), nv)] = mapping::convert(value);
 }
 
@@ -606,17 +477,6 @@ inline void AttributeManager::deleteFromTable(AttrHash<T>& table,
 }
 
 /**
- * Obliterate a NodeValue from a (context-dependent) attribute table.
- */
-template <class T>
-inline void SmtAttributes::deleteFromTable(CDAttrHash<T>& table,
-                                           NodeValue* nv) {
-  for(unsigned id = 0; id < attr::LastAttributeId<T, true>::getId(); ++id) {
-    table.obliterate(std::make_pair(id, nv));
-  }
-}
-
-/**
  * Remove all attributes from the table calling the cleanup function
  * if one is defined.
  */
diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h
index 861739932..37c7b6a0b 100644
--- a/src/expr/attribute_internals.h
+++ b/src/expr/attribute_internals.h
@@ -23,9 +23,7 @@
 #ifndef __CVC4__EXPR__ATTRIBUTE_INTERNALS_H
 #define __CVC4__EXPR__ATTRIBUTE_INTERNALS_H
 
-#include <ext/hash_map>
-
-#include "context/cdhashmap.h"
+#include <unordered_map>
 
 namespace CVC4 {
 namespace expr {
@@ -152,7 +150,7 @@ namespace attr {
  */
 template <class value_type>
 class AttrHash :
-    public __gnu_cxx::hash_map<std::pair<uint64_t, NodeValue*>,
+    public std::unordered_map<std::pair<uint64_t, NodeValue*>,
                                value_type,
                                AttrHashFunction> {
 };/* class AttrHash<> */
@@ -163,12 +161,12 @@ class AttrHash :
  */
 template <>
 class AttrHash<bool> :
-    protected __gnu_cxx::hash_map<NodeValue*,
+    protected std::unordered_map<NodeValue*,
                                   uint64_t,
                                   AttrBoolHashFunction> {
 
   /** A "super" type, like in Java, for easy reference below. */
-  typedef __gnu_cxx::hash_map<NodeValue*, uint64_t, AttrBoolHashFunction> super;
+  typedef std::unordered_map<NodeValue*, uint64_t, AttrBoolHashFunction> super;
 
   /**
    * BitAccessor allows us to return a bit "by reference."  Of course,
@@ -368,217 +366,6 @@ public:
   }
 };/* class AttrHash<bool> */
 
-/**
- * A "CDAttrHash<value_type>"---the hash table underlying
- * attributes---is simply a context-dependent mapping of
- * pair<unique-attribute-id, Node> to value_type using our specialized
- * hash function for these pairs.
- */
-template <class value_type>
-class CDAttrHash :
-    public context::CDHashMap<std::pair<uint64_t, NodeValue*>,
-                          value_type,
-                          AttrHashFunction> {
-public:
-  CDAttrHash(context::Context* ctxt) :
-    context::CDHashMap<std::pair<uint64_t, NodeValue*>,
-                   value_type,
-                   AttrHashFunction>(ctxt) {
-  }
-};/* class CDAttrHash<> */
-
-/**
- * In the case of Boolean-valued attributes we have a special
- * "CDAttrHash<bool>" to pack bits together in words.
- */
-template <>
-class CDAttrHash<bool> :
-    protected context::CDHashMap<NodeValue*,
-                             uint64_t,
-                             AttrBoolHashFunction> {
-
-  /** A "super" type, like in Java, for easy reference below. */
-  typedef context::CDHashMap<NodeValue*, uint64_t, AttrBoolHashFunction> super;
-
-  /**
-   * BitAccessor allows us to return a bit "by reference."  Of course,
-   * we don't require bit-addressibility supported by the system, we
-   * do it with a complex type.
-   */
-  class BitAccessor {
-
-    super& d_map;
-
-    NodeValue* d_key;
-
-    uint64_t d_word;
-
-    unsigned d_bit;
-
-  public:
-
-    BitAccessor(super& map, NodeValue* key, uint64_t word, unsigned bit) :
-      d_map(map),
-      d_key(key),
-      d_word(word),
-      d_bit(bit) {
-      /*
-      Debug.printf("cdboolattr",
-                   "CDAttrHash<bool>::BitAccessor(%p, %p, %016llx, %u)\n",
-                   &map, key, (unsigned long long) word, bit);
-      */
-    }
-
-    BitAccessor& operator=(bool b) {
-      if(b) {
-        // set the bit
-        d_word |= (1 << d_bit);
-        d_map.insert(d_key, d_word);
-        /*
-        Debug.printf("cdboolattr",
-                     "CDAttrHash<bool>::BitAccessor::set(%p, %p, %016llx, %u)\n",
-                     &d_map, d_key, (unsigned long long) d_word, d_bit);
-        */
-      } else {
-        // clear the bit
-        d_word &= ~(1 << d_bit);
-        d_map.insert(d_key, d_word);
-        /*
-        Debug.printf("cdboolattr",
-                     "CDAttrHash<bool>::BitAccessor::clr(%p, %p, %016llx, %u)\n",
-                     &d_map, d_key, (unsigned long long) d_word, d_bit);
-        */
-      }
-
-      return *this;
-    }
-
-    operator bool() const {
-      /*
-      Debug.printf("cdboolattr",
-                   "CDAttrHash<bool>::BitAccessor::toBool(%p, %p, %016llx, %u)\n",
-                   &d_map, d_key, (unsigned long long) d_word, d_bit);
-      */
-      return (d_word & (1 << d_bit)) ? true : false;
-    }
-  };/* class CDAttrHash<bool>::BitAccessor */
-
-  /**
-   * A (somewhat degenerate) const_iterator over boolean-valued
-   * attributes.  This const_iterator doesn't support anything except
-   * comparison and dereference.  It's intended just for the result of
-   * find() on the table.
-   */
-  class ConstBitIterator {
-
-    const std::pair<NodeValue* const, uint64_t> d_entry;
-
-    unsigned d_bit;
-
-  public:
-
-    ConstBitIterator() :
-      d_entry(),
-      d_bit(0) {
-    }
-
-    ConstBitIterator(const std::pair<NodeValue* const, uint64_t>& entry,
-                     unsigned bit) :
-      d_entry(entry),
-      d_bit(bit) {
-    }
-
-    std::pair<NodeValue* const, bool> operator*() {
-      return std::make_pair(d_entry.first,
-                            (d_entry.second & (1 << d_bit)) ? true : false);
-    }
-
-    bool operator==(const ConstBitIterator& b) {
-      return d_entry == b.d_entry && d_bit == b.d_bit;
-    }
-  };/* class CDAttrHash<bool>::ConstBitIterator */
-
-  /* remove non-permitted operations */
-  CDAttrHash(const CDAttrHash<bool>&) CVC4_UNDEFINED;
-  CDAttrHash<bool>& operator=(const CDAttrHash<bool>&) CVC4_UNDEFINED;
-
-public:
-
-  CDAttrHash(context::Context* context) : super(context) { }
-
-  typedef std::pair<uint64_t, NodeValue*> key_type;
-  typedef bool data_type;
-  typedef std::pair<const key_type, data_type> value_type;
-
-  /** an iterator type; see above for limitations */
-  typedef ConstBitIterator iterator;
-  /** a const_iterator type; see above for limitations */
-  typedef ConstBitIterator const_iterator;
-
-  /**
-   * Find the boolean value in the hash table.  Returns something ==
-   * end() if not found.
-   */
-  ConstBitIterator find(const std::pair<uint64_t, NodeValue*>& k) const {
-    super::const_iterator i = super::find(k.second);
-    if(i == super::end()) {
-      return ConstBitIterator();
-    }
-    /*
-    Debug.printf("cdboolattr",
-                 "underlying word at address looks like 0x%016llx, bit is %u\n",
-                 (unsigned long long)((*i).second),
-                 unsigned(k.first));
-    */
-    return ConstBitIterator(*i, k.first);
-  }
-
-  /** The "off the end" const_iterator */
-  ConstBitIterator end() const {
-    return ConstBitIterator();
-  }
-
-  /**
-   * Access the hash table using the underlying operator[].  Inserts
-   * the key into the table (associated to default value) if it's not
-   * already there.
-   */
-  BitAccessor operator[](const std::pair<uint64_t, NodeValue*>& k) {
-    uint64_t word = super::operator[](k.second);
-    return BitAccessor(*this, k.second, word, k.first);
-  }
-
-  /**
-   * Delete all flags from the given node.  Simply calls superclass's
-   * obliterate().  Note this removes all attributes at all context
-   * levels for this NodeValue!  This is important when the NodeValue
-   * is no longer referenced and is being collected, but otherwise
-   * it probably isn't useful to do this.
-   */
-  void erase(NodeValue* nv) {
-    super::obliterate(nv);
-  }
-
-  /**
-   * Clear the hash table.  This simply exposes the protected superclass
-   * version of clear() to clients.
-   */
-  void clear() {
-    super::clear();
-  }
-
-  /** Is the hash table empty? */
-  bool empty() const {
-    return super::empty();
-  }
-
-  /** This is currently very misleading! */
-  size_t size() const {
-    return super::size();
-  }
-
-};/* class CDAttrHash<bool> */
-
 }/* CVC4::expr::attr namespace */
 
 // ATTRIBUTE CLEANUP FUNCTIONS =================================================
@@ -853,17 +640,6 @@ public:
 };/* class Attribute<..., bool, ...> */
 
 /**
- * This is a context-dependent attribute kind (the only difference
- * between CDAttribute<> and Attribute<> (with the fourth argument
- * "true") is that you cannot supply a cleanup function (a no-op one
- * is used).
- */
-template <class T,
-          class value_type>
-struct CDAttribute :
-    public Attribute<T, value_type, attr::NullCleanupStrategy, true> {};
-
-/**
  * This is a managed attribute kind (the only difference between
  * ManagedAttribute<> and Attribute<> is the default cleanup function
  * and the fact that ManagedAttributes cannot be context-dependent).
diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index 84588fef0..27057ca99 100644
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -20,6 +20,7 @@
 #ifndef __CVC4__DATATYPE_H
 #define __CVC4__DATATYPE_H
 
+#include <functional>
 #include <iostream>
 #include <string>
 #include <vector>
@@ -788,16 +789,16 @@ public:
  */
 struct CVC4_PUBLIC DatatypeHashFunction {
   inline size_t operator()(const Datatype& dt) const {
-    return StringHashFunction()(dt.getName());
+    return std::hash<std::string>()(dt.getName());
   }
   inline size_t operator()(const Datatype* dt) const {
-    return StringHashFunction()(dt->getName());
+    return std::hash<std::string>()(dt->getName());
   }
   inline size_t operator()(const DatatypeConstructor& dtc) const {
-    return StringHashFunction()(dtc.getName());
+    return std::hash<std::string>()(dtc.getName());
   }
   inline size_t operator()(const DatatypeConstructor* dtc) const {
-    return StringHashFunction()(dtc->getName());
+    return std::hash<std::string>()(dtc->getName());
   }
 };/* struct DatatypeHashFunction */
 
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index cee154743..b0611ccbb 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -115,7 +115,7 @@ static Node exportConstant(TNode n, NodeManager* to, ExprManagerMapCollection& v
 
 class ExportPrivate {
 private:
-  typedef std::hash_map <NodeTemplate<false>, NodeTemplate<true>, TNodeHashFunction> ExportCache;
+  typedef std::unordered_map <NodeTemplate<false>, NodeTemplate<true>, TNodeHashFunction> ExportCache;
   ExprManager* from;
   ExprManager* to;
   ExprManagerMapCollection& vmap;
@@ -393,7 +393,7 @@ static inline NodePairIteratorAdaptor<Iterator> mkNodePairIteratorAdaptor(Iterat
   return NodePairIteratorAdaptor<Iterator>(i);
 }
 
-Expr Expr::substitute(const std::hash_map<Expr, Expr, ExprHashFunction> map) const {
+Expr Expr::substitute(const std::unordered_map<Expr, Expr, ExprHashFunction> map) const {
   ExprManagerScope ems(*this);
   return Expr(d_exprManager, new Node(d_node->substitute(mkNodePairIteratorAdaptor(map.begin()), mkNodePairIteratorAdaptor(map.end()))));
 }
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 57b4ff93a..d2ad45dee 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -29,8 +29,8 @@ ${includes}
 #include <stdint.h>
 #include <iostream>
 #include <iterator>
-
 #include <string>
+#include <unordered_map>
 
 #include "base/exception.h"
 #include "options/language.h"
@@ -433,7 +433,7 @@ public:
   /**
    * Substitute pairs of (ex,replacement) from the given map.
    */
-  Expr substitute(const std::hash_map<Expr, Expr, ExprHashFunction> map) const;
+  Expr substitute(const std::unordered_map<Expr, Expr, ExprHashFunction> map) const;
 
   /**
    * Returns the string representation of the expression.
diff --git a/src/expr/node.h b/src/expr/node.h
index 69bb98f95..7a8bafe38 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -22,13 +22,16 @@
 #ifndef __CVC4__NODE_H
 #define __CVC4__NODE_H
 
-#include <vector>
-#include <string>
-#include <iostream>
-#include <utility>
+#include <stdint.h>
+
 #include <algorithm>
 #include <functional>
-#include <stdint.h>
+#include <iostream>
+#include <string>
+#include <unordered_map>
+#include <unordered_set>
+#include <utility>
+#include <vector>
 
 #include "base/configuration.h"
 #include "base/cvc4_assert.h"
@@ -42,7 +45,6 @@
 #include "options/language.h"
 #include "options/set_language.h"
 #include "util/utility.h"
-#include "util/hash.h"
 
 namespace CVC4 {
 
@@ -243,7 +245,7 @@ public:
    * member function with a similar signature.
    */
   Node substitute(TNode node, TNode replacement,
-                  std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const;
+                  std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const;
 
   /**
    * Cache-aware, recursive version of substitute() used by the public
@@ -252,7 +254,7 @@ public:
   template <class Iterator1, class Iterator2>
   Node substitute(Iterator1 nodesBegin, Iterator1 nodesEnd,
                   Iterator2 replacementsBegin, Iterator2 replacementsEnd,
-                  std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const;
+                  std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const;
 
   /**
    * Cache-aware, recursive version of substitute() used by the public
@@ -260,7 +262,7 @@ public:
    */
   template <class Iterator>
   Node substitute(Iterator substitutionsBegin, Iterator substitutionsEnd,
-                  std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const;
+                  std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const;
 
   /** Default constructor, makes a null expression. */
   NodeTemplate() : d_nv(&expr::NodeValue::null()) { }
@@ -943,8 +945,6 @@ inline std::ostream& operator<<(std::ostream& out,
 
 }/* CVC4 namespace */
 
-#include <ext/hash_map>
-
 //#include "expr/attribute.h"
 #include "expr/node_manager.h"
 #include "expr/type_checker.h"
@@ -1296,14 +1296,14 @@ NodeTemplate<ref_count>::substitute(TNode node, TNode replacement) const {
   if (node == *this) {
     return replacement;
   }
-  std::hash_map<TNode, TNode, TNodeHashFunction> cache;
+  std::unordered_map<TNode, TNode, TNodeHashFunction> cache;
   return substitute(node, replacement, cache);
 }
 
 template <bool ref_count>
 Node
 NodeTemplate<ref_count>::substitute(TNode node, TNode replacement,
-                                    std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const {
+                                    std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const {
   Assert(node != *this);
 
   if (getNumChildren() == 0) {
@@ -1311,7 +1311,7 @@ NodeTemplate<ref_count>::substitute(TNode node, TNode replacement,
   }
 
   // in cache?
-  typename std::hash_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this);
+  typename std::unordered_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this);
   if(i != cache.end()) {
     return (*i).second;
   }
@@ -1351,7 +1351,7 @@ NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin,
                                     Iterator1 nodesEnd,
                                     Iterator2 replacementsBegin,
                                     Iterator2 replacementsEnd) const {
-  std::hash_map<TNode, TNode, TNodeHashFunction> cache;
+  std::unordered_map<TNode, TNode, TNodeHashFunction> cache;
   return substitute(nodesBegin, nodesEnd,
                     replacementsBegin, replacementsEnd, cache);
 }
@@ -1363,9 +1363,9 @@ NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin,
                                     Iterator1 nodesEnd,
                                     Iterator2 replacementsBegin,
                                     Iterator2 replacementsEnd,
-                                    std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const {
+                                    std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const {
   // in cache?
-  typename std::hash_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this);
+  typename std::unordered_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this);
   if(i != cache.end()) {
     return (*i).second;
   }
@@ -1410,7 +1410,7 @@ template <class Iterator>
 inline Node
 NodeTemplate<ref_count>::substitute(Iterator substitutionsBegin,
                                     Iterator substitutionsEnd) const {
-  std::hash_map<TNode, TNode, TNodeHashFunction> cache;
+  std::unordered_map<TNode, TNode, TNodeHashFunction> cache;
   return substitute(substitutionsBegin, substitutionsEnd, cache);
 }
 
@@ -1419,9 +1419,9 @@ template <class Iterator>
 Node
 NodeTemplate<ref_count>::substitute(Iterator substitutionsBegin,
                                     Iterator substitutionsEnd,
-                                    std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const {
+                                    std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const {
   // in cache?
-  typename std::hash_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this);
+  typename std::unordered_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this);
   if(i != cache.end()) {
     return (*i).second;
   }
@@ -1468,7 +1468,7 @@ inline Node NodeTemplate<true>::fromExpr(const Expr& e) {
 
 template<bool ref_count>
 bool NodeTemplate<ref_count>::hasSubterm(NodeTemplate<false> t, bool strict) const {
-  typedef std::hash_set<TNode, TNodeHashFunction> node_set;
+  typedef std::unordered_set<TNode, TNodeHashFunction> node_set;
 
   if (!strict && *this == t) {
     return true;
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index f7a1d98d6..e440261cb 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -18,7 +18,6 @@
 #include "expr/node_manager.h"
 
 #include <algorithm>
-#include <ext/hash_set>
 #include <stack>
 #include <utility>
 
@@ -36,7 +35,6 @@
 
 using namespace std;
 using namespace CVC4::expr;
-using __gnu_cxx::hash_set;
 
 namespace CVC4 {
 
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 44c116558..f112381d8 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -30,7 +30,7 @@
 
 #include <vector>
 #include <string>
-#include <ext/hash_set>
+#include <unordered_set>
 
 #include "base/tls.h"
 #include "expr/kind.h"
@@ -95,12 +95,12 @@ class NodeManager {
     bool operator()(expr::NodeValue* nv) { return nv->d_rc > 0; }
   };
 
-  typedef __gnu_cxx::hash_set<expr::NodeValue*,
-                              expr::NodeValuePoolHashFunction,
-                              expr::NodeValuePoolEq> NodeValuePool;
-  typedef __gnu_cxx::hash_set<expr::NodeValue*,
-                              expr::NodeValueIDHashFunction,
-                              expr::NodeValueIDEquality> NodeValueIDSet;
+  typedef std::unordered_set<expr::NodeValue*,
+                             expr::NodeValuePoolHashFunction,
+                             expr::NodeValuePoolEq> NodeValuePool;
+  typedef std::unordered_set<expr::NodeValue*,
+                             expr::NodeValueIDHashFunction,
+                             expr::NodeValueIDEquality> NodeValueIDSet;
 
   static CVC4_THREADLOCAL(NodeManager*) s_current;
 
diff --git a/src/expr/record.h b/src/expr/record.h
index 685756112..7c5854db2 100644
--- a/src/expr/record.h
+++ b/src/expr/record.h
@@ -19,11 +19,11 @@
 #ifndef __CVC4__RECORD_H
 #define __CVC4__RECORD_H
 
+#include <functional>
 #include <iostream>
 #include <string>
 #include <vector>
 #include <utility>
-#include "util/hash.h"
 
 // Forward Declarations
 namespace CVC4 {
@@ -56,13 +56,13 @@ public:
 
 struct CVC4_PUBLIC RecordSelectHashFunction {
   inline size_t operator()(const RecordSelect& t) const {
-    return StringHashFunction()(t.getField());
+    return std::hash<std::string>()(t.getField());
   }
 };/* struct RecordSelectHashFunction */
 
 struct CVC4_PUBLIC RecordUpdateHashFunction {
   inline size_t operator()(const RecordUpdate& t) const {
-    return StringHashFunction()(t.getField());
+    return std::hash<std::string>()(t.getField());
   }
 };/* struct RecordUpdateHashFunction */
 
diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp
index 864ade423..7fd938a9b 100644
--- a/src/expr/symbol_table.cpp
+++ b/src/expr/symbol_table.cpp
@@ -36,8 +36,8 @@ namespace CVC4 {
 
 SymbolTable::SymbolTable() :
   d_context(new Context()),
-  d_exprMap(new(true) CDHashMap<std::string, Expr, StringHashFunction>(d_context)),
-  d_typeMap(new(true) CDHashMap<std::string, pair<vector<Type>, Type>, StringHashFunction>(d_context)),
+  d_exprMap(new(true) CDHashMap<std::string, Expr>(d_context)),
+  d_typeMap(new(true) CDHashMap<std::string, pair<vector<Type>, Type>>(d_context)),
   d_functions(new(true) CDHashSet<Expr, ExprHashFunction>(d_context)) {
 }
 
@@ -74,7 +74,7 @@ bool SymbolTable::isBound(const std::string& name) const throw() {
 }
 
 bool SymbolTable::isBoundDefinedFunction(const std::string& name) const throw() {
-  CDHashMap<std::string, Expr, StringHashFunction>::iterator found =
+  CDHashMap<std::string, Expr>::iterator found =
     d_exprMap->find(name);
   return found != d_exprMap->end() && d_functions->contains((*found).second);
 }
diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h
index cefa65d0a..7c3b13003 100644
--- a/src/expr/symbol_table.h
+++ b/src/expr/symbol_table.h
@@ -21,7 +21,6 @@
 
 #include <vector>
 #include <utility>
-#include <ext/hash_map>
 
 #include "expr/expr.h"
 #include "util/hash.h"
@@ -50,10 +49,11 @@ class CVC4_PUBLIC SymbolTable {
   context::Context* d_context;
 
   /** A map for expressions. */
-  context::CDHashMap<std::string, Expr, StringHashFunction> *d_exprMap;
+  context::CDHashMap<std::string, Expr>* d_exprMap;
 
   /** A map for types. */
-  context::CDHashMap<std::string, std::pair<std::vector<Type>, Type>, StringHashFunction> *d_typeMap;
+  context::CDHashMap<std::string, std::pair<std::vector<Type>, Type> >*
+      d_typeMap;
 
   /** A set of defined functions. */
   context::CDHashSet<Expr, ExprHashFunction> *d_functions;
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 383a31dd0..a4ab2f3b7 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -31,9 +31,9 @@ TypeNode TypeNode::s_null( &expr::NodeValue::null() );
 
 TypeNode TypeNode::substitute(const TypeNode& type,
                               const TypeNode& replacement,
-                              std::hash_map<TypeNode, TypeNode, HashFunction>& cache) const {
+                              std::unordered_map<TypeNode, TypeNode, HashFunction>& cache) const {
   // in cache?
-  std::hash_map<TypeNode, TypeNode, HashFunction>::const_iterator i = cache.find(*this);
+  std::unordered_map<TypeNode, TypeNode, HashFunction>::const_iterator i = cache.find(*this);
   if(i != cache.end()) {
     return (*i).second;
   }
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 8dd80bc37..65b422a53 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -22,11 +22,13 @@
 #ifndef __CVC4__TYPE_NODE_H
 #define __CVC4__TYPE_NODE_H
 
-#include <vector>
-#include <string>
-#include <iostream>
 #include <stdint.h>
 
+#include <iostream>
+#include <string>
+#include <unordered_map>
+#include <vector>
+
 #include "base/cvc4_assert.h"
 #include "expr/kind.h"
 #include "expr/metakind.h"
@@ -93,7 +95,7 @@ private:
    * member function with a similar signature.
    */
   TypeNode substitute(const TypeNode& type, const TypeNode& replacement,
-                      std::hash_map<TypeNode, TypeNode, HashFunction>& cache) const;
+                      std::unordered_map<TypeNode, TypeNode, HashFunction>& cache) const;
 
   /**
    * Cache-aware, recursive version of substitute() used by the public
@@ -102,7 +104,7 @@ private:
   template <class Iterator1, class Iterator2>
   TypeNode substitute(Iterator1 typesBegin, Iterator1 typesEnd,
                       Iterator2 replacementsBegin, Iterator2 replacementsEnd,
-                      std::hash_map<TypeNode, TypeNode, HashFunction>& cache) const;
+                      std::unordered_map<TypeNode, TypeNode, HashFunction>& cache) const;
 
 public:
 
@@ -670,8 +672,6 @@ typedef TypeNode::HashFunction TypeNodeHashFunction;
 
 }/* CVC4 namespace */
 
-#include <ext/hash_map>
-
 #include "expr/node_manager.h"
 
 namespace CVC4 {
@@ -687,7 +687,7 @@ inline TypeNode TypeNode::fromType(const Type& t) {
 inline TypeNode
 TypeNode::substitute(const TypeNode& type,
                      const TypeNode& replacement) const {
-  std::hash_map<TypeNode, TypeNode, HashFunction> cache;
+  std::unordered_map<TypeNode, TypeNode, HashFunction> cache;
   return substitute(type, replacement, cache);
 }
 
@@ -697,7 +697,7 @@ TypeNode::substitute(Iterator1 typesBegin,
                      Iterator1 typesEnd,
                      Iterator2 replacementsBegin,
                      Iterator2 replacementsEnd) const {
-  std::hash_map<TypeNode, TypeNode, HashFunction> cache;
+  std::unordered_map<TypeNode, TypeNode, HashFunction> cache;
   return substitute(typesBegin, typesEnd,
                     replacementsBegin, replacementsEnd, cache);
 }
@@ -707,9 +707,9 @@ TypeNode TypeNode::substitute(Iterator1 typesBegin,
                               Iterator1 typesEnd,
                               Iterator2 replacementsBegin,
                               Iterator2 replacementsEnd,
-                              std::hash_map<TypeNode, TypeNode, HashFunction>& cache) const {
+                              std::unordered_map<TypeNode, TypeNode, HashFunction>& cache) const {
   // in cache?
-  std::hash_map<TypeNode, TypeNode, HashFunction>::const_iterator i = cache.find(*this);
+  std::unordered_map<TypeNode, TypeNode, HashFunction>::const_iterator i = cache.find(*this);
   if(i != cache.end()) {
     return (*i).second;
   }
diff --git a/src/expr/variable_type_map.h b/src/expr/variable_type_map.h
index 739a8d425..94d9c2f67 100644
--- a/src/expr/variable_type_map.h
+++ b/src/expr/variable_type_map.h
@@ -20,8 +20,9 @@
 #ifndef __CVC4__VARIABLE_TYPE_MAP_H
 #define __CVC4__VARIABLE_TYPE_MAP_H
 
+#include <unordered_map>
+
 #include "expr/expr.h"
-#include "util/hash.h"
 
 namespace CVC4 {
 
@@ -35,13 +36,13 @@ class CVC4_PUBLIC VariableTypeMap {
    * A map Expr -> Expr, intended to be used for a mapping of variables
    * between two ExprManagers.
    */
-  std::hash_map<Expr, Expr, ExprHashFunction> d_variables;
+  std::unordered_map<Expr, Expr, ExprHashFunction> d_variables;
 
   /**
    * A map Type -> Type, intended to be used for a mapping of types
    * between two ExprManagers.
    */
-  std::hash_map<Type, Type, TypeHashFunction> d_types;
+  std::unordered_map<Type, Type, TypeHashFunction> d_types;
 
 public:
   Expr& operator[](Expr e) { return d_variables[e]; }
@@ -49,7 +50,7 @@ public:
 
 };/* class VariableTypeMap */
 
-typedef __gnu_cxx::hash_map<uint64_t, uint64_t> VarMap;
+typedef std::unordered_map<uint64_t, uint64_t> VarMap;
 
 struct CVC4_PUBLIC ExprManagerMapCollection {
   VariableTypeMap d_typeMap;
diff --git a/src/parser/smt1/smt1.cpp b/src/parser/smt1/smt1.cpp
index 02f0566a7..c4e670f6d 100644
--- a/src/parser/smt1/smt1.cpp
+++ b/src/parser/smt1/smt1.cpp
@@ -12,21 +12,17 @@
  ** Definitions of SMT-LIB (v1) constants.
  **/
 
-#include <ext/hash_map>
-namespace std {
-  using namespace __gnu_cxx;
-}
+#include "parser/smt1/smt1.h"
 
 #include "expr/type.h"
 #include "smt/command.h"
 #include "parser/parser.h"
-#include "parser/smt1/smt1.h"
 
 namespace CVC4 {
 namespace parser {
 
-std::hash_map<const std::string, Smt1::Logic, CVC4::StringHashFunction> Smt1::newLogicMap() {
-  std::hash_map<const std::string, Smt1::Logic, CVC4::StringHashFunction> logicMap;
+std::unordered_map<std::string, Smt1::Logic> Smt1::newLogicMap() {
+  std::unordered_map<std::string, Smt1::Logic> logicMap;
   logicMap["AUFLIA"] = AUFLIA;
   logicMap["AUFLIRA"] = AUFLIRA;
   logicMap["AUFNIRA"] = AUFNIRA;
@@ -68,7 +64,7 @@ std::hash_map<const std::string, Smt1::Logic, CVC4::StringHashFunction> Smt1::ne
 }
 
 Smt1::Logic Smt1::toLogic(const std::string& name) {
-  static std::hash_map<const std::string, Smt1::Logic, CVC4::StringHashFunction> logicMap = newLogicMap();
+  static std::unordered_map<std::string, Smt1::Logic> logicMap = newLogicMap();
   return logicMap[name];
 }
 
diff --git a/src/parser/smt1/smt1.h b/src/parser/smt1/smt1.h
index 7036aad64..e9dbea1a9 100644
--- a/src/parser/smt1/smt1.h
+++ b/src/parser/smt1/smt1.h
@@ -17,10 +17,9 @@
 #ifndef __CVC4__PARSER__SMT1_H
 #define __CVC4__PARSER__SMT1_H
 
-#include <ext/hash_map>
-namespace std { using namespace __gnu_cxx; }
+#include <string>
+#include <unordered_map>
 
-#include "util/hash.h"
 #include "parser/parser.h"
 
 namespace CVC4 {
@@ -117,7 +116,7 @@ public:
 private:
 
   void addArithmeticOperators();
-  static std::hash_map<const std::string, Logic, CVC4::StringHashFunction> newLogicMap();
+  static std::unordered_map<std::string, Logic> newLogicMap();
 };/* class Smt1 */
 
 }/* CVC4::parser namespace */
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 88709c29a..c7156635d 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -117,6 +117,7 @@ namespace CVC4 {
 #include <set>
 #include <sstream>
 #include <string>
+#include <unordered_set>
 #include <vector>
 
 #include "base/output.h"
@@ -150,7 +151,7 @@ using namespace CVC4::parser;
 #define MK_CONST EXPR_MANAGER->mkConst
 #define UNSUPPORTED PARSER_STATE->unimplementedFeature
 
-static bool isClosed(const Expr& e, std::set<Expr>& free, std::hash_set<Expr, ExprHashFunction>& closedCache) {
+static bool isClosed(const Expr& e, std::set<Expr>& free, std::unordered_set<Expr, ExprHashFunction>& closedCache) {
   if(closedCache.find(e) != closedCache.end()) {
     return true;
   }
@@ -181,7 +182,7 @@ static bool isClosed(const Expr& e, std::set<Expr>& free, std::hash_set<Expr, Ex
 }
 
 static inline bool isClosed(const Expr& e, std::set<Expr>& free) {
-  std::hash_set<Expr, ExprHashFunction> cache;
+  std::unordered_set<Expr, ExprHashFunction> cache;
   return isClosed(e, free, cache);
 }  
   
@@ -898,7 +899,7 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun]
         sgt.d_gterm_type = SygusGTerm::gterm_op;
         sgt.d_expr = EXPR_MANAGER->operatorOf(k);
       }
-     | LET_TOK LPAREN_TOK { 
+     | SYGUS_LET_TOK LPAREN_TOK { 
          sgt.d_name = std::string("let");
          sgt.d_gterm_type = SygusGTerm::gterm_let;
          PARSER_STATE->pushScope(true);
@@ -1798,12 +1799,11 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
   Expr attexpr;
   std::vector<Expr> patexprs;
   std::vector<Expr> patconds;
-  std::hash_set<std::string, StringHashFunction> names;
+  std::unordered_set<std::string> names;
   std::vector< std::pair<std::string, Expr> > binders;
   Type type;
   std::string s;
   bool isBuiltinOperator = false;
-  bool readLetSort = false;
   int match_vindex = -1;
   std::vector<Type> match_ptypes;
 }
@@ -2005,27 +2005,41 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
         expr = MK_CONST( ::CVC4::ArrayStoreAll(type, f) );
       }
     )
-  | /* a let binding */
-    LPAREN_TOK LET_TOK LPAREN_TOK
-    { PARSER_STATE->pushScope(true); }
-    ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE]
-      (term[expr, f2] | sortSymbol[type,CHECK_DECLARED]
-       { readLetSort = true; } term[expr, f2]
-      )
-      RPAREN_TOK
-      // this is a parallel let, so we have to save up all the contributions
-      // of the let and define them only later on
-      { if( !PARSER_STATE->sygus() && readLetSort ){
-          PARSER_STATE->parseError("Bad syntax for let term.");
-        }else if(names.count(name) == 1) {
-          std::stringstream ss;
-          ss << "warning: symbol `" << name << "' bound multiple times by let;"
-             << " the last binding will be used, shadowing earlier ones";
-          PARSER_STATE->warning(ss.str());
-        } else {
-          names.insert(name);
-        }
-        binders.push_back(std::make_pair(name, expr)); } )+
+  | /* a let or sygus let binding */
+    LPAREN_TOK ( 
+      LET_TOK LPAREN_TOK
+      { PARSER_STATE->pushScope(true); }
+      ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE]
+        term[expr, f2]
+        RPAREN_TOK
+        // this is a parallel let, so we have to save up all the contributions
+        // of the let and define them only later on
+        { if(names.count(name) == 1) {
+            std::stringstream ss;
+            ss << "warning: symbol `" << name << "' bound multiple times by let;"
+               << " the last binding will be used, shadowing earlier ones";
+            PARSER_STATE->warning(ss.str());
+          } else {
+            names.insert(name);
+          }
+          binders.push_back(std::make_pair(name, expr)); } )+ |
+      SYGUS_LET_TOK LPAREN_TOK
+      { PARSER_STATE->pushScope(true); }
+      ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE]
+        sortSymbol[type,CHECK_DECLARED]
+        term[expr, f2]
+        RPAREN_TOK
+        // this is a parallel let, so we have to save up all the contributions
+        // of the let and define them only later on
+        { if(names.count(name) == 1) {
+            std::stringstream ss;
+            ss << "warning: symbol `" << name << "' bound multiple times by let;"
+               << " the last binding will be used, shadowing earlier ones";
+            PARSER_STATE->warning(ss.str());
+          } else {
+            names.insert(name);
+          }
+          binders.push_back(std::make_pair(name, expr)); } )+ )
     { // now implement these bindings
       for(std::vector< std::pair<std::string, Expr> >::iterator
             i = binders.begin(); i != binders.end(); ++i) {
@@ -3004,7 +3018,8 @@ EXIT_TOK : 'exit';
 RESET_TOK : { PARSER_STATE->v2_5(false) }? 'reset';
 RESET_ASSERTIONS_TOK : 'reset-assertions';
 ITE_TOK : 'ite';
-LET_TOK : 'let';
+LET_TOK : { !PARSER_STATE->sygus() }? 'let';
+SYGUS_LET_TOK : { PARSER_STATE->sygus() }? 'let';
 ATTRIBUTE_TOK : '!';
 LPAREN_TOK : '(';
 RPAREN_TOK : ')';
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 3eed0e871..e470c8111 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -22,6 +22,7 @@
 #include <sstream>
 #include <stack>
 #include <string>
+#include <unordered_map>
 #include <utility>
 
 #include "parser/parser.h"
@@ -58,7 +59,7 @@ public:
 private:
   bool d_logicSet;
   LogicInfo d_logic;
-  std::hash_map<std::string, Kind, StringHashFunction> operatorKindMap;
+  std::unordered_map<std::string, Kind> operatorKindMap;
   std::pair<Expr, std::string> d_lastNamedTerm;
   // this is a user-context stack
   std::stack< std::map<Expr, std::string> > d_unsatCoreNames;
diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h
index f137a9d92..3afd29415 100644
--- a/src/parser/tptp/tptp.h
+++ b/src/parser/tptp/tptp.h
@@ -22,7 +22,8 @@
 #define __CVC4__PARSER__TPTP_H
 
 #include <cassert>
-#include <ext/hash_set>
+#include <unordered_map>
+#include <unordered_set>
 
 #include "parser/parser.h"
 #include "smt/command.h"
@@ -45,8 +46,8 @@ class Tptp : public Parser {
   Expr d_utr_op;
   Expr d_uts_op;
   // The set of expression that already have a bridge
-  std::hash_set<Expr, ExprHashFunction> d_r_converted;
-  std::hash_map<std::string, Expr, StringHashFunction> d_distinct_objects;
+  std::unordered_set<Expr, ExprHashFunction> d_r_converted;
+  std::unordered_map<std::string, Expr> d_distinct_objects;
   
   std::vector< pANTLR3_INPUT_STREAM > d_in_created;
 
diff --git a/src/printer/dagification_visitor.h b/src/printer/dagification_visitor.h
index 1f89d36f6..6cbe5f863 100644
--- a/src/printer/dagification_visitor.h
+++ b/src/printer/dagification_visitor.h
@@ -19,12 +19,13 @@
 #ifndef __CVC4__PRINTER__DAGIFICATION_VISITOR_H
 #define __CVC4__PRINTER__DAGIFICATION_VISITOR_H
 
+#include <string>
+#include <unordered_map>
+#include <vector>
+
 #include "expr/node.h"
 #include "util/hash.h"
 
-#include <vector>
-#include <string>
-
 namespace CVC4 {
 
 namespace context {
@@ -65,7 +66,7 @@ class DagificationVisitor {
   /**
    * A map of subexprs to their occurrence count.
    */
-  std::hash_map<TNode, unsigned, TNodeHashFunction> d_nodeCount;
+  std::unordered_map<TNode, unsigned, TNodeHashFunction> d_nodeCount;
 
   /**
    * The top-most node we are visiting.
@@ -109,7 +110,7 @@ class DagificationVisitor {
    * in independently dagifying the child.  (If it is beyond the threshold
    * and occurs in more than one parent, we'll independently dagify.)
    */
-  std::hash_map<TNode, TNode, TNodeHashFunction> d_uniqueParent;
+  std::unordered_map<TNode, TNode, TNodeHashFunction> d_uniqueParent;
 
   /**
    * A list of all nodes that meet the occurrence threshold and therefore
diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h
index a3868fe46..3de53f866 100644
--- a/src/proof/arith_proof.h
+++ b/src/proof/arith_proof.h
@@ -19,6 +19,8 @@
 #ifndef __CVC4__ARITH__PROOF_H
 #define __CVC4__ARITH__PROOF_H
 
+#include <unordered_set>
+
 #include "expr/expr.h"
 #include "proof/proof_manager.h"
 #include "proof/theory_proof.h"
@@ -45,7 +47,7 @@ class TheoryArith;
 }
 }
 
-typedef __gnu_cxx::hash_set<Type, TypeHashFunction > TypeSet;
+typedef std::unordered_set<Type, TypeHashFunction > TypeSet;
 
 
 class ArithProof : public TheoryProof {
diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h
index 507b65fef..9a2eef9e7 100644
--- a/src/proof/array_proof.h
+++ b/src/proof/array_proof.h
@@ -19,6 +19,8 @@
 #ifndef __CVC4__ARRAY__PROOF_H
 #define __CVC4__ARRAY__PROOF_H
 
+#include <unordered_set>
+
 #include "expr/expr.h"
 #include "proof/proof_manager.h"
 #include "proof/theory_proof.h"
@@ -94,7 +96,7 @@ class TheoryArrays;
 } /* namespace CVC4::theory::arrays */
 } /* namespace CVC4::theory */
 
-typedef __gnu_cxx::hash_set<Type, TypeHashFunction > TypeSet;
+typedef std::unordered_set<Type, TypeHashFunction > TypeSet;
 
 class ArrayProof : public TheoryProof {
   // TODO: whatever goes in this theory
diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h
index 4c390e86f..69f9e774b 100644
--- a/src/proof/bitvector_proof.h
+++ b/src/proof/bitvector_proof.h
@@ -19,12 +19,11 @@
 #ifndef __CVC4__BITVECTOR__PROOF_H
 #define __CVC4__BITVECTOR__PROOF_H
 
-//#include <cstdint>
-#include <ext/hash_map>
-#include <ext/hash_set>
 #include <iostream>
 #include <set>
 #include <sstream>
+#include <unordered_map>
+#include <unordered_set>
 #include <vector>
 
 #include "expr/expr.h"
@@ -56,11 +55,11 @@ typedef TSatProof< CVC4::BVMinisat::Solver> BVSatProof;
 template <class Solver> class LFSCSatProof;
 typedef LFSCSatProof< CVC4::BVMinisat::Solver> LFSCBVSatProof;
 
-typedef __gnu_cxx::hash_set<Expr, ExprHashFunction> ExprSet;
-typedef __gnu_cxx::hash_map<Expr, ClauseId, ExprHashFunction> ExprToClauseId;
-typedef __gnu_cxx::hash_map<Expr, unsigned, ExprHashFunction> ExprToId;
-typedef __gnu_cxx::hash_map<Expr, Expr, ExprHashFunction> ExprToExpr;
-typedef __gnu_cxx::hash_map<Expr, std::string, ExprHashFunction> ExprToString;
+typedef std::unordered_set<Expr, ExprHashFunction> ExprSet;
+typedef std::unordered_map<Expr, ClauseId, ExprHashFunction> ExprToClauseId;
+typedef std::unordered_map<Expr, unsigned, ExprHashFunction> ExprToId;
+typedef std::unordered_map<Expr, Expr, ExprHashFunction> ExprToExpr;
+typedef std::unordered_map<Expr, std::string, ExprHashFunction> ExprToString;
 
 class BitVectorProof : public TheoryProof {
 protected:
diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h
index 0cc0bf93e..a0d7096c0 100644
--- a/src/proof/cnf_proof.h
+++ b/src/proof/cnf_proof.h
@@ -21,9 +21,9 @@
 #ifndef __CVC4__CNF_PROOF_H
 #define __CVC4__CNF_PROOF_H
 
-#include <ext/hash_map>
-#include <ext/hash_set>
 #include <iosfwd>
+#include <unordered_map>
+#include <unordered_set>
 
 #include "context/cdhashmap.h"
 #include "proof/clause_id.h"
@@ -38,9 +38,9 @@ namespace prop {
 
 class CnfProof;
 
-typedef __gnu_cxx::hash_map<prop::SatVariable, Expr> SatVarToExpr;
-typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeToNode;
-typedef __gnu_cxx::hash_set<ClauseId> ClauseIdSet;
+typedef std::unordered_map<prop::SatVariable, Expr> SatVarToExpr;
+typedef std::unordered_map<Node, Node, NodeHashFunction> NodeToNode;
+typedef std::unordered_set<ClauseId> ClauseIdSet;
 
 typedef context::CDHashMap<ClauseId, Node> ClauseIdToNode;
 typedef context::CDHashMap<Node, ProofRule, NodeHashFunction> NodeToProofRule;
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index 2510b770a..f77a96726 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -20,7 +20,9 @@
 #define __CVC4__PROOF_MANAGER_H
 
 #include <iosfwd>
-#include <map>
+#include <unordered_map>
+#include <unordered_set>
+
 #include "expr/node.h"
 #include "context/cdhashset.h"
 #include "context/cdhashmap.h"
@@ -96,13 +98,11 @@ enum ProofFormat {
 
 std::string append(const std::string& str, uint64_t num);
 
-typedef __gnu_cxx::hash_map < ClauseId, prop::SatClause* > IdToSatClause;
-typedef __gnu_cxx::hash_set<Expr, ExprHashFunction> ExprSet;
+typedef std::unordered_map<ClauseId, prop::SatClause*> IdToSatClause;
 typedef context::CDHashSet<Expr, ExprHashFunction> CDExprSet;
-typedef __gnu_cxx::hash_set<Node, NodeHashFunction > NodeSet;
-typedef __gnu_cxx::hash_map<Node, std::vector<Node>, NodeHashFunction > NodeToNodes;
-typedef context::CDHashMap<Node, std::vector<Node>, NodeHashFunction > CDNodeToNodes;
-typedef std::hash_set<ClauseId> IdHashSet;
+typedef std::unordered_map<Node, std::vector<Node>, NodeHashFunction> NodeToNodes;
+typedef context::CDHashMap<Node, std::vector<Node>, NodeHashFunction> CDNodeToNodes;
+typedef std::unordered_set<ClauseId> IdHashSet;
 
 enum ProofRule {
   RULE_GIVEN,       /* input assertion */
diff --git a/src/proof/proof_output_channel.h b/src/proof/proof_output_channel.h
index 74d159bec..b114ec25f 100644
--- a/src/proof/proof_output_channel.h
+++ b/src/proof/proof_output_channel.h
@@ -16,6 +16,8 @@
 #ifndef __CVC4__PROOF_OUTPUT_CHANNEL_H
 #define __CVC4__PROOF_OUTPUT_CHANNEL_H
 
+#include <unordered_set>
+
 #include "theory/output_channel.h"
 
 namespace CVC4 {
@@ -42,7 +44,7 @@ public:
 
 class MyPreRegisterVisitor {
   theory::Theory* d_theory;
-  __gnu_cxx::hash_set<TNode, TNodeHashFunction> d_visited;
+  std::unordered_set<TNode, TNodeHashFunction> d_visited;
 public:
   typedef void return_type;
   MyPreRegisterVisitor(theory::Theory* theory);
diff --git a/src/proof/proof_utils.h b/src/proof/proof_utils.h
index d7ac80fc8..7c0660a83 100644
--- a/src/proof/proof_utils.h
+++ b/src/proof/proof_utils.h
@@ -20,14 +20,16 @@
 #pragma once
 
 #include <set>
-#include <vector>
 #include <sstream>
+#include <unordered_set>
+#include <vector>
+
 #include "expr/node_manager.h"
 
 namespace CVC4 {
 
-typedef __gnu_cxx::hash_set<Expr, ExprHashFunction> ExprSet;
-typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
+typedef std::unordered_set<Expr, ExprHashFunction> ExprSet;
+typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
 
 typedef std::pair<Node, Node> NodePair;
 typedef std::set<NodePair> NodePairSet;
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index 7c9631896..6b2b39fd4 100644
--- a/src/proof/sat_proof.h
+++ b/src/proof/sat_proof.h
@@ -21,11 +21,10 @@
 
 #include <stdint.h>
 
-#include <ext/hash_map>
-#include <ext/hash_set>
 #include <iosfwd>
 #include <set>
 #include <sstream>
+#include <unordered_map>
 #include <vector>
 
 #include "context/cdhashmap.h"
@@ -101,18 +100,18 @@ class TSatProof {
 
   typedef std::set<typename Solver::TLit> LitSet;
   typedef std::set<typename Solver::TVar> VarSet;
-  typedef std::hash_map<ClauseId, typename Solver::TCRef> IdCRefMap;
-  typedef std::hash_map<typename Solver::TCRef, ClauseId> ClauseIdMap;
+  typedef std::unordered_map<ClauseId, typename Solver::TCRef> IdCRefMap;
+  typedef std::unordered_map<typename Solver::TCRef, ClauseId> ClauseIdMap;
   typedef context::CDHashMap<ClauseId, typename Solver::TLit> IdUnitMap;
   typedef context::CDHashMap<int, ClauseId> UnitIdMap;
   typedef context::CDHashMap<ClauseId, ResolutionChain*> IdResMap;
-  typedef std::hash_map<ClauseId, uint64_t> IdProofRuleMap;
+  typedef std::unordered_map<ClauseId, uint64_t> IdProofRuleMap;
   typedef std::vector<ResolutionChain*> ResStack;
   typedef std::set<ClauseId> IdSet;
   typedef std::vector<typename Solver::TLit> LitVector;
-  typedef __gnu_cxx::hash_map<ClauseId, typename Solver::TClause&>
+  typedef std::unordered_map<ClauseId, typename Solver::TClause&>
       IdToMinisatClause;
-  typedef __gnu_cxx::hash_map<ClauseId, LitVector*> IdToConflicts;
+  typedef std::unordered_map<ClauseId, LitVector*> IdToConflicts;
 
  public:
   TSatProof(Solver* solver, context::Context* context,
@@ -362,7 +361,7 @@ class TSatProof {
   IdToSatClause d_seenLemmas;
 
    private:
-  __gnu_cxx::hash_map<ClauseId, int> d_glueMap;
+  std::unordered_map<ClauseId, int> d_glueMap;
   struct Statistics {
     IntStat d_numLearnedClauses;
     IntStat d_numLearnedInProof;
diff --git a/src/proof/skolemization_manager.cpp b/src/proof/skolemization_manager.cpp
index 2234b7b19..a666e23d3 100644
--- a/src/proof/skolemization_manager.cpp
+++ b/src/proof/skolemization_manager.cpp
@@ -57,11 +57,11 @@ void SkolemizationManager::clear() {
   d_skolemToDisequality.clear();
 }
 
-std::hash_map<Node, Node, NodeHashFunction>::const_iterator SkolemizationManager::begin() {
+std::unordered_map<Node, Node, NodeHashFunction>::const_iterator SkolemizationManager::begin() {
   return d_disequalityToSkolem.begin();
 }
 
-std::hash_map<Node, Node, NodeHashFunction>::const_iterator SkolemizationManager::end() {
+std::unordered_map<Node, Node, NodeHashFunction>::const_iterator SkolemizationManager::end() {
   return d_disequalityToSkolem.end();
 }
 
diff --git a/src/proof/skolemization_manager.h b/src/proof/skolemization_manager.h
index 02aa6b6f0..7ec594859 100644
--- a/src/proof/skolemization_manager.h
+++ b/src/proof/skolemization_manager.h
@@ -21,7 +21,8 @@
 #define __CVC4__SKOLEMIZATION_MANAGER_H
 
 #include <iostream>
-#include <map>
+#include <unordered_map>
+
 #include "proof/proof.h"
 #include "util/proof.h"
 #include "expr/node.h"
@@ -39,12 +40,12 @@ public:
   bool isSkolem(Node skolem);
   void clear();
 
-  std::hash_map<Node, Node, NodeHashFunction>::const_iterator begin();
-  std::hash_map<Node, Node, NodeHashFunction>::const_iterator end();
+  std::unordered_map<Node, Node, NodeHashFunction>::const_iterator begin();
+  std::unordered_map<Node, Node, NodeHashFunction>::const_iterator end();
 
 private:
-  std::hash_map<Node, Node, NodeHashFunction> d_disequalityToSkolem;
-  std::hash_map<Node, Node, NodeHashFunction> d_skolemToDisequality;
+  std::unordered_map<Node, Node, NodeHashFunction> d_disequalityToSkolem;
+  std::unordered_map<Node, Node, NodeHashFunction> d_skolemToDisequality;
 };
 
 }/* CVC4 namespace */
diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h
index 541e4ce82..15ac533b7 100644
--- a/src/proof/theory_proof.h
+++ b/src/proof/theory_proof.h
@@ -20,8 +20,9 @@
 #ifndef __CVC4__THEORY_PROOF_H
 #define __CVC4__THEORY_PROOF_H
 
-#include <ext/hash_set>
 #include <iosfwd>
+#include <unordered_map>
+#include <unordered_set>
 
 #include "expr/expr.h"
 #include "proof/clause_id.h"
@@ -35,11 +36,11 @@ namespace theory {
 class Theory;
 } /* namespace CVC4::theory */
 
-typedef __gnu_cxx::hash_map < ClauseId, prop::SatClause* > IdToSatClause;
+typedef std::unordered_map < ClauseId, prop::SatClause* > IdToSatClause;
 
 class TheoryProof;
 
-typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet;
+typedef std::unordered_set<Expr, ExprHashFunction > ExprSet;
 typedef std::map<theory::TheoryId, TheoryProof* > TheoryProofTable;
 
 typedef std::set<theory::TheoryId> TheoryIdSet;
diff --git a/src/proof/uf_proof.h b/src/proof/uf_proof.h
index 1fb1c4683..b817ceb69 100644
--- a/src/proof/uf_proof.h
+++ b/src/proof/uf_proof.h
@@ -19,6 +19,8 @@
 #ifndef __CVC4__UF__PROOF_H
 #define __CVC4__UF__PROOF_H
 
+#include <unordered_set>
+
 #include "expr/expr.h"
 #include "proof/proof_manager.h"
 #include "theory/uf/equality_engine.h"
@@ -45,7 +47,7 @@ class TheoryUF;
 }
 }
 
-typedef __gnu_cxx::hash_set<Type, TypeHashFunction > TypeSet;
+typedef std::unordered_set<Type, TypeHashFunction > TypeSet;
 
 
 class UFProof : public TheoryProof {
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index d626a5d15..0213ef7e3 100644
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -990,7 +990,7 @@ lbool Solver::search(int nof_conflicts, UIP uip)
               if(d_bvp){
                  ClauseId id = d_bvp->getSatProof()->registerClause(cr, LEARNT);
                  PSTATS(
-                 __gnu_cxx::hash_set<int> cl_levels;
+                 std::unordered_set<int> cl_levels;
                  for (int i = 0; i < learnt_clause.size(); ++i) {
                    cl_levels.insert(level(var(learnt_clause[i])));
                  }
diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h
index 555495149..485eb8535 100644
--- a/src/prop/bvminisat/core/Solver.h
+++ b/src/prop/bvminisat/core/Solver.h
@@ -21,7 +21,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef BVMinisat_Solver_h
 #define BVMinisat_Solver_h
 
-#include <ext/hash_set>
 #include <vector>
 
 #include "context/context.h"
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index affcc2999..80f8742a3 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -25,8 +25,6 @@
 #ifndef __CVC4__PROP__CNF_STREAM_H
 #define __CVC4__PROP__CNF_STREAM_H
 
-#include <ext/hash_map>
-
 #include "context/cdinsert_hashmap.h"
 #include "context/cdlist.h"
 #include "expr/node.h"
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 0bf5d5d7c..2b58f2f17 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -23,6 +23,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <math.h>
 
 #include <iostream>
+#include <unordered_set>
 
 #include "base/output.h"
 #include "options/prop_options.h"
@@ -1219,7 +1220,7 @@ lbool Solver::search(int nof_conflicts)
                 PROOF(
                       ClauseId id = ProofManager::getSatProof()->registerClause(cr, LEARNT);
                       PSTATS(
-                      __gnu_cxx::hash_set<int> cl_levels;
+                      std::unordered_set<int> cl_levels;
                       for (int i = 0; i < learnt_clause.size(); ++i) {
                         cl_levels.insert(level(var(learnt_clause[i])));
                       }
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index 510a12eb2..67d3b3b7e 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -24,6 +24,7 @@
 #define __CVC4_USE_MINISAT
 
 #include <iosfwd>
+#include <unordered_set>
 
 #include "context/cdqueue.h"
 #include "expr/expr_stream.h"
@@ -138,7 +139,7 @@ public:
    * Set of all lemmas that have been "shared" in the portfolio---i.e.,
    * all imported and exported lemmas.
    */
-  std::hash_set<Node, NodeHashFunction> d_shared;
+  std::unordered_set<Node, NodeHashFunction> d_shared;
 
   /**
    * Statistic: the number of replayed decisions (via --replay).
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 327f978e4..704303826 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -18,7 +18,8 @@
 
 #include <algorithm>
 #include <cctype>
-#include <ext/hash_map>
+#include <unordered_map>
+#include <unordered_set>
 #include <iterator>
 #include <sstream>
 #include <stack>
@@ -463,8 +464,8 @@ class PrintSuccessListener : public Listener {
 class SmtEnginePrivate : public NodeManagerListener {
   SmtEngine& d_smt;
 
-  typedef hash_map<Node, Node, NodeHashFunction> NodeToNodeHashMap;
-  typedef hash_map<Node, bool, NodeHashFunction> NodeToBoolHashMap;
+  typedef unordered_map<Node, Node, NodeHashFunction> NodeToNodeHashMap;
+  typedef unordered_map<Node, bool, NodeHashFunction> NodeToBoolHashMap;
 
   /**
    * Manager for limiting time and abstract resource usage.
@@ -634,7 +635,7 @@ private:
    * conjuncts.
    */
   size_t removeFromConjunction(Node& n,
-                               const std::hash_set<unsigned long>& toRemove);
+                               const std::unordered_set<unsigned long>& toRemove);
 
   /** Scrub miplib encodings. */
   void doMiplibTrick();
@@ -794,9 +795,7 @@ public:
     }
   }
 
-  void nmNotifyDeleteNode(TNode n) {
-    d_smt.d_smtAttributes->deleteAllAttributes(n);
-  }
+  void nmNotifyDeleteNode(TNode n) {}
 
   Node applySubstitutions(TNode node) const {
     return Rewriter::rewrite(d_topLevelSubstitutions.apply(node));
@@ -981,14 +980,12 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
   d_status(),
   d_replayStream(NULL),
   d_private(NULL),
-  d_smtAttributes(NULL),
   d_statisticsRegistry(NULL),
   d_stats(NULL),
   d_channels(new LemmaChannels())
 {
   SmtScope smts(this);
   d_originalOptions.copyValues(em->getOptions());
-  d_smtAttributes = new expr::attr::SmtAttributes(d_context);
   d_private = new smt::SmtEnginePrivate(*this);
   d_statisticsRegistry = new StatisticsRegistry();
   d_stats = new SmtEngineStatistics();
@@ -1204,9 +1201,6 @@ SmtEngine::~SmtEngine() throw() {
     delete d_private;
     d_private = NULL;
 
-    delete d_smtAttributes;
-    d_smtAttributes = NULL;
-
     delete d_userContext;
     d_userContext = NULL;
     delete d_context;
@@ -2262,7 +2256,7 @@ bool SmtEngine::isDefinedFunction( Expr func ){
   return d_definedFunctions->find(nf) != d_definedFunctions->end();
 }
 
-Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache, bool expandOnly)
+Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, NodeHashFunction>& cache, bool expandOnly)
   throw(TypeCheckingException, LogicException, UnsafeInterruptException) {
 
   stack< triple<Node, Node, bool> > worklist;
@@ -2302,7 +2296,7 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
       }
 
       // maybe it's in the cache
-      hash_map<Node, Node, NodeHashFunction>::iterator cacheHit = cache.find(n);
+      unordered_map<Node, Node, NodeHashFunction>::iterator cacheHit = cache.find(n);
       if(cacheHit != cache.end()) {
         TNode ret = (*cacheHit).second;
         result.push(ret.isNull() ? n : ret);
@@ -2434,7 +2428,7 @@ struct intToBV_stack_element {
   : node(node), children_added(false) {}
 };/* struct intToBV_stack_element */
 
-typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
+typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
 
 Node SmtEnginePrivate::intToBVMakeBinary(TNode n, NodeMap& cache) {
   // Do a topological sort of the subexpressions and substitute them
@@ -3038,7 +3032,7 @@ bool SmtEnginePrivate::nonClausalSimplify() {
   Trace("simplify") << "Resize non-clausal learned literals to " << j << std::endl;
   d_nonClausalLearnedLiterals.resize(j);
 
-  hash_set<TNode, TNodeHashFunction> s;
+  unordered_set<TNode, TNodeHashFunction> s;
   Trace("debugging") << "NonClausal simplify pre-preprocess\n";
   for (unsigned i = 0; i < d_assertions.size(); ++ i) {
     Node assertion = d_assertions[i];
@@ -3273,7 +3267,7 @@ void SmtEnginePrivate::traceBackToAssertions(const std::vector<Node>& nodes, std
   }
 }
 
-size_t SmtEnginePrivate::removeFromConjunction(Node& n, const std::hash_set<unsigned long>& toRemove) {
+size_t SmtEnginePrivate::removeFromConjunction(Node& n, const std::unordered_set<unsigned long>& toRemove) {
   Assert(n.getKind() == kind::AND);
   size_t removals = 0;
   for(Node::iterator j = n.begin(); j != n.end(); ++j) {
@@ -3327,12 +3321,12 @@ void SmtEnginePrivate::doMiplibTrick() {
   Assert(!options::incrementalSolving());
 
   const booleans::CircuitPropagator::BackEdgesMap& backEdges = d_propagator.getBackEdges();
-  hash_set<unsigned long> removeAssertions;
+  unordered_set<unsigned long> removeAssertions;
 
   NodeManager* nm = NodeManager::currentNM();
   Node zero = nm->mkConst(Rational(0)), one = nm->mkConst(Rational(1));
 
-  hash_map<TNode, Node, TNodeHashFunction> intVars;
+  unordered_map<TNode, Node, TNodeHashFunction> intVars;
   for(vector<Node>::const_iterator i = d_boolVars.begin(); i != d_boolVars.end(); ++i) {
     if(d_propagator.isAssigned(*i)) {
       Debug("miplib") << "ineligible: " << *i << " because assigned " << d_propagator.getAssignment(*i) << endl;
@@ -3826,9 +3820,9 @@ Result SmtEngine::quickCheck() {
 }
 
 
-void SmtEnginePrivate::collectSkolems(TNode n, set<TNode>& skolemSet, hash_map<Node, bool, NodeHashFunction>& cache)
+void SmtEnginePrivate::collectSkolems(TNode n, set<TNode>& skolemSet, unordered_map<Node, bool, NodeHashFunction>& cache)
 {
-  hash_map<Node, bool, NodeHashFunction>::iterator it;
+  unordered_map<Node, bool, NodeHashFunction>::iterator it;
   it = cache.find(n);
   if (it != cache.end()) {
     return;
@@ -3852,9 +3846,9 @@ void SmtEnginePrivate::collectSkolems(TNode n, set<TNode>& skolemSet, hash_map<N
 }
 
 
-bool SmtEnginePrivate::checkForBadSkolems(TNode n, TNode skolem, hash_map<Node, bool, NodeHashFunction>& cache)
+bool SmtEnginePrivate::checkForBadSkolems(TNode n, TNode skolem, unordered_map<Node, bool, NodeHashFunction>& cache)
 {
-  hash_map<Node, bool, NodeHashFunction>::iterator it;
+  unordered_map<Node, bool, NodeHashFunction>::iterator it;
   it = cache.find(n);
   if (it != cache.end()) {
     return (*it).second;
@@ -3925,7 +3919,7 @@ void SmtEnginePrivate::processAssertions() {
     Chat() << "expanding definitions..." << endl;
     Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl;
     TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_definitionExpansionTime);
-    hash_map<Node, Node, NodeHashFunction> cache;
+    unordered_map<Node, Node, NodeHashFunction> cache;
     for(unsigned i = 0; i < d_assertions.size(); ++ i) {
       d_assertions.replace(i, expandDefinitions(d_assertions[i], cache));
     }
@@ -3944,8 +3938,8 @@ void SmtEnginePrivate::processAssertions() {
   Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
 
   if( options::nlExtPurify() ){
-    hash_map<Node, Node, NodeHashFunction> cache;
-    hash_map<Node, Node, NodeHashFunction> bcache;
+    unordered_map<Node, Node, NodeHashFunction> cache;
+    unordered_map<Node, Node, NodeHashFunction> bcache;
     std::vector< Node > var_eq;
     for (unsigned i = 0; i < d_assertions.size(); ++ i) {
       d_assertions.replace(i, purifyNlTerms(d_assertions[i], cache, bcache, var_eq));
@@ -3966,7 +3960,7 @@ void SmtEnginePrivate::processAssertions() {
 
   if (options::solveRealAsInt()) {
     Chat() << "converting reals to ints..." << endl;
-    hash_map<Node, Node, NodeHashFunction> cache;
+    unordered_map<Node, Node, NodeHashFunction> cache;
     std::vector< Node > var_eq;
     for(unsigned i = 0; i < d_assertions.size(); ++ i) {
       d_assertions.replace(i, realToInt(d_assertions[i], cache, var_eq));
@@ -3982,7 +3976,7 @@ void SmtEnginePrivate::processAssertions() {
 
   if (options::solveIntAsBV() > 0) {
     Chat() << "converting ints to bit-vectors..." << endl;
-    hash_map<Node, Node, NodeHashFunction> cache;
+    unordered_map<Node, Node, NodeHashFunction> cache;
     for(unsigned i = 0; i < d_assertions.size(); ++ i) {
       d_assertions.replace(i, intToBV(d_assertions[i], cache));
     }
@@ -4210,7 +4204,7 @@ void SmtEnginePrivate::processAssertions() {
       // For each skolem variable sk, let iteExpr = iteMap(sk) be the ite expr mapped to by sk.
 
       // cache for expression traversal
-      hash_map<Node, bool, NodeHashFunction> cache;
+      unordered_map<Node, bool, NodeHashFunction> cache;
 
       // First, find all skolems that appear in the substitution map - their associated iteExpr will need
       // to be moved to the main assertion set
@@ -4663,7 +4657,7 @@ Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, L
   if(Dump.isOn("benchmark")) {
     Dump("benchmark") << ExpandDefinitionsCommand(e);
   }
-  hash_map<Node, Node, NodeHashFunction> cache;
+  unordered_map<Node, Node, NodeHashFunction> cache;
   Node n = d_private->expandDefinitions(Node::fromExpr(e), cache, /* expandOnly = */ true);
   n = postprocess(n, TypeNode::fromType(e.getType()));
 
@@ -4708,7 +4702,7 @@ Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckin
   TypeNode expectedType = n.getType();
 
   // Expand, then normalize
-  hash_map<Node, Node, NodeHashFunction> cache;
+  unordered_map<Node, Node, NodeHashFunction> cache;
   n = d_private->expandDefinitions(n, cache);
   // There are two ways model values for terms are computed (for historical
   // reasons).  One way is that used in check-model; the other is that
@@ -4821,7 +4815,7 @@ CVC4::SExpr SmtEngine::getAssignment() {
     Trace("smt") << "--- getting value of " << *i << endl;
 
     // Expand, then normalize
-    hash_map<Node, Node, NodeHashFunction> cache;
+    unordered_map<Node, Node, NodeHashFunction> cache;
     Node n = d_private->expandDefinitions(*i, cache);
     n = Rewriter::rewrite(n);
 
@@ -5063,7 +5057,7 @@ void SmtEngine::checkModel(bool hardFailure) {
 
     // Apply any define-funs from the problem.
     {
-      hash_map<Node, Node, NodeHashFunction> cache;
+      unordered_map<Node, Node, NodeHashFunction> cache;
       n = d_private->expandDefinitions(n, cache);
     }
     Notice() << "SmtEngine::checkModel(): -- expands to " << n << endl;
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 3df1dbea8..ed265e2b8 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -74,13 +74,6 @@ namespace prop {
   class PropEngine;
 }/* CVC4::prop namespace */
 
-namespace expr {
-  namespace attr {
-    class AttributeManager;
-    struct SmtAttributes;
-  }/* CVC4::expr::attr namespace */
-}/* CVC4::expr namespace */
-
 namespace smt {
   /**
    * Representation of a defined function.  We keep these around in
@@ -357,20 +350,9 @@ class CVC4_PUBLIC SmtEngine {
   // to access d_modelCommands
   friend class ::CVC4::Model;
   friend class ::CVC4::theory::TheoryModel;
-  // to access SmtAttributes
-  friend class expr::attr::AttributeManager;
   // to access getModel(), which is private (for now)
   friend class GetModelCommand;
 
-  /**
-   * There's something of a handshake between the expr package's
-   * AttributeManager and the SmtEngine because the expr package
-   * doesn't have a Context on its own (that's owned by the
-   * SmtEngine).  Thus all context-dependent attributes are stored
-   * here.
-   */
-  expr::attr::SmtAttributes* d_smtAttributes;
-
   StatisticsRegistry* d_statisticsRegistry;
 
   smt::SmtEngineStatistics* d_stats;
diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h
index 535e6fb52..854ddc61e 100644
--- a/src/smt/term_formula_removal.h
+++ b/src/smt/term_formula_removal.h
@@ -18,6 +18,7 @@
 
 #pragma once
 
+#include <unordered_map>
 #include <vector>
 
 #include "context/cdinsert_hashmap.h"
@@ -33,7 +34,7 @@ namespace theory {
   class ContainsTermITEVisitor;
 }/* CVC4::theory namespace */
 
-typedef std::hash_map<Node, unsigned, NodeHashFunction> IteSkolemMap;
+typedef std::unordered_map<Node, unsigned, NodeHashFunction> IteSkolemMap;
 
 class RemoveTermFormulas {
   typedef context::CDInsertHashMap< std::pair<Node, int>, Node, PairHashFunction<Node, int, NodeHashFunction, BoolHashFunction> > ITECache;
diff --git a/src/smt_util/nary_builder.h b/src/smt_util/nary_builder.h
index 244420e66..dde7e1ccd 100644
--- a/src/smt_util/nary_builder.h
+++ b/src/smt_util/nary_builder.h
@@ -20,7 +20,9 @@
 
 #pragma once
 
+#include <unordered_map>
 #include <vector>
+
 #include "expr/node.h"
 
 namespace CVC4{
@@ -47,7 +49,7 @@ private:
   Node case_assoccomm(TNode n);
   Node case_other(TNode n);
 
-  typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
+  typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
   NodeMap d_cache;
 };/* class RePairAssocCommutativeOperators */
 
diff --git a/src/theory/arith/arith_ite_utils.h b/src/theory/arith/arith_ite_utils.h
index 47f1caf9e..e2d0d2baf 100644
--- a/src/theory/arith/arith_ite_utils.h
+++ b/src/theory/arith/arith_ite_utils.h
@@ -15,11 +15,6 @@
  ** \todo document this file
  **/
 
-
-
-
-
-
 // Pass 1: label the ite as (constant) or (+ constant variable)
 
 #include "cvc4_private.h"
@@ -27,9 +22,9 @@
 #ifndef __CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H
 #define __CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H
 
+#include <unordered_map>
+
 #include "expr/node.h"
-#include <ext/hash_map>
-#include <ext/hash_set>
 #include "context/cdo.h"
 #include "context/cdtrail_hashmap.h"
 
@@ -46,7 +41,7 @@ class ArithIteUtils {
   SubstitutionMap* d_subs;
   TheoryModel* d_model;
 
-  typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
+  typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
   // cache for reduce vars
   NodeMap d_reduceVar; // if reduceVars[n].isNull(), treat reduceVars[n] == n
 
@@ -56,7 +51,7 @@ class ArithIteUtils {
 
 
   NodeMap d_reduceGcd;
-  typedef std::hash_map<Node, Integer, NodeHashFunction> NodeIntegerMap;
+  typedef std::unordered_map<Node, Integer, NodeHashFunction> NodeIntegerMap;
   NodeIntegerMap d_gcds;
 
   Integer d_one;
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index 68d4d8f1a..4a9539d49 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -19,7 +19,8 @@
 #ifndef __CVC4__THEORY__ARITH__ARITH_UTILITIES_H
 #define __CVC4__THEORY__ARITH__ARITH_UTILITIES_H
 
-#include <ext/hash_map>
+#include <unordered_map>
+#include <unordered_set>
 #include <vector>
 
 #include "context/cdhashset.h"
@@ -35,12 +36,12 @@ namespace theory {
 namespace arith {
 
 //Sets of Nodes
-typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
-typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
+typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
+typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
 typedef context::CDHashSet<Node, NodeHashFunction> CDNodeSet;
 
 //Maps from Nodes -> ArithVars, and vice versa
-typedef __gnu_cxx::hash_map<Node, ArithVar, NodeHashFunction> NodeToArithVarMap;
+typedef std::unordered_map<Node, ArithVar, NodeHashFunction> NodeToArithVarMap;
 typedef DenseMap<Node> ArithVarToNodeMap;
 
 inline Node mkRationalNode(const Rational& q){
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index 9ba4074c1..3427edbd3 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -16,8 +16,9 @@
  **/
 #include "theory/arith/constraint.h"
 
-#include <ostream>
 #include <algorithm>
+#include <ostream>
+#include <unordered_set>
 
 #include "base/output.h"
 #include "proof/proof.h"
@@ -1333,7 +1334,7 @@ struct ConstraintCPHash {
 };
 
 void Constraint::assertionFringe(ConstraintCPVec& v){
-  hash_set<ConstraintCP, ConstraintCPHash> visited;
+  unordered_set<ConstraintCP, ConstraintCPHash> visited;
   size_t writePos = 0;
 
   if(!v.empty()){
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index 662327301..25f838567 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -75,7 +75,7 @@
 #ifndef __CVC4__THEORY__ARITH__CONSTRAINT_H
 #define __CVC4__THEORY__ARITH__CONSTRAINT_H
 
-#include <ext/hash_map>
+#include <unordered_map>
 #include <list>
 #include <set>
 #include <vector>
@@ -145,7 +145,7 @@ enum ConstraintType {LowerBound, Equality, UpperBound, Disequality};
 
 typedef context::CDList<ConstraintCP> CDConstraintList;
 
-typedef __gnu_cxx::hash_map<Node, ConstraintP, NodeHashFunction> NodetoConstraintMap;
+typedef std::unordered_map<Node, ConstraintP, NodeHashFunction> NodetoConstraintMap;
 
 typedef size_t ConstraintRuleID;
 static const ConstraintRuleID ConstraintRuleIdSentinel = std::numeric_limits<ConstraintRuleID>::max();
diff --git a/src/theory/arith/cut_log.h b/src/theory/arith/cut_log.h
index 77273f609..7d41666e7 100644
--- a/src/theory/arith/cut_log.h
+++ b/src/theory/arith/cut_log.h
@@ -20,7 +20,7 @@
 
 #pragma once
 
-#include <ext/hash_map>
+#include <unordered_map>
 #include <map>
 #include <set>
 #include <vector>
@@ -179,7 +179,7 @@ private:
   int d_upId;
 
 public:
-  typedef __gnu_cxx::hash_map<int, ArithVar> RowIdMap;
+  typedef std::unordered_map<int, ArithVar> RowIdMap;
 private:
   RowIdMap d_rowId2ArithVar;
 
diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp
index d862dabbd..5b61385f3 100644
--- a/src/theory/arith/dio_solver.cpp
+++ b/src/theory/arith/dio_solver.cpp
@@ -304,7 +304,7 @@ bool DioSolver::queueEmpty() const{
 }
 
 Node DioSolver::columnGcdIsOne() const{
-  std::hash_map<Node, Integer, NodeHashFunction> gcdMap;
+  std::unordered_map<Node, Integer, NodeHashFunction> gcdMap;
 
   std::deque<TrailIndex>::const_iterator iter, end;
   for(iter = d_currentF.begin(), end = d_currentF.end(); iter != end; ++iter){
diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h
index 2b8b64e75..292f2b856 100644
--- a/src/theory/arith/dio_solver.h
+++ b/src/theory/arith/dio_solver.h
@@ -20,6 +20,7 @@
 #ifndef __CVC4__THEORY__ARITH__DIO_SOLVER_H
 #define __CVC4__THEORY__ARITH__DIO_SOLVER_H
 
+#include <unordered_map>
 #include <utility>
 #include <vector>
 
@@ -68,7 +69,7 @@ private:
    * We maintain a map from the variables associated with proofs to an input constraint.
    * These variables can then be used in polynomial manipulations.
    */
-  typedef std::hash_map<Node, InputConstraintIndex, NodeHashFunction> NodeToInputConstraintIndexMap;
+  typedef std::unordered_map<Node, InputConstraintIndex, NodeHashFunction> NodeToInputConstraintIndexMap;
   NodeToInputConstraintIndexMap d_varToInputConstraintMap;
 
   Node proofVariableToReason(const Variable& v) const{
diff --git a/src/theory/arith/pseudoboolean_proc.h b/src/theory/arith/pseudoboolean_proc.h
index 471e37fa1..0b91ed074 100644
--- a/src/theory/arith/pseudoboolean_proc.h
+++ b/src/theory/arith/pseudoboolean_proc.h
@@ -19,7 +19,7 @@
 
 #pragma once
 
-#include <ext/hash_set>
+#include <unordered_set>
 #include <vector>
 
 #include "context/cdhashmap.h"
@@ -43,7 +43,7 @@ private:
   CDNode2PairMap d_pbBounds;
   SubstitutionMap d_subCache;
 
-  typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
+  typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
   NodeSet d_learningCache;
 
   context::CDO<unsigned> d_pbs;
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index 13fba2c77..bd983e0bf 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -53,6 +53,8 @@
 
 #pragma once
 
+#include <unordered_map>
+
 #include "theory/arith/arithvar.h"
 #include "theory/arith/delta_rational.h"
 #include "theory/arith/error_set.h"
@@ -199,7 +201,7 @@ protected:
     }
   };
 
-  typedef std::hash_map< std::pair<ArithVar, int>, ArithVarVec, ArithVarIntPairHashFunc> sgn_table;
+  typedef std::unordered_map< std::pair<ArithVar, int>, ArithVarVec, ArithVarIntPairHashFunc> sgn_table;
 
   static inline int determinizeSgn(int sgn){
     return sgn < 0 ? -1 : (sgn == 0 ? 0 : 1);
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 5fb31e93f..ab5a19858 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -4268,7 +4268,7 @@ void TheoryArithPrivate::collectModelInfo( TheoryModel* m ){
 
   // Delta lasts at least the duration of the function call
   const Rational& delta = d_partialModel.getDelta();
-  std::hash_set<TNode, TNodeHashFunction> shared = d_containing.currentlySharedTerms();
+  std::unordered_set<TNode, TNodeHashFunction> shared = d_containing.currentlySharedTerms();
 
   // TODO:
   // This is not very good for user push/pop....
diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h
index cc5fddf25..5955fb4e4 100644
--- a/src/theory/arrays/array_info.h
+++ b/src/theory/arrays/array_info.h
@@ -18,10 +18,9 @@
 #ifndef __CVC4__THEORY__ARRAYS__ARRAY_INFO_H
 #define __CVC4__THEORY__ARRAYS__ARRAY_INFO_H
 
-#include <ext/hash_set>
-#include <ext/hash_map>
 #include <iostream>
 #include <map>
+#include <unordered_map>
 
 #include "context/backtrackable.h"
 #include "context/cdlist.h"
@@ -92,7 +91,7 @@ public:
 };/* class Info */
 
 
-typedef __gnu_cxx::hash_map<Node, Info*, NodeHashFunction> CNodeInfoMap;
+typedef std::unordered_map<Node, Info*, NodeHashFunction> CNodeInfoMap;
 
 /**
  * Class keeping track of the following information for canonical
diff --git a/src/theory/arrays/static_fact_manager.h b/src/theory/arrays/static_fact_manager.h
index 53d935813..4a08838fe 100644
--- a/src/theory/arrays/static_fact_manager.h
+++ b/src/theory/arrays/static_fact_manager.h
@@ -23,7 +23,7 @@
 
 #include <utility>
 #include <vector>
-#include <ext/hash_map>
+#include <unordered_map>
 
 #include "expr/node.h"
 
@@ -33,7 +33,7 @@ namespace arrays {
 
   class StaticFactManager {
   /** Our underlying map type. */
-  typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> MapType;
+  typedef std::unordered_map<Node, Node, NodeHashFunction> MapType;
 
   /**
    * Our map of Nodes to their canonical representatives.
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index bde88abab..2f5a9a14f 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -551,7 +551,7 @@ void TheoryArrays::weakEquivMakeRepIndex(TNode node) {
 }
 
 void TheoryArrays::weakEquivAddSecondary(TNode index, TNode arrayFrom, TNode arrayTo, TNode reason) {
-  std::hash_set<TNode, TNodeHashFunction> marked;
+  std::unordered_set<TNode, TNodeHashFunction> marked;
   vector<TNode> index_trail;
   vector<TNode>::iterator it, iend;
   Node equivalence_trail = reason;
@@ -1198,7 +1198,7 @@ void TheoryArrays::collectModelInfo( TheoryModel* m )
       /*
     }
     else {
-      std::hash_map<Node, Node, NodeHashFunction>::iterator it = d_skolemCache.find(n);
+      std::unordered_map<Node, Node, NodeHashFunction>::iterator it = d_skolemCache.find(n);
       if (it == d_skolemCache.end()) {
         rep = nm->mkSkolem("array_collect_model_var", n.getType(), "base model variable for array collectModelInfo");
         d_skolemCache[n] = rep;
@@ -1240,7 +1240,7 @@ void TheoryArrays::presolve()
 Node TheoryArrays::getSkolem(TNode ref, const string& name, const TypeNode& type, const string& comment, bool makeEqual)
 {
   Node skolem;
-  std::hash_map<Node, Node, NodeHashFunction>::iterator it = d_skolemCache.find(ref);
+  std::unordered_map<Node, Node, NodeHashFunction>::iterator it = d_skolemCache.find(ref);
   if (it == d_skolemCache.end()) {
     NodeManager* nm = NodeManager::currentNM();
     skolem = nm->mkSkolem(name, type, comment);
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 7e8831733..3ef9578ef 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -19,6 +19,8 @@
 #ifndef __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H
 #define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H
 
+#include <unordered_map>
+
 #include "context/cdhashmap.h"
 #include "context/cdhashset.h"
 #include "context/cdqueue.h"
@@ -384,7 +386,7 @@ class TheoryArrays : public Theory {
   // When a new read term is created, we check the index to see if we know the model value.  If so, we add it to d_constReads (and d_constReadsList)
   // If not, we push it onto d_reads and figure out where it goes at computeCareGraph time.
   // d_constReadsList is used as a backup in case we can't compute the model at computeCareGraph time.
-  typedef std::hash_map<Node, CTNodeList*, NodeHashFunction> CNodeNListMap;
+  typedef std::unordered_map<Node, CTNodeList*, NodeHashFunction> CNodeNListMap;
   CNodeNListMap d_constReads;
   context::CDList<TNode> d_reads;
   context::CDList<TNode> d_constReadsList;
@@ -408,7 +410,7 @@ class TheoryArrays : public Theory {
   };/* class ContextPopper */
   ContextPopper d_contextPopper;
 
-  std::hash_map<Node, Node, NodeHashFunction> d_skolemCache;
+  std::unordered_map<Node, Node, NodeHashFunction> d_skolemCache;
   context::CDO<unsigned> d_skolemIndex;
   std::vector<Node> d_skolemAssertions;
 
@@ -425,7 +427,7 @@ class TheoryArrays : public Theory {
   typedef context::CDHashMap<Node,Node,NodeHashFunction> DefValMap;
   DefValMap d_defValues;
 
-  typedef std::hash_map<std::pair<TNode, TNode>, CTNodeList*, TNodePairHashFunction> ReadBucketMap;
+  typedef std::unordered_map<std::pair<TNode, TNode>, CTNodeList*, TNodePairHashFunction> ReadBucketMap;
   ReadBucketMap d_readBucketTable;
   context::Context* d_readTableContext;
   context::CDList<Node> d_arrayMerges;
diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h
index 4a05f3789..04d199971 100644
--- a/src/theory/arrays/theory_arrays_rewriter.h
+++ b/src/theory/arrays/theory_arrays_rewriter.h
@@ -20,6 +20,9 @@
 #ifndef __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H
 #define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H
 
+#include <unordered_map>
+#include <unordered_set>
+
 #include "theory/rewriter.h"
 #include "theory/type_enumerator.h"
 
@@ -150,9 +153,9 @@ public:
     // Bad case: have to recompute value counts and/or possibly switch out
     // default value
     store = n;
-    std::hash_set<TNode, TNodeHashFunction> indexSet;
-    std::hash_map<TNode, unsigned, TNodeHashFunction> elementsMap;
-    std::hash_map<TNode, unsigned, TNodeHashFunction>::iterator it;
+    std::unordered_set<TNode, TNodeHashFunction> indexSet;
+    std::unordered_map<TNode, unsigned, TNodeHashFunction> elementsMap;
+    std::unordered_map<TNode, unsigned, TNodeHashFunction>::iterator it;
     unsigned count;
     unsigned max = 0;
     TNode maxValue;
diff --git a/src/theory/arrays/union_find.h b/src/theory/arrays/union_find.h
index e896784ef..eb60f339b 100644
--- a/src/theory/arrays/union_find.h
+++ b/src/theory/arrays/union_find.h
@@ -23,7 +23,7 @@
 
 #include <utility>
 #include <vector>
-#include <ext/hash_map>
+#include <unordered_map>
 
 #include "expr/node.h"
 #include "context/cdo.h"
@@ -41,7 +41,7 @@ namespace arrays {
 template <class NodeType, class NodeHash>
 class UnionFind : context::ContextNotifyObj {
   /** Our underlying map type. */
-  typedef __gnu_cxx::hash_map<NodeType, NodeType, NodeHash> MapType;
+  typedef std::unordered_map<NodeType, NodeType, NodeHash> MapType;
 
   /**
    * Our map of Nodes to their canonical representatives.
diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h
index 03c811eee..78e01f690 100644
--- a/src/theory/booleans/circuit_propagator.h
+++ b/src/theory/booleans/circuit_propagator.h
@@ -19,8 +19,9 @@
 #ifndef __CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H
 #define __CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H
 
-#include <vector>
 #include <functional>
+#include <unordered_map>
+#include <vector>
 
 #include "theory/theory.h"
 #include "context/context.h"
@@ -64,7 +65,7 @@ public:
     else return ASSIGNED_TO_TRUE;
   }
 
-  typedef std::hash_map<Node, std::vector<Node>, NodeHashFunction> BackEdgesMap;
+  typedef std::unordered_map<Node, std::vector<Node>, NodeHashFunction> BackEdgesMap;
 
 private:
 
diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp
index b5f7e37d4..8373f636b 100644
--- a/src/theory/booleans/theory_bool_rewriter.cpp
+++ b/src/theory/booleans/theory_bool_rewriter.cpp
@@ -16,6 +16,8 @@
  **/
 
 #include <algorithm>
+#include <unordered_set>
+
 #include "theory/booleans/theory_bool_rewriter.h"
 
 namespace CVC4 {
@@ -41,7 +43,7 @@ RewriteResponse TheoryBoolRewriter::postRewrite(TNode node) {
  */
 RewriteResponse flattenNode(TNode n, TNode trivialNode, TNode skipNode)
 {
-  typedef std::hash_set<TNode, TNodeHashFunction> node_set;
+  typedef std::unordered_set<TNode, TNodeHashFunction> node_set;
 
   node_set visited;
   visited.insert(skipNode);
diff --git a/src/theory/bv/abstraction.h b/src/theory/bv/abstraction.h
index ed4b8aeb6..0d7e0ff2a 100644
--- a/src/theory/bv/abstraction.h
+++ b/src/theory/bv/abstraction.h
@@ -19,8 +19,8 @@
 #ifndef __CVC4__THEORY__BV__ABSTRACTION_H
 #define __CVC4__THEORY__BV__ABSTRACTION_H
 
-#include <ext/hash_map>
-#include <ext/hash_set>
+#include <unordered_map>
+#include <unordered_set>
 
 #include "expr/node.h"
 #include "theory/substitutions.h"
@@ -64,10 +64,10 @@ class AbstractionModule {
   };
 
   class ArgsTable {
-    __gnu_cxx::hash_map<TNode, ArgsTableEntry, TNodeHashFunction > d_data;
+    std::unordered_map<TNode, ArgsTableEntry, TNodeHashFunction > d_data;
     bool hasEntry(TNode signature) const;
   public:
-    typedef __gnu_cxx::hash_map<TNode, ArgsTableEntry, TNodeHashFunction >::iterator iterator;
+    typedef std::unordered_map<TNode, ArgsTableEntry, TNodeHashFunction >::iterator iterator;
     ArgsTable() {}
     void addEntry(TNode signature, const ArgsVec& args);
     ArgsTableEntry& getEntry(TNode signature);
@@ -122,16 +122,16 @@ class AbstractionModule {
 
   };
 
-  typedef __gnu_cxx::hash_map<Node, std::vector<Node>, NodeHashFunction> NodeVecMap;
-  typedef __gnu_cxx::hash_map<Node, TNode, NodeHashFunction> NodeTNodeMap;
-  typedef __gnu_cxx::hash_map<TNode, TNode, TNodeHashFunction> TNodeTNodeMap;
-  typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeNodeMap;
-  typedef __gnu_cxx::hash_map<Node, TNode, NodeHashFunction> TNodeNodeMap;
-  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
-  typedef __gnu_cxx::hash_map<unsigned, Node> IntNodeMap;
-  typedef __gnu_cxx::hash_map<unsigned, unsigned> IndexMap;
-  typedef __gnu_cxx::hash_map<unsigned, std::vector<Node> > SkolemMap;
-  typedef __gnu_cxx::hash_map<TNode, unsigned, TNodeHashFunction > SignatureMap;
+  typedef std::unordered_map<Node, std::vector<Node>, NodeHashFunction> NodeVecMap;
+  typedef std::unordered_map<Node, TNode, NodeHashFunction> NodeTNodeMap;
+  typedef std::unordered_map<TNode, TNode, TNodeHashFunction> TNodeTNodeMap;
+  typedef std::unordered_map<Node, Node, NodeHashFunction> NodeNodeMap;
+  typedef std::unordered_map<Node, TNode, NodeHashFunction> TNodeNodeMap;
+  typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
+  typedef std::unordered_map<unsigned, Node> IntNodeMap;
+  typedef std::unordered_map<unsigned, unsigned> IndexMap;
+  typedef std::unordered_map<unsigned, std::vector<Node> > SkolemMap;
+  typedef std::unordered_map<TNode, unsigned, TNodeHashFunction > SignatureMap;
 
   ArgsTable d_argsTable;
 
diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
index b6b2e2926..565c454e3 100644
--- a/src/theory/bv/bitblaster_template.h
+++ b/src/theory/bv/bitblaster_template.h
@@ -19,7 +19,8 @@
 #ifndef __CVC4__BITBLASTER_TEMPLATE_H
 #define __CVC4__BITBLASTER_TEMPLATE_H
 
-#include <ext/hash_map>
+#include <unordered_map>
+#include <unordered_set>
 #include <vector>
 
 #include "bitblast_strategies_template.h"
@@ -58,8 +59,8 @@ namespace bv {
 
 class BitblastingRegistrar;
 
-typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
-typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
+typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
+typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
 
 class AbstractionModule;
 
@@ -73,9 +74,9 @@ template <class T>
 class TBitblaster {
 protected:
   typedef std::vector<T> Bits;
-  typedef __gnu_cxx::hash_map <Node, Bits, NodeHashFunction>  TermDefMap;
-  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction>       TNodeSet;
-  typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction>   ModelCache;
+  typedef std::unordered_map <Node, Bits, NodeHashFunction>  TermDefMap;
+  typedef std::unordered_set<TNode, TNodeHashFunction>       TNodeSet;
+  typedef std::unordered_map<Node, Node, NodeHashFunction>   ModelCache;
 
   typedef void  (*TermBBStrategy) (TNode, Bits&, TBitblaster<T>*);
   typedef T     (*AtomBBStrategy) (TNode, TBitblaster<T>*);
@@ -258,7 +259,7 @@ public:
 
 
 class EagerBitblaster : public TBitblaster<Node> {
-  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
+  typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
   // sat solver used for bitblasting and associated CnfStream
   prop::SatSolver*                   d_satSolver;
   BitblastingRegistrar*              d_bitblastingRegistrar;
@@ -305,8 +306,8 @@ public:
 }; /* class Registrar */
 
 class AigBitblaster : public TBitblaster<Abc_Obj_t*> {
-  typedef std::hash_map<TNode, Abc_Obj_t*, TNodeHashFunction > TNodeAigMap;
-  typedef std::hash_map<Node, Abc_Obj_t*, NodeHashFunction > NodeAigMap;
+  typedef std::unordered_map<TNode, Abc_Obj_t*, TNodeHashFunction > TNodeAigMap;
+  typedef std::unordered_map<Node, Abc_Obj_t*, NodeHashFunction > NodeAigMap;
   
   static Abc_Ntk_t* abcAigNetwork;
   context::Context* d_nullContext;
diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h
index 380d06349..ec6cbad09 100644
--- a/src/theory/bv/bv_eager_solver.h
+++ b/src/theory/bv/bv_eager_solver.h
@@ -9,18 +9,21 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Eager bit-blasting solver. 
+ ** \brief Eager bit-blasting solver.
  **
  ** Eager bit-blasting solver.
  **/
 
 #include "cvc4_private.h"
+
+#pragma once
+
+#include <unordered_set>
+#include <vector>
+
 #include "expr/node.h"
 #include "theory/theory_model.h"
 #include "theory/bv/theory_bv.h"
-#include <vector>
-#pragma once
-
 
 namespace CVC4 {
 namespace theory {
@@ -33,7 +36,7 @@ class AigBitblaster;
  * BitblastSolver
  */
 class EagerBitblastSolver {
-  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> AssertionSet;
+  typedef std::unordered_set<TNode, TNodeHashFunction> AssertionSet;
   AssertionSet d_assertionSet;
   /** Bitblasters */
   EagerBitblaster* d_bitblaster;
diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h
index f85d8a835..30270b3c3 100644
--- a/src/theory/bv/bv_inequality_graph.h
+++ b/src/theory/bv/bv_inequality_graph.h
@@ -9,7 +9,7 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Algebraic solver. 
+ ** \brief Algebraic solver.
  **
  ** Algebraic solver.
  **/
@@ -19,23 +19,25 @@
 #ifndef __CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H
 #define __CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H
 
-#include "context/context.h"
+#include <list>
+#include <queue>
+#include <unordered_map>
+#include <unordered_set>
+
 #include "context/cdqueue.h"
-#include "theory/uf/equality_engine.h"
+#include "context/context.h"
 #include "theory/theory.h"
-#include <queue>
-#include <list>
+#include "theory/uf/equality_engine.h"
+
 namespace CVC4 {
 namespace theory {
-
-
 namespace bv {
 
-typedef unsigned TermId; 
+typedef unsigned TermId;
 typedef unsigned ReasonId;
 extern const TermId UndefinedTermId;
 extern const ReasonId UndefinedReasonId;
-extern const ReasonId AxiomReasonId; 
+extern const ReasonId AxiomReasonId;
 
 class InequalityGraph : public context::ContextNotifyObj{
 
@@ -100,15 +102,15 @@ class InequalityGraph : public context::ContextNotifyObj{
     }
   }; 
 
-  typedef __gnu_cxx::hash_map<TNode, ReasonId, TNodeHashFunction> ReasonToIdMap;
-  typedef __gnu_cxx::hash_map<TNode, TermId, TNodeHashFunction> TermNodeToIdMap;
+  typedef std::unordered_map<TNode, ReasonId, TNodeHashFunction> ReasonToIdMap;
+  typedef std::unordered_map<TNode, TermId, TNodeHashFunction> TermNodeToIdMap;
 
   typedef std::vector<InequalityEdge> Edges; 
-  typedef __gnu_cxx::hash_set<TermId> TermIdSet;
+  typedef std::unordered_set<TermId> TermIdSet;
 
   typedef std::priority_queue<TermId, std::vector<TermId>, QueueComparator> BFSQueue; 
-  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
-  typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
+  typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
+  typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
 
   std::vector<InequalityNode> d_ineqNodes;
   std::vector< Edges > d_ineqEdges;
diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h
index dcd3f1062..c5fe63ad6 100644
--- a/src/theory/bv/bv_quick_check.h
+++ b/src/theory/bv/bv_quick_check.h
@@ -20,7 +20,7 @@
 #define __CVC4__BV_QUICK_CHECK_H
 
 #include <vector>
-#include <ext/hash_map>
+#include <unordered_set>
 
 #include "context/cdo.h"
 #include "expr/node.h"
@@ -99,7 +99,7 @@ public:
   uint64_t computeAtomWeight(TNode atom, NodeSet& seen);
   void collectModelInfo(theory::TheoryModel* model, bool fullModel); 
 
-  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction>::const_iterator vars_iterator;
+  typedef std::unordered_set<TNode, TNodeHashFunction>::const_iterator vars_iterator;
   vars_iterator beginVars(); 
   vars_iterator endVars(); 
 
diff --git a/src/theory/bv/bv_subtheory_algebraic.h b/src/theory/bv/bv_subtheory_algebraic.h
index 3730ebc90..4b4103e44 100644
--- a/src/theory/bv/bv_subtheory_algebraic.h
+++ b/src/theory/bv/bv_subtheory_algebraic.h
@@ -14,12 +14,16 @@
  ** Algebraic solver.
  **/
 
+#include "cvc4_private.h"
+
 #pragma once
 
-#include "cvc4_private.h"
+#include <unordered_map>
+#include <unordered_set>
+
 #include "theory/bv/bv_subtheory.h"
-#include "theory/substitutions.h"
 #include "theory/bv/slicer.h"
+#include "theory/substitutions.h"
 
 namespace CVC4 {
 namespace theory {
@@ -60,8 +64,8 @@ class SubstitutionEx {
     {}
   };
 
-  typedef __gnu_cxx::hash_map<Node, SubstitutionElement, NodeHashFunction> Substitutions;
-  typedef __gnu_cxx::hash_map<Node, SubstitutionElement, NodeHashFunction> SubstitutionsCache;
+  typedef std::unordered_map<Node, SubstitutionElement, NodeHashFunction> Substitutions;
+  typedef std::unordered_map<Node, SubstitutionElement, NodeHashFunction> SubstitutionsCache;
 
   Substitutions d_substitutions;
   SubstitutionsCache d_cache;
@@ -104,9 +108,9 @@ struct WorklistElement {
 }; 
 
 
-typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeNodeMap;
-typedef __gnu_cxx::hash_map<Node, unsigned, NodeHashFunction> NodeIdMap;
-typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
+typedef std::unordered_map<Node, Node, NodeHashFunction> NodeNodeMap;
+typedef std::unordered_map<Node, unsigned, NodeHashFunction> NodeIdMap;
+typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
 
 
 class ExtractSkolemizer {
@@ -123,7 +127,7 @@ class ExtractSkolemizer {
     ExtractList() : base(1), extracts() {}
     void addExtract(Extract& e); 
   };
-  typedef   __gnu_cxx::hash_map<Node, ExtractList, NodeHashFunction> VarExtractMap;
+  typedef   std::unordered_map<Node, ExtractList, NodeHashFunction> VarExtractMap;
   context::Context d_emptyContext;
   VarExtractMap d_varToExtract;
   theory::SubstitutionMap* d_modelMap;
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index c9fb81195..4bbe4327e 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -18,6 +18,8 @@
 
 #pragma once
 
+#include <unordered_map>
+
 #include "theory/bv/bitblaster_template.h"
 #include "theory/bv/bv_subtheory.h"
 
@@ -47,7 +49,7 @@ class BitblastSolver : public SubtheorySolver {
   context::CDQueue<TNode> d_bitblastQueue;
   Statistics d_statistics;
 
-  typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
+  typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
   NodeMap d_modelCache;
   context::CDO<bool> d_validModelCache;
 
diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h
index 662f8835e..b416e019d 100644
--- a/src/theory/bv/bv_subtheory_core.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -14,12 +14,16 @@
  ** Algebraic solver.
  **/
 
+#include "cvc4_private.h"
+
 #pragma once
 
-#include "cvc4_private.h"
-#include "theory/bv/bv_subtheory.h"
+#include <unordered_map>
+#include <unordered_set>
+
 #include "context/cdhashmap.h"
 #include "context/cdhashset.h"
+#include "theory/bv/bv_subtheory.h"
 
 namespace CVC4 {
 namespace theory {
@@ -31,9 +35,9 @@ class Base;
  * Bitvector equality solver
  */
 class CoreSolver : public SubtheorySolver {
-  typedef __gnu_cxx::hash_map<TNode, Node, TNodeHashFunction> ModelValue;
-  typedef __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> TNodeBoolMap;
-  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
+  typedef std::unordered_map<TNode, Node, TNodeHashFunction> ModelValue;
+  typedef std::unordered_map<TNode, bool, TNodeHashFunction> TNodeBoolMap;
+  typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
 
 
   struct Statistics {
diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h
index 37d3723ac..1123d15ae 100644
--- a/src/theory/bv/bv_subtheory_inequality.h
+++ b/src/theory/bv/bv_subtheory_inequality.h
@@ -19,10 +19,12 @@
 #ifndef __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H
 #define __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H
 
-#include "theory/bv/bv_subtheory.h"
-#include "theory/bv/bv_inequality_graph.h"
+#include <unordered_set>
+
 #include "context/cdhashset.h"
 #include "expr/attribute.h"
+#include "theory/bv/bv_inequality_graph.h"
+#include "theory/bv/bv_subtheory.h"
 
 namespace CVC4 {
 namespace theory {
@@ -47,7 +49,7 @@ class InequalitySolver: public SubtheorySolver {
   InequalityGraph d_inequalityGraph;
   context::CDHashMap<Node, TNode, NodeHashFunction> d_explanations;
   context::CDO<bool> d_isComplete;
-  typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
+  typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
   NodeSet d_ineqTerms;
   bool isInequalityOnly(TNode node);
   bool addInequality(TNode a, TNode b, bool strict, TNode fact);
diff --git a/src/theory/bv/bv_to_bool.h b/src/theory/bv/bv_to_bool.h
index a934cf045..93a83626e 100644
--- a/src/theory/bv/bv_to_bool.h
+++ b/src/theory/bv/bv_to_bool.h
@@ -19,6 +19,8 @@
 #ifndef __CVC4__THEORY__BV__BV_TO_BOOL_H
 #define __CVC4__THEORY__BV__BV_TO_BOOL_H
 
+#include <unordered_map>
+
 #include "theory/bv/theory_bv_utils.h"
 #include "util/statistics_registry.h"
 
@@ -26,7 +28,7 @@ namespace CVC4 {
 namespace theory {
 namespace bv {
 
-typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeNodeMap;
+typedef std::unordered_map<Node, Node, NodeHashFunction> NodeNodeMap;
 
 class BvToBoolPreprocessor {
 
diff --git a/src/theory/bv/bvintropow2.h b/src/theory/bv/bvintropow2.h
index 935cbb7ed..e335c1339 100644
--- a/src/theory/bv/bvintropow2.h
+++ b/src/theory/bv/bvintropow2.h
@@ -21,7 +21,7 @@
 #include "expr/node.h"
 
 #include <vector>
-#include <ext/hash_map>
+#include <unordered_map>
 
 #ifndef __CVC4__THEORY__BV__BV_INTRO_POW_H
 #define __CVC4__THEORY__BV__BV_INTRO_POW_H
@@ -36,7 +36,7 @@ public:
   static void pow2Rewrite(std::vector<Node>& assertionsToPreprocess);
 
 private:
-  typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeMap;
+  typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
   static Node pow2Rewrite(Node assertionsToPreprocess, NodeMap& cache);
 }; 
 
diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h
index b594d5fec..dc8d333c4 100644
--- a/src/theory/bv/slicer.h
+++ b/src/theory/bv/slicer.h
@@ -20,7 +20,7 @@
 
 #include <vector>
 #include <list>
-#include <ext/hash_map>
+#include <unordered_map>
 
 #include "expr/node.h"
 #include "theory/bv/theory_bv_utils.h"
@@ -79,7 +79,7 @@ public:
  * UnionFind
  * 
  */
-typedef __gnu_cxx::hash_set<TermId> TermSet;
+typedef std::unordered_set<TermId> TermSet;
 typedef std::vector<TermId> Decomposition; 
 
 struct ExtractTerm {
@@ -226,9 +226,9 @@ public:
 };
 
 class Slicer {
-  __gnu_cxx::hash_map<TermId, TNode> d_idToNode;
-  __gnu_cxx::hash_map<TNode, TermId, TNodeHashFunction> d_nodeToId;
-  __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> d_coreTermCache;
+  std::unordered_map<TermId, TNode> d_idToNode;
+  std::unordered_map<TNode, TermId, TNodeHashFunction> d_nodeToId;
+  std::unordered_map<TNode, bool, TNodeHashFunction> d_coreTermCache;
   UnionFind d_unionFind;
   ExtractTerm registerTerm(TNode node); 
 public:
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index f8d3e6509..c20df35d5 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -19,6 +19,9 @@
 #ifndef __CVC4__THEORY__BV__THEORY_BV_H
 #define __CVC4__THEORY__BV__THEORY_BV_H
 
+#include <unordered_map>
+#include <unordered_set>
+
 #include "context/cdhashset.h"
 #include "context/cdlist.h"
 #include "context/context.h"
@@ -51,7 +54,7 @@ class TheoryBV : public Theory {
   context::CDHashSet<Node, NodeHashFunction> d_sharedTermsSet;
 
   std::vector<SubtheorySolver*> d_subtheories;
-  __gnu_cxx::hash_map<SubTheory, SubtheorySolver*, std::hash<int> > d_subtheoryMap;
+  std::unordered_map<SubTheory, SubtheorySolver*, std::hash<int> > d_subtheoryMap;
 
 public:
 
@@ -129,22 +132,22 @@ private:
    */
   Node getBVDivByZero(Kind k, unsigned width);
 
-  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
+  typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
   void collectFunctionSymbols(TNode term, TNodeSet& seen);
   void storeFunction(TNode func, TNode term);
-  typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
+  typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
   NodeSet d_staticLearnCache;
 
   /**
    * Maps from bit-vector width to division-by-zero uninterpreted
    * function symbols.
    */
-  __gnu_cxx::hash_map<unsigned, Node> d_BVDivByZero;
-  __gnu_cxx::hash_map<unsigned, Node> d_BVRemByZero;
+  std::unordered_map<unsigned, Node> d_BVDivByZero;
+  std::unordered_map<unsigned, Node> d_BVRemByZero;
 
 
-  typedef __gnu_cxx::hash_map<Node, NodeSet, NodeHashFunction>  FunctionToArgs;
-  typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction>  NodeToNode;
+  typedef std::unordered_map<Node, NodeSet, NodeHashFunction>  FunctionToArgs;
+  typedef std::unordered_map<Node, Node, NodeHashFunction>  NodeToNode;
   // for ackermanization
   FunctionToArgs d_funcToArgs;
   CVC4::theory::SubstitutionMap d_funcToSkolem;
diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index 46297cb68..61f072643 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -19,6 +19,9 @@
 
 #pragma once
 
+#include <unordered_map>
+#include <unordered_set>
+
 #include "theory/rewriter.h"
 #include "theory/bv/theory_bv_rewrite_rules.h"
 #include "theory/bv/theory_bv_utils.h"
@@ -922,7 +925,7 @@ struct Count {
   {}
 };
 
-inline static void insert(std::hash_map<TNode, Count, TNodeHashFunction>& map, TNode node, bool neg) {
+inline static void insert(std::unordered_map<TNode, Count, TNodeHashFunction>& map, TNode node, bool neg) {
   if(map.find(node) == map.end()) {
     Count c = neg? Count(0,1) : Count(1, 0);
     map[node] = c; 
@@ -945,7 +948,7 @@ Node RewriteRule<AndSimplify>::apply(TNode node) {
   Debug("bv-rewrite") << "RewriteRule<AndSimplify>(" << node << ")" << std::endl;
 
   // this will remove duplicates
-  std::hash_map<TNode, Count, TNodeHashFunction> subterms;
+  std::unordered_map<TNode, Count, TNodeHashFunction> subterms;
   unsigned size = utils::getSize(node);
   BitVector constant = utils::mkBitVectorOnes(size); 
   
@@ -974,7 +977,7 @@ Node RewriteRule<AndSimplify>::apply(TNode node) {
     children.push_back(utils::mkConst(constant)); 
   }
   
-  std::hash_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin();
+  std::unordered_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin();
 
   for (; it != subterms.end(); ++it) {
     if (it->second.pos > 0 && it->second.neg > 0) {
@@ -1018,7 +1021,7 @@ Node RewriteRule<FlattenAssocCommutNoDuplicates>::apply(TNode node) {
   Debug("bv-rewrite") << "RewriteRule<FlattenAssocCommut>(" << node << ")" << std::endl;
   std::vector<Node> processingStack;
   processingStack.push_back(node);
-  __gnu_cxx::hash_set<TNode, TNodeHashFunction> processed;
+  std::unordered_set<TNode, TNodeHashFunction> processed;
   std::vector<Node> children;
   Kind kind = node.getKind(); 
   
@@ -1053,7 +1056,7 @@ Node RewriteRule<OrSimplify>::apply(TNode node) {
   Debug("bv-rewrite") << "RewriteRule<OrSimplify>(" << node << ")" << std::endl;
 
   // this will remove duplicates
-  std::hash_map<TNode, Count, TNodeHashFunction> subterms;
+  std::unordered_map<TNode, Count, TNodeHashFunction> subterms;
   unsigned size = utils::getSize(node);
   BitVector constant(size, (unsigned)0); 
   
@@ -1082,7 +1085,7 @@ Node RewriteRule<OrSimplify>::apply(TNode node) {
     children.push_back(utils::mkConst(constant)); 
   }
   
-  std::hash_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin();
+  std::unordered_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin();
 
   for (; it != subterms.end(); ++it) {
     if (it->second.pos > 0 && it->second.neg > 0) {
@@ -1116,7 +1119,7 @@ Node RewriteRule<XorSimplify>::apply(TNode node) {
   Debug("bv-rewrite") << "RewriteRule<XorSimplify>(" << node << ")" << std::endl;
 
 
-  std::hash_map<TNode, Count, TNodeHashFunction> subterms;
+  std::unordered_map<TNode, Count, TNodeHashFunction> subterms;
   unsigned size = utils::getSize(node);
   BitVector constant; 
   bool const_set = false; 
@@ -1144,7 +1147,7 @@ Node RewriteRule<XorSimplify>::apply(TNode node) {
 
   std::vector<Node> children;
 
-  std::hash_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin();
+  std::unordered_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin();
   unsigned true_count = 0;
   bool seen_false = false; 
   for (; it != subterms.end(); ++it) {
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 5bae1af4f..8b8d5e003 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -17,19 +17,22 @@
 
 #include "cvc4_private.h"
 
-#pragma once 
+#pragma once
 
 #include <set>
-#include <vector>
 #include <sstream>
+#include <unordered_map>
+#include <unordered_set>
+#include <vector>
+
 #include "expr/node_manager.h"
 
 namespace CVC4 {
 namespace theory {
 namespace bv {
 
-typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
-typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
+typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
+typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
 
 namespace utils {
 
@@ -505,11 +508,11 @@ inline T gcd(T a, T b) {
   return a;
 }
 
-typedef __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> TNodeBoolMap;
+typedef std::unordered_map<TNode, bool, TNodeHashFunction> TNodeBoolMap;
 
 bool isCoreTerm(TNode term, TNodeBoolMap& cache);
 bool isEqualityTerm(TNode term, TNodeBoolMap& cache);
-typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
+typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
 
 uint64_t numNodes(TNode node, NodeSet& seen);
 
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index fd79e3fdc..a0333ed8b 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -19,7 +19,6 @@
 #ifndef __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_H
 #define __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_H
 
-#include <ext/hash_set>
 #include <iostream>
 #include <map>
 
diff --git a/src/theory/ite_utilities.cpp b/src/theory/ite_utilities.cpp
index e32fa1e71..6d81dbab0 100644
--- a/src/theory/ite_utilities.cpp
+++ b/src/theory/ite_utilities.cpp
@@ -1092,7 +1092,7 @@ bool ITESimplifier::leavesAreConst(TNode e, TheoryId tid)
     return true;
   }
 
-  hash_map<Node, bool, NodeHashFunction>::iterator it;
+  unordered_map<Node, bool, NodeHashFunction>::iterator it;
   it = d_leavesConstCache.find(e);
   if (it != d_leavesConstCache.end()) {
     return (*it).second;
@@ -1173,7 +1173,7 @@ Node ITESimplifier::simpConstants(TNode simpContext, TNode iteNode, TNode simpVa
 
 Node ITESimplifier::getSimpVar(TypeNode t)
 {
-  std::hash_map<TypeNode, Node, TypeNode::HashFunction>::iterator it;
+  std::unordered_map<TypeNode, Node, TypeNode::HashFunction>::iterator it;
   it = d_simpVars.find(t);
   if (it != d_simpVars.end()) {
     return (*it).second;
@@ -1231,7 +1231,7 @@ Node ITESimplifier::createSimpContext(TNode c, Node& iteNode, Node& simpVar)
   d_simpContextCache[c] = result;
   return result;
 }
-typedef std::hash_set<Node, NodeHashFunction> NodeSet;
+typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
 void countReachable_(Node x, Kind k, NodeSet& visited, uint32_t& reached){
   if(visited.find(x) != visited.end()){
     return;
diff --git a/src/theory/ite_utilities.h b/src/theory/ite_utilities.h
index 29f4f7f1f..4aad9a3f0 100644
--- a/src/theory/ite_utilities.h
+++ b/src/theory/ite_utilities.h
@@ -22,8 +22,7 @@
 #ifndef __CVC4__ITE_UTILITIES_H
 #define __CVC4__ITE_UTILITIES_H
 
-#include <ext/hash_map>
-#include <ext/hash_set>
+#include <unordered_map>
 #include <vector>
 
 #include "expr/node.h"
@@ -80,7 +79,7 @@ public:
   size_t cache_size() const { return d_cache.size(); }
 
 private:
-  typedef std::hash_map<Node, bool, NodeHashFunction> NodeBoolMap;
+  typedef std::unordered_map<Node, bool, NodeHashFunction> NodeBoolMap;
   NodeBoolMap d_cache;
 };
 
@@ -100,7 +99,7 @@ public:
   }
   void clear();
 private:
-  typedef std::hash_map<Node, uint32_t, NodeHashFunction> NodeCountMap;
+  typedef std::unordered_map<Node, uint32_t, NodeHashFunction> NodeCountMap;
   NodeCountMap d_reachCount;
 
   bool d_skipVariables;
@@ -131,7 +130,7 @@ public:
   size_t cache_size() const;
 
 private:
-  typedef std::hash_map<Node, uint32_t, NodeHashFunction> NodeCountMap;
+  typedef std::unordered_map<Node, uint32_t, NodeHashFunction> NodeCountMap;
   NodeCountMap d_termITEHeight;
 }; /* class TermITEHeightCounter */
 
@@ -158,7 +157,7 @@ private:
   std::vector<Node>* d_assertions;
   IncomingArcCounter d_incoming;
 
-  typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
+  typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
   NodeMap d_compressed;
 
   void reset();
@@ -206,7 +205,7 @@ private:
   //     constant
   // or  termITE(cnd, ConstantIte, ConstantIte)
   typedef std::vector<Node> NodeVec;
-  typedef std::hash_map<Node, NodeVec*, NodeHashFunction > ConstantLeavesMap;
+  typedef std::unordered_map<Node, NodeVec*, NodeHashFunction > ConstantLeavesMap;
   ConstantLeavesMap d_constantLeaves;
 
   // d_constantLeaves satisfies the following invariants:
@@ -249,23 +248,23 @@ private:
       return hash;
     }
   };/* struct ITESimplifier::NodePairHashFunction */
-  typedef std::hash_map<NodePair, Node, NodePairHashFunction> NodePairMap;
+  typedef std::unordered_map<NodePair, Node, NodePairHashFunction> NodePairMap;
   NodePairMap d_constantIteEqualsConstantCache;
   NodePairMap d_replaceOverCache;
   NodePairMap d_replaceOverTermIteCache;
   Node replaceOver(Node n, Node replaceWith, Node simpVar);
   Node replaceOverTermIte(Node term, Node simpAtom, Node simpVar);
 
-  std::hash_map<Node, bool, NodeHashFunction> d_leavesConstCache;
+  std::unordered_map<Node, bool, NodeHashFunction> d_leavesConstCache;
   bool leavesAreConst(TNode e, theory::TheoryId tid);
   bool leavesAreConst(TNode e);
 
   NodePairMap d_simpConstCache;
   Node simpConstants(TNode simpContext, TNode iteNode, TNode simpVar);
-  std::hash_map<TypeNode, Node, TypeNode::HashFunction> d_simpVars;
+  std::unordered_map<TypeNode, Node, TypeNode::HashFunction> d_simpVars;
   Node getSimpVar(TypeNode t);
 
-  typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
+  typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
   NodeMap d_simpContextCache;
   Node createSimpContext(TNode c, Node& iteNode, Node& simpVar);
 
@@ -314,7 +313,7 @@ private:
   Node d_true;
   Node d_false;
 
-  typedef std::hash_map<TNode, Node, TNodeHashFunction> TNodeMap;
+  typedef std::unordered_map<TNode, Node, TNodeHashFunction> TNodeMap;
 
   class CareSetPtr;
   class CareSetPtrVal {
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index a635568fe..cb8e6f200 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -924,7 +924,9 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) {
       if( d_last_inst_si ){
         Assert( d_conj->getCegConjectureSingleInv() != NULL );
         sol = d_conj->getSingleInvocationSolution( i, tn, status );
-        sol = sol.getKind()==LAMBDA ? sol[1] : sol;
+        if( !sol.isNull() ){
+          sol = sol.getKind()==LAMBDA ? sol[1] : sol;
+        }
       }else{
         Node cprog = d_conj->getCandidate( i );
         if( !d_conj->d_cinfo[cprog].d_inst.empty() ){
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index a8dcd5887..f25d42284 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -888,6 +888,8 @@ Node CegConjectureSingleInv::reconstructToSyntax( Node s, TypeNode stn, int& rec
   Node sol;
   if( reconstructed==1 ){
     sol = d_sygus_solution;
+  }else if( reconstructed==-1 ){
+    return Node::null();
   }else{
     sol = d_solution;
   }
diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
index 9e65be202..1eafe1a93 100644
--- a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
@@ -714,8 +714,10 @@ Node CegConjectureSingleInvSol::reconstructSolution( Node sol, TypeNode stn, int
       }
     }while( !active.empty() );
 
-    //if solution is null, we ran out of elements, return the original solution
-    return sol;
+    // we ran out of elements, return null
+    reconstructed = -1;
+    Warning() << CommandFailure("Cannot get synth function: reconstruction to syntax failed.");
+    return Node::null(); // return sol;
   }
 }
 
diff --git a/src/theory/quantifiers/equality_infer.h b/src/theory/quantifiers/equality_infer.h
index 4c1c93c17..5b714c2d3 100644
--- a/src/theory/quantifiers/equality_infer.h
+++ b/src/theory/quantifiers/equality_infer.h
@@ -17,7 +17,6 @@
 #ifndef __CVC4__THEORY__QUANTIFIERS__EQUALITY_INFER_H
 #define __CVC4__THEORY__QUANTIFIERS__EQUALITY_INFER_H
 
-#include <ext/hash_set>
 #include <iostream>
 #include <map>
 #include <vector>
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index 8d41c75d8..8597755c9 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -17,13 +17,10 @@
 #ifndef __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H
 #define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H
 
-#include "util/hash.h"
-#include "context/cdo.h"
-
-#include <ext/hash_set>
 #include <map>
 
 #include "context/cdlist.h"
+#include "context/cdo.h"
 #include "expr/node.h"
 
 namespace CVC4 {
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 40a5b5849..f46b73b1c 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -17,13 +17,12 @@
 #ifndef __CVC4__THEORY__QUANT_UTIL_H
 #define __CVC4__THEORY__QUANT_UTIL_H
 
-#include "theory/theory.h"
-#include "theory/uf/equality_engine.h"
-
-#include <ext/hash_set>
 #include <iostream>
 #include <map>
 
+#include "theory/theory.h"
+#include "theory/uf/equality_engine.h"
+
 namespace CVC4 {
 namespace theory {
 
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 93390facb..ec5fc633d 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -720,7 +720,7 @@ bool TermDb::reset( Theory::Effort effort ){
     }
   }
   //explicitly add inst closure terms to the equality engine to ensure only EE terms are indexed
-  for( std::hash_set< Node, NodeHashFunction >::iterator it = d_iclosure_processed.begin(); it !=d_iclosure_processed.end(); ++it ){
+  for( std::unordered_set< Node, NodeHashFunction >::iterator it = d_iclosure_processed.begin(); it !=d_iclosure_processed.end(); ++it ){
     Node n = *it;
     if( !ee->hasTerm( n ) ){
       ee->addTerm( n );
@@ -2288,4 +2288,3 @@ Node TermDb::getQAttrQuantIdNumNode( Node q ) {
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
-
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index f187e5989..4650cc5d4 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -17,12 +17,14 @@
 #ifndef __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H
 #define __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H
 
+#include <map>
+#include <unordered_set>
+
 #include "expr/attribute.h"
 #include "theory/theory.h"
 #include "theory/type_enumerator.h"
 #include "theory/quantifiers/quant_util.h"
 
-#include <map>
 
 namespace CVC4 {
 namespace theory {
@@ -194,9 +196,9 @@ private:
   /** reference to the quantifiers engine */
   QuantifiersEngine* d_quantEngine;
   /** terms processed */
-  std::hash_set< Node, NodeHashFunction > d_processed;
+  std::unordered_set< Node, NodeHashFunction > d_processed;
   /** terms processed */
-  std::hash_set< Node, NodeHashFunction > d_iclosure_processed;
+  std::unordered_set< Node, NodeHashFunction > d_iclosure_processed;
   /** select op map */
   std::map< Node, std::map< TypeNode, Node > > d_par_op_map;
   /** whether master equality engine is UF-inconsistent */
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index d1412500e..9c621dbd6 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -19,25 +19,19 @@
 #ifndef __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H
 #define __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H
 
-#include <ext/hash_set>
-#include <iostream>
-#include <map>
-
 #include "context/cdhashmap.h"
+#include "context/context.h"
+#include "expr/node.h"
+#include "theory/output_channel.h"
 #include "theory/theory.h"
-#include "util/hash.h"
+#include "theory/theory_engine.h"
+#include "theory/valuation.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
-class TheoryEngine;
-
 namespace theory {
-
 namespace quantifiers {
 
-class ModelEngine;
-class InstantiationEngine;
-
 class TheoryQuantifiers : public Theory {
 private:
   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index faf14e0c7..fa1394f39 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -1882,7 +1882,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f,
         r_best = r;
       }
       //now, make sure that no other member of the class is an instance
-      std::hash_map<TNode, Node, TNodeHashFunction> cache;
+      std::unordered_map<TNode, Node, TNodeHashFunction> cache;
       r_best = getInstance( r_best, eqc, cache );
       //store that this representative was chosen at this point
       if( d_rep_score.find( r_best )==d_rep_score.end() ){
@@ -2001,7 +2001,7 @@ TNode EqualityQueryQuantifiersEngine::getCongruentTerm( Node f, std::vector< TNo
 
 //helper functions
 
-Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Node >& eqc, std::hash_map<TNode, Node, TNodeHashFunction>& cache ){
+Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map<TNode, Node, TNodeHashFunction>& cache ){
   if(cache.find(n) != cache.end()) {
     return cache[n];
   }
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 92dfcdae5..7d8f5354b 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -17,9 +17,9 @@
 #ifndef __CVC4__THEORY__QUANTIFIERS_ENGINE_H
 #define __CVC4__THEORY__QUANTIFIERS_ENGINE_H
 
-#include <ext/hash_set>
 #include <iostream>
 #include <map>
+#include <unordered_map>
 
 #include "context/cdchunk_list.h"
 #include "context/cdhashset.h"
@@ -449,7 +449,7 @@ private:
   /** processInferences : will merge equivalence classes in master equality engine, if possible */
   bool processInferences( Theory::Effort e );
   /** node contains */
-  Node getInstance( Node n, const std::vector< Node >& eqc, std::hash_map<TNode, Node, TNodeHashFunction>& cache );
+  Node getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map<TNode, Node, TNodeHashFunction>& cache );
   /** get score */
   int getRepScore( Node n, Node f, int index, TypeNode v_tn );
   /** flatten representatives */
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index 27ab7615c..0c20c48a4 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -35,7 +35,7 @@ static TheoryId theoryOf(TNode node) {
 }
 
 #ifdef CVC4_ASSERTIONS
-static CVC4_THREADLOCAL(std::hash_set<Node, NodeHashFunction>*) s_rewriteStack = NULL;
+static CVC4_THREADLOCAL(std::unordered_set<Node, NodeHashFunction>*) s_rewriteStack = NULL;
 #endif /* CVC4_ASSERTIONS */
 
 class RewriterInitializer {
@@ -94,7 +94,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
   bool isEquality = node.getKind() == kind::EQUAL && (!node[0].getType().isBoolean());
 
   if(s_rewriteStack == NULL) {
-    s_rewriteStack = new std::hash_set<Node, NodeHashFunction>();
+    s_rewriteStack = new std::unordered_set<Node, NodeHashFunction>();
   }
 #endif
 
diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index 34c17a34c..beb5e946c 100644
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -27,9 +27,9 @@ namespace sets {
 
 typedef std::map< Node, std::vector< Node > >::iterator                                         MEM_IT;
 typedef std::map< kind::Kind_t, std::vector< Node > >::iterator                                 KIND_TERM_IT;
-typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator                     TC_GRAPH_IT;
+typedef std::map< Node, std::unordered_set< Node, NodeHashFunction > >::iterator                     TC_GRAPH_IT;
 typedef std::map< Node, std::map< kind::Kind_t, std::vector< Node > > >::iterator               TERM_IT;
-typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > > >::iterator   TC_IT;
+typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFunction > > >::iterator   TC_IT;
 
   void TheorySetsRels::check(Theory::Effort level) {
     Trace("rels") << "\n[sets-rels] ******************************* Start the relational solver, effort = " << level << " *******************************\n" << std::endl;
@@ -240,7 +240,7 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction >
     }
 
     Node join_image_rel = join_image_term[0];
-    std::hash_set< Node, NodeHashFunction > hasChecked;
+    std::unordered_set< Node, NodeHashFunction > hasChecked;
     Node join_image_rel_rep = getRepresentative( join_image_rel );
     std::vector< Node >::iterator mem_rep_it = (*rel_mem_it).second.begin();
     MEM_IT rel_mem_exp_it = d_rReps_memberReps_exp_cache.find( join_image_rel_rep );
@@ -480,14 +480,14 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction >
       if( tc_graph_it != (tc_it->second).end() ) {
         (tc_graph_it->second).insert( mem_rep_snd );
       } else {
-        std::hash_set< Node, NodeHashFunction > sets;
+        std::unordered_set< Node, NodeHashFunction > sets;
         sets.insert( mem_rep_snd );
         (tc_it->second)[mem_rep_fst] = sets;
       }
     } else {
       std::map< Node, Node > exp_map;
-      std::hash_set< Node, NodeHashFunction > sets;
-      std::map< Node, std::hash_set<Node, NodeHashFunction> > element_map;
+      std::unordered_set< Node, NodeHashFunction > sets;
+      std::map< Node, std::unordered_set<Node, NodeHashFunction> > element_map;
       sets.insert( mem_rep_snd );
       element_map[mem_rep_fst] = sets;
       d_tcr_tcGraph[tc_rel] = element_map;
@@ -529,7 +529,7 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction >
     TC_IT tc_it = d_rRep_tcGraph.find( getRepresentative(tc_rel[0]) );
     if( tc_it != d_rRep_tcGraph.end() ) {
       bool isReachable = false;
-      std::hash_set<Node, NodeHashFunction> seen;
+      std::unordered_set<Node, NodeHashFunction> seen;
       isTCReachable( getRepresentative( RelsUtils::nthElementOfTuple(mem_rep, 0) ),
                      getRepresentative( RelsUtils::nthElementOfTuple(mem_rep, 1) ), seen, tc_it->second, isReachable );
       return isReachable;
@@ -537,8 +537,8 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction >
     return false;
   }
 
-  void TheorySetsRels::isTCReachable( Node start, Node dest, std::hash_set<Node, NodeHashFunction>& hasSeen,
-                                    std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable ) {
+  void TheorySetsRels::isTCReachable( Node start, Node dest, std::unordered_set<Node, NodeHashFunction>& hasSeen,
+                                    std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable ) {
     if(hasSeen.find(start) == hasSeen.end()) {
       hasSeen.insert(start);
     }
@@ -550,7 +550,7 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction >
         isReachable = true;
         return;
       } else {
-        std::hash_set< Node, NodeHashFunction >::iterator set_it = pair_set_it->second.begin();
+        std::unordered_set< Node, NodeHashFunction >::iterator set_it = pair_set_it->second.begin();
 
         while( set_it != pair_set_it->second.end() ) {
           // need to check if *set_it has been looked already
@@ -565,7 +565,7 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction >
 
   void TheorySetsRels::buildTCGraphForRel( Node tc_rel ) {
     std::map< Node, Node > rel_tc_graph_exps;
-    std::map< Node, std::hash_set<Node, NodeHashFunction> > rel_tc_graph;
+    std::map< Node, std::unordered_set<Node, NodeHashFunction> > rel_tc_graph;
 
     Node rel_rep = getRepresentative( tc_rel[0] );
     Node tc_rel_rep = getRepresentative( tc_rel );
@@ -576,10 +576,10 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction >
       Node fst_element_rep = getRepresentative( RelsUtils::nthElementOfTuple( members[i], 0 ));
       Node snd_element_rep = getRepresentative( RelsUtils::nthElementOfTuple( members[i], 1 ));
       Node tuple_rep = RelsUtils::constructPair( rel_rep, fst_element_rep, snd_element_rep );
-      std::map< Node, std::hash_set<Node, NodeHashFunction> >::iterator rel_tc_graph_it = rel_tc_graph.find( fst_element_rep );
+      std::map< Node, std::unordered_set<Node, NodeHashFunction> >::iterator rel_tc_graph_it = rel_tc_graph.find( fst_element_rep );
 
       if( rel_tc_graph_it == rel_tc_graph.end() ) {
-        std::hash_set< Node, NodeHashFunction > snd_elements;
+        std::unordered_set< Node, NodeHashFunction > snd_elements;
         snd_elements.insert( snd_element_rep );
         rel_tc_graph[fst_element_rep] = snd_elements;
         rel_tc_graph_exps[tuple_rep] = exps[i];
@@ -596,13 +596,13 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction >
     }
   }
 
-  void TheorySetsRels::doTCInference( std::map< Node, std::hash_set<Node, NodeHashFunction> > rel_tc_graph, std::map< Node, Node > rel_tc_graph_exps, Node tc_rel ) {
+  void TheorySetsRels::doTCInference( std::map< Node, std::unordered_set<Node, NodeHashFunction> > rel_tc_graph, std::map< Node, Node > rel_tc_graph_exps, Node tc_rel ) {
     Trace("rels-debug") << "[Theory::Rels] ****** doTCInference !" << std::endl;
     for( TC_GRAPH_IT tc_graph_it = rel_tc_graph.begin(); tc_graph_it != rel_tc_graph.end(); tc_graph_it++ ) {
-      for( std::hash_set< Node, NodeHashFunction >::iterator snd_elements_it = tc_graph_it->second.begin();
+      for( std::unordered_set< Node, NodeHashFunction >::iterator snd_elements_it = tc_graph_it->second.begin();
            snd_elements_it != tc_graph_it->second.end(); snd_elements_it++ ) {
         std::vector< Node > reasons;
-        std::hash_set<Node, NodeHashFunction> seen;
+        std::unordered_set<Node, NodeHashFunction> seen;
         Node tuple = RelsUtils::constructPair( tc_rel, getRepresentative( tc_graph_it->first ), getRepresentative( *snd_elements_it) );
         Assert( rel_tc_graph_exps.find( tuple ) != rel_tc_graph_exps.end() );
         Node exp   = rel_tc_graph_exps.find( tuple )->second;
@@ -615,8 +615,8 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction >
     Trace("rels-debug") << "[Theory::Rels] ****** Done with doTCInference !" << std::endl;
   }
 
-  void TheorySetsRels::doTCInference(Node tc_rel, std::vector< Node > reasons, std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph,
-                                       std::map< Node, Node >& rel_tc_graph_exps, Node start_node_rep, Node cur_node_rep, std::hash_set< Node, NodeHashFunction >& seen ) {
+  void TheorySetsRels::doTCInference(Node tc_rel, std::vector< Node > reasons, std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph,
+                                       std::map< Node, Node >& rel_tc_graph_exps, Node start_node_rep, Node cur_node_rep, std::unordered_set< Node, NodeHashFunction >& seen ) {
     Node tc_mem = RelsUtils::constructPair( tc_rel, RelsUtils::nthElementOfTuple((reasons.front())[0], 0), RelsUtils::nthElementOfTuple((reasons.back())[0], 1) );
     std::vector< Node > all_reasons( reasons );
 
@@ -646,7 +646,7 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction >
     seen.insert( cur_node_rep );
     TC_GRAPH_IT  cur_set = tc_graph.find( cur_node_rep );
     if( cur_set != tc_graph.end() ) {
-      for( std::hash_set< Node, NodeHashFunction >::iterator set_it = cur_set->second.begin();
+      for( std::unordered_set< Node, NodeHashFunction >::iterator set_it = cur_set->second.begin();
            set_it != cur_set->second.end(); set_it++ ) {
         Node new_pair = RelsUtils::constructPair( tc_rel, cur_node_rep, *set_it );
         std::vector< Node > new_reasons( reasons );
diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h
index 16770671a..eb97405dc 100644
--- a/src/theory/sets/theory_sets_rels.h
+++ b/src/theory/sets/theory_sets_rels.h
@@ -17,11 +17,13 @@
 #ifndef SRC_THEORY_SETS_THEORY_SETS_RELS_H_
 #define SRC_THEORY_SETS_THEORY_SETS_RELS_H_
 
-#include "theory/theory.h"
-#include "theory/uf/equality_engine.h"
-#include "context/cdhashset.h"
+#include <unordered_set>
+
 #include "context/cdchunk_list.h"
+#include "context/cdhashset.h"
 #include "theory/sets/rels_utils.h"
+#include "theory/theory.h"
+#include "theory/uf/equality_engine.h"
 
 namespace CVC4 {
 namespace theory {
@@ -103,12 +105,12 @@ private:
   std::map< Node, Node >        d_pending_facts;
 
 
-  std::hash_set< Node, NodeHashFunction >       d_rel_nodes;
+  std::unordered_set< Node, NodeHashFunction >       d_rel_nodes;
   std::map< Node, std::vector<Node> >           d_tuple_reps;
   std::map< Node, TupleTrie >                   d_membership_trie;
 
   /** Symbolic tuple variables that has been reduced to concrete ones */
-  std::hash_set< Node, NodeHashFunction >       d_symbolic_tuples;
+  std::unordered_set< Node, NodeHashFunction >       d_symbolic_tuples;
 
   /** Mapping between relation and its member representatives */
   std::map< Node, std::vector< Node > >           d_rReps_memberReps_cache;
@@ -120,8 +122,8 @@ private:
   std::map< Node, std::map<kind::Kind_t, std::vector<Node> > >                  d_terms_cache;
 
   /** Mapping between transitive closure relation TC(r) and its TC graph constructed based on the members of r*/
-  std::map< Node, std::map< Node, std::hash_set<Node, NodeHashFunction> > >     d_rRep_tcGraph;
-  std::map< Node, std::map< Node, std::hash_set<Node, NodeHashFunction> > >     d_tcr_tcGraph;
+  std::map< Node, std::map< Node, std::unordered_set<Node, NodeHashFunction> > >     d_rRep_tcGraph;
+  std::map< Node, std::map< Node, std::unordered_set<Node, NodeHashFunction> > >     d_tcr_tcGraph;
   std::map< Node, std::map< Node, Node > > d_tcr_tcGraph_exps;
   std::map< Node, std::vector< Node > > d_tc_lemmas_last;
 
@@ -154,9 +156,9 @@ private:
   void applyTCRule( Node mem, Node rel, Node rel_rep, Node exp);
   void buildTCGraphForRel( Node tc_rel );
   void doTCInference();
-  void doTCInference( std::map< Node, std::hash_set<Node, NodeHashFunction> > rel_tc_graph, std::map< Node, Node > rel_tc_graph_exps, Node tc_rel );
-  void doTCInference(Node tc_rel, std::vector< Node > reasons, std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph,
-                       std::map< Node, Node >& rel_tc_graph_exps, Node start_node_rep, Node cur_node_rep, std::hash_set< Node, NodeHashFunction >& seen );
+  void doTCInference( std::map< Node, std::unordered_set<Node, NodeHashFunction> > rel_tc_graph, std::map< Node, Node > rel_tc_graph_exps, Node tc_rel );
+  void doTCInference(Node tc_rel, std::vector< Node > reasons, std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph,
+                       std::map< Node, Node >& rel_tc_graph_exps, Node start_node_rep, Node cur_node_rep, std::unordered_set< Node, NodeHashFunction >& seen );
 
   void composeMembersForRels( Node );
   void computeMembersForBinOpRel( Node );
@@ -165,8 +167,8 @@ private:
   void computeMembersForJoinImageTerm( Node );
 
   bool isTCReachable( Node mem_rep, Node tc_rel );
-  void isTCReachable( Node start, Node dest, std::hash_set<Node, NodeHashFunction>& hasSeen,
-                    std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable );
+  void isTCReachable( Node start, Node dest, std::unordered_set<Node, NodeHashFunction>& hasSeen,
+                    std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable );
 
 
   void addSharedTerm( TNode n );
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index 3cce08398..8c3fe67d3 100644
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -25,7 +25,7 @@ namespace theory {
 namespace sets {
 
 typedef std::set<TNode> Elements;
-typedef std::hash_map<TNode, Elements, TNodeHashFunction> SettermElementsMap;
+typedef std::unordered_map<TNode, Elements, TNodeHashFunction> SettermElementsMap;
 
 struct FlattenedNodeTag {};
 typedef expr::Attribute<FlattenedNodeTag, bool> flattened;
@@ -50,7 +50,7 @@ RewriteResponse flattenNode(TNode n, TNode trivialNode, TNode skipNode)
     return RewriteResponse(REWRITE_DONE, n);
   }
 
-  typedef std::hash_set<TNode, TNodeHashFunction> node_set;
+  typedef std::unordered_set<TNode, TNodeHashFunction> node_set;
 
   node_set visited;
   visited.insert(skipNode);
diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h
index 6b78a1698..5ca625751 100644
--- a/src/theory/shared_terms_database.h
+++ b/src/theory/shared_terms_database.h
@@ -17,6 +17,8 @@
 
 #pragma once
 
+#include <unordered_map>
+
 #include "context/cdhashset.h"
 #include "expr/node.h"
 #include "theory/theory.h"
@@ -43,7 +45,7 @@ private:
   IntStat d_statSharedTerms;
 
   // Needs to be a map from Nodes as after a backtrack they might not exist
-  typedef std::hash_map<Node, shared_terms_list, TNodeHashFunction> SharedTermsMap;
+  typedef std::unordered_map<Node, shared_terms_list, TNodeHashFunction> SharedTermsMap;
 
   /** A map from atoms to a list of shared terms */
   SharedTermsMap d_atomsToTerms;
diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h
index 5a6618175..cca39a62e 100644
--- a/src/theory/substitutions.h
+++ b/src/theory/substitutions.h
@@ -19,9 +19,10 @@
 #ifndef __CVC4__THEORY__SUBSTITUTIONS_H
 #define __CVC4__THEORY__SUBSTITUTIONS_H
 
+//#include <algorithm>
 #include <utility>
 #include <vector>
-#include <algorithm>
+#include <unordered_map>
 
 #include "expr/node.h"
 #include "context/context.h"
@@ -51,7 +52,7 @@ public:
 
 private:
 
-  typedef std::hash_map<Node, Node, NodeHashFunction> NodeCache;
+  typedef std::unordered_map<Node, Node, NodeHashFunction> NodeCache;
 
   /** The variables, in order of addition */
   NodeMap d_substitutions;
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;
 
   /**
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index f010798cd..8509e84ab 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -220,8 +220,8 @@ void Theory::debugPrintFacts() const{
   printFacts(DebugChannel.getStream());
 }
 
-std::hash_set<TNode, TNodeHashFunction> Theory::currentlySharedTerms() const{
-  std::hash_set<TNode, TNodeHashFunction> currentlyShared;
+std::unordered_set<TNode, TNodeHashFunction> Theory::currentlySharedTerms() const{
+  std::unordered_set<TNode, TNodeHashFunction> currentlyShared;
   for (shared_terms_iterator i = shared_terms_begin(),
            i_end = shared_terms_end(); i != i_end; ++i) {
     currentlyShared.insert (*i);
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 82607a165..73102a6e2 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -19,11 +19,11 @@
 #ifndef __CVC4__THEORY__THEORY_H
 #define __CVC4__THEORY__THEORY_H
 
-#include <ext/hash_set>
 #include <iosfwd>
 #include <map>
 #include <set>
 #include <string>
+#include <unordered_set>
 
 #include "context/cdlist.h"
 #include "context/cdhashset.h"
@@ -760,7 +760,7 @@ public:
    * This is a utility function for constructing a copy of the currently shared terms
    * in a queriable form.  As this is
    */
-  std::hash_set<TNode, TNodeHashFunction> currentlySharedTerms() const;
+  std::unordered_set<TNode, TNodeHashFunction> currentlySharedTerms() const;
 
   /**
    * This allows the theory to be queried for whether a literal, lit, is
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 7369b7c1f..1023071dc 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1645,7 +1645,7 @@ Node TheoryEngine::getExplanation(TNode node) {
 struct AtomsCollect {
 
   std::vector<TNode> d_atoms;
-  std::hash_set<TNode, TNodeHashFunction> d_visited;
+  std::unordered_set<TNode, TNodeHashFunction> d_visited;
 
 public:
 
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 82283ef7b..408bff228 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -21,6 +21,7 @@
 
 #include <deque>
 #include <set>
+#include <unordered_map>
 #include <vector>
 #include <utility>
 
@@ -189,8 +190,8 @@ class TheoryEngine {
   theory::TheoryEngineModelBuilder* d_curr_model_builder;
   bool d_aloc_curr_model_builder;
 
-  typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
-  typedef std::hash_map<TNode, Node, TNodeHashFunction> TNodeMap;
+  typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
+  typedef std::unordered_map<TNode, Node, TNodeHashFunction> TNodeMap;
 
   /**
   * Cache for theory-preprocessing of assertions
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index b9a08e3ac..0f92f976e 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -132,7 +132,7 @@ Cardinality TheoryModel::getCardinality( Type t ) const{
 
 Node TheoryModel::getModelValue(TNode n, bool hasBoundVars, bool useDontCares) const
 {
-  std::hash_map<Node, Node, NodeHashFunction>::iterator it = d_modelCache.find(n);
+  std::unordered_map<Node, Node, NodeHashFunction>::iterator it = d_modelCache.find(n);
   if (it != d_modelCache.end()) {
     return (*it).second;
   }
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index 126de1e46..c1c57795b 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -17,6 +17,9 @@
 #ifndef __CVC4__THEORY__THEORY_MODEL_H
 #define __CVC4__THEORY__THEORY_MODEL_H
 
+#include <unordered_map>
+#include <unordered_set>
+
 #include "smt/model.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/rep_set.h"
@@ -52,7 +55,7 @@ public:
   /** true/false nodes */
   Node d_true;
   Node d_false;
-  mutable std::hash_map<Node, Node, NodeHashFunction> d_modelCache;
+  mutable std::unordered_map<Node, Node, NodeHashFunction> d_modelCache;
 public: 
   /** comment stream to include in printing */
   std::stringstream d_comment_str;
@@ -140,8 +143,8 @@ public:
  */
 class TypeSet {
 public:
-  typedef std::hash_map<TypeNode, std::set<Node>*, TypeNodeHashFunction> TypeSetMap;
-  typedef std::hash_map<TypeNode, TypeEnumerator*, TypeNodeHashFunction> TypeToTypeEnumMap;
+  typedef std::unordered_map<TypeNode, std::set<Node>*, TypeNodeHashFunction> TypeSetMap;
+  typedef std::unordered_map<TypeNode, TypeEnumerator*, TypeNodeHashFunction> TypeToTypeEnumMap;
   typedef TypeSetMap::iterator iterator;
   typedef TypeSetMap::const_iterator const_iterator;
 private:
@@ -265,9 +268,9 @@ class TheoryEngineModelBuilder : public ModelBuilder
 protected:
   /** pointer to theory engine */
   TheoryEngine* d_te;
-  typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
+  typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
   NodeMap d_normalizedCache;
-  typedef std::hash_set<Node, NodeHashFunction> NodeSet;
+  typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
   std::map< Node, Node > d_constantReps;
 
   /** process build model */
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 7c8e27575..5be32ab90 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -20,8 +20,8 @@
 #pragma once
 
 #include <deque>
-#include <ext/hash_map>
 #include <queue>
+#include <unordered_map>
 #include <vector>
 
 #include "base/output.h"
@@ -234,10 +234,10 @@ private:
   std::map<unsigned, const PathReconstructionNotify*> d_pathReconstructionTriggers;
 
   /** Map from nodes to their ids */
-  __gnu_cxx::hash_map<TNode, EqualityNodeId, TNodeHashFunction> d_nodeIds;
+  std::unordered_map<TNode, EqualityNodeId, TNodeHashFunction> d_nodeIds;
 
   /** Map from function applications to their ids */
-  typedef __gnu_cxx::hash_map<FunctionApplication, EqualityNodeId, FunctionApplicationHashFunction> ApplicationIdsMap;
+  typedef std::unordered_map<FunctionApplication, EqualityNodeId, FunctionApplicationHashFunction> ApplicationIdsMap;
 
   /**
    * A map from a pair (a', b') to a function application f(a, b), where a' and b' are the current representatives
@@ -611,7 +611,7 @@ private:
    */
   std::vector<TriggerTermSetRef> d_nodeIndividualTrigger;
 
-  typedef std::hash_map<EqualityPair, DisequalityReasonRef, EqualityPairHashFunction> DisequalityReasonsMap;
+  typedef std::unordered_map<EqualityPair, DisequalityReasonRef, EqualityPairHashFunction> DisequalityReasonsMap;
 
   /**
    * A map from pairs of disequal terms, to the reason why we deduced they are disequal.
diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp
index cffa367cf..8a1c30ba6 100644
--- a/src/theory/uf/symmetry_breaker.cpp
+++ b/src/theory/uf/symmetry_breaker.cpp
@@ -61,7 +61,7 @@ SymmetryBreaker::Template::Template() :
 }
 
 TNode SymmetryBreaker::Template::find(TNode n) {
-  hash_map<TNode, TNode, TNodeHashFunction>::iterator i = d_reps.find(n);
+  unordered_map<TNode, TNode, TNodeHashFunction>::iterator i = d_reps.find(n);
   if(i == d_reps.end()) {
     return n;
   } else {
@@ -400,8 +400,8 @@ void SymmetryBreaker::assertFormula(TNode phi) {
         break;
       }
     }
-    hash_map<TNode, set<TNode>, TNodeHashFunction>& ps = t.partitions();
-    for(hash_map<TNode, set<TNode>, TNodeHashFunction>::iterator i = ps.begin();
+    unordered_map<TNode, set<TNode>, TNodeHashFunction>& ps = t.partitions();
+    for(unordered_map<TNode, set<TNode>, TNodeHashFunction>::iterator i = ps.begin();
         i != ps.end();
         ++i) {
       Debug("ufsymm") << "UFSYMM partition*: " << (*i).first;
@@ -421,9 +421,9 @@ void SymmetryBreaker::assertFormula(TNode phi) {
   }
   if(!d_template.match(phi)) {
     // we hit a bad match, extract the partitions and reset the template
-    hash_map<TNode, set<TNode>, TNodeHashFunction>& ps = d_template.partitions();
+    unordered_map<TNode, set<TNode>, TNodeHashFunction>& ps = d_template.partitions();
     Debug("ufsymm") << "UFSYMM hit a bad match---have " << ps.size() << " partitions:" << endl;
-    for(hash_map<TNode, set<TNode>, TNodeHashFunction>::iterator i = ps.begin();
+    for(unordered_map<TNode, set<TNode>, TNodeHashFunction>::iterator i = ps.begin();
         i != ps.end();
         ++i) {
       Debug("ufsymm") << "UFSYMM partition: " << (*i).first;
diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h
index a814c670b..64ca41df2 100644
--- a/src/theory/uf/symmetry_breaker.h
+++ b/src/theory/uf/symmetry_breaker.h
@@ -46,6 +46,7 @@
 
 #include <iostream>
 #include <list>
+#include <unordered_map>
 #include <vector>
 
 #include "context/cdlist.h"
@@ -64,8 +65,8 @@ class SymmetryBreaker : public context::ContextNotifyObj {
   class Template {
     Node d_template;
     NodeBuilder<> d_assertions;
-    std::hash_map<TNode, std::set<TNode>, TNodeHashFunction> d_sets;
-    std::hash_map<TNode, TNode, TNodeHashFunction> d_reps;
+    std::unordered_map<TNode, std::set<TNode>, TNodeHashFunction> d_sets;
+    std::unordered_map<TNode, TNode, TNodeHashFunction> d_reps;
 
     TNode find(TNode n);
     bool matchRecursive(TNode t, TNode n);
@@ -73,7 +74,7 @@ class SymmetryBreaker : public context::ContextNotifyObj {
   public:
     Template();
     bool match(TNode n);
-    std::hash_map<TNode, std::set<TNode>, TNodeHashFunction>& partitions() { return d_sets; }
+    std::unordered_map<TNode, std::set<TNode>, TNodeHashFunction>& partitions() { return d_sets; }
     Node assertions() {
       switch(d_assertions.getNumChildren()) {
       case 0: return Node::null();
@@ -91,7 +92,7 @@ public:
   typedef TNode Term;
   typedef std::list<Term> Terms;
   typedef std::set<Term> TermEq;
-  typedef std::hash_map<Term, TermEq, TNodeHashFunction> TermEqs;
+  typedef std::unordered_map<Term, TermEq, TNodeHashFunction> TermEqs;
 
 private:
 
@@ -113,7 +114,7 @@ private:
   Permutations d_permutations;
   Terms d_terms;
   Template d_template;
-  std::hash_map<Node, Node, NodeHashFunction> d_normalizationCache;
+  std::unordered_map<Node, Node, NodeHashFunction> d_normalizationCache;
   TermEqs d_termEqs;
   TermEqs d_termEqsOnly;
 
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 783585f8f..6d4d96a87 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -300,7 +300,7 @@ void TheoryUF::ppStaticLearn(TNode n, NodeBuilder<>& learned) {
 
   vector<TNode> workList;
   workList.push_back(n);
-  __gnu_cxx::hash_set<TNode, TNodeHashFunction> processed;
+  std::unordered_set<TNode, TNodeHashFunction> processed;
 
   while(!workList.empty()) {
     n = workList.back();
diff --git a/src/theory/unconstrained_simplifier.h b/src/theory/unconstrained_simplifier.h
index a32dd076e..04c32f408 100644
--- a/src/theory/unconstrained_simplifier.h
+++ b/src/theory/unconstrained_simplifier.h
@@ -20,8 +20,10 @@
 #ifndef __CVC4__UNCONSTRAINED_SIMPLIFIER_H
 #define __CVC4__UNCONSTRAINED_SIMPLIFIER_H
 
-#include <vector>
+#include <unordered_map>
+#include <unordered_set>
 #include <utility>
+#include <vector>
 
 #include "expr/node.h"
 #include "theory/substitutions.h"
@@ -37,9 +39,9 @@ class UnconstrainedSimplifier {
   /** number of expressions eliminated due to unconstrained simplification */
   IntStat d_numUnconstrainedElim;
 
-  typedef std::hash_map<TNode, unsigned, TNodeHashFunction> TNodeCountMap;
-  typedef std::hash_map<TNode, TNode, TNodeHashFunction> TNodeMap;
-  typedef std::hash_set<TNode, TNodeHashFunction> TNodeSet;
+  typedef std::unordered_map<TNode, unsigned, TNodeHashFunction> TNodeCountMap;
+  typedef std::unordered_map<TNode, TNode, TNodeHashFunction> TNodeMap;
+  typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
 
   TNodeCountMap d_visited;
   TNodeMap d_visitedOnce;
diff --git a/src/util/cache.h b/src/util/cache.h
index 6f5bac8eb..38dc0fc99 100644
--- a/src/util/cache.h
+++ b/src/util/cache.h
@@ -21,8 +21,10 @@
 #ifndef __CVC4__CACHE_H
 #define __CVC4__CACHE_H
 
-#include <utility>
 #include <functional>
+#include <unordered_map>
+#include <utility>
+#include <vector>
 
 namespace CVC4 {
 
@@ -33,7 +35,7 @@ namespace CVC4 {
  */
 template <class T, class U, class Hasher = std::hash<T> >
 class Cache {
-  typedef std::hash_map<T, U, Hasher> Map;
+  typedef std::unordered_map<T, U, Hasher> Map;
   Map d_map;
   std::vector<T> d_current;
   typename Map::iterator d_result;
diff --git a/src/util/hash.h b/src/util/hash.h
index af468e25b..b04fb8bb5 100644
--- a/src/util/hash.h
+++ b/src/util/hash.h
@@ -20,13 +20,10 @@
 #ifndef __CVC4__HASH_H
 #define __CVC4__HASH_H
 
-// in case it's not been declared as a namespace yet
-namespace __gnu_cxx {}
+#include <functional>
+#include <string>
 
-#include <ext/hash_map>
-#include <ext/hash_set>
-
-namespace __gnu_cxx {
+namespace std {
 
 #ifdef CVC4_NEED_HASH_UINT64_T
 // on some versions and architectures of GNU C++, we need a
@@ -39,18 +36,10 @@ struct hash<uint64_t> {
 };/* struct hash<uint64_t> */
 #endif /* CVC4_NEED_HASH_UINT64_T */
 
-}/* __gnu_cxx namespace */
-
-// hackish: treat hash stuff as if it were in std namespace
-namespace std { using namespace __gnu_cxx; }
+}/* std namespace */
 
 namespace CVC4 {
 
-struct StringHashFunction {
-  size_t operator()(const std::string& str) const {
-    return __gnu_cxx::hash<const char*>()(str.c_str());
-  }
-};/* struct StringHashFunction */
 
 template <class T, class U, class HashT = std::hash<T>, class HashU = std::hash<U> >
 struct PairHashFunction {
diff --git a/src/util/hash.i b/src/util/hash.i
index 470447fc3..f2f1e6652 100644
--- a/src/util/hash.i
+++ b/src/util/hash.i
@@ -2,6 +2,4 @@
 #include "util/hash.h"
 %}
 
-%rename(apply) CVC4::StringHashFunction::operator()(const std::string&) const;
-
 %include "util/hash.h"
diff --git a/src/util/proof.h b/src/util/proof.h
index af68efa97..b34e4aed9 100644
--- a/src/util/proof.h
+++ b/src/util/proof.h
@@ -21,7 +21,7 @@
 #define __CVC4__PROOF_H
 
 #include <iosfwd>
-#include <ext/hash_map>
+#include <unordered_map>
 
 namespace CVC4 {
 
@@ -29,7 +29,7 @@ class Expr;
 class ProofLetCount;
 struct ExprHashFunction;
 
-typedef __gnu_cxx::hash_map<Expr, ProofLetCount, ExprHashFunction> ProofLetMap;
+typedef std::unordered_map<Expr, ProofLetCount, ExprHashFunction> ProofLetMap;
 
 class CVC4_PUBLIC Proof {
 public:
diff --git a/src/util/regexp.h b/src/util/regexp.h
index 9fb8aea60..f451a8dec 100644
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -21,6 +21,7 @@
 #define __CVC4__REGEXP_H
 
 #include <cstddef>
+#include <functional>
 #include <ostream>
 #include <string>
 #include <vector>