diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 9f5799a45..85286056f 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -217,6 +217,8 @@ theory_seq::theory_seq(ast_manager& m):
     m_new_solution(false),
     m_new_propagation(false),
     m_len_prop_lvl(-1),
+    m_overlap(m),
+    m_overlap2(m),
     m_mk_aut(m) {
     m_prefix         = "seq.p.suffix";
     m_suffix         = "seq.s.prefix";
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index 3d786ddff..85ec35557 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -29,6 +29,7 @@ Revision History:
 #include "math/automata/automaton.h"
 #include "ast/rewriter/seq_rewriter.h"
 #include "util/union_find.h"
+#include "util/obj_ref_hashtable.h"
 
 namespace smt {
 
@@ -301,8 +302,8 @@ namespace smt {
         unsigned                   m_eq_id;
         th_union_find              m_find;
 
-        obj_map<expr, unsigned_vector>        m_overlap;
-        obj_map<expr, unsigned_vector>        m_overlap2;
+        obj_ref_map<ast_manager, expr, unsigned_vector>    m_overlap;
+        obj_ref_map<ast_manager, expr, unsigned_vector>    m_overlap2;
         obj_map<enode, obj_map<enode, int>>   m_len_offset;
         int                                   m_len_prop_lvl;
 
diff --git a/src/util/obj_ref_hashtable.h b/src/util/obj_ref_hashtable.h
index 3d6bbf883..23a2a1867 100644
--- a/src/util/obj_ref_hashtable.h
+++ b/src/util/obj_ref_hashtable.h
@@ -26,7 +26,7 @@ class obj_ref_map {
     M&                  m;
     obj_map<Key, Value> m_table;
 public:
-    typedef typename obj_map<Key, Value> iterator;
+    typedef typename obj_map<Key, Value>::iterator iterator;
     typedef Key key;
     typedef Value value;
     typedef typename obj_map<Key, Value>::key_data key_data;