diff --git a/src/smt/seq/seq_model.cpp b/src/smt/seq/seq_model.cpp
index efea5c13a..2cbbf17ba 100644
--- a/src/smt/seq/seq_model.cpp
+++ b/src/smt/seq/seq_model.cpp
@@ -17,7 +17,6 @@ Author:
 
 --*/
 #include "smt/seq/seq_model.h"
-#include "smt/theory_nseq.h"
 #include "smt/seq/seq_regex.h"
 #include "smt/seq/seq_state.h"
 #include "smt/smt_context.h"
@@ -27,9 +26,9 @@ Author:
 
 namespace smt {
 
-    seq_model::seq_model(theory_nseq& th, ast_manager& m, seq_util& seq,
+    seq_model::seq_model(ast_manager& m, seq_util& seq,
                            seq_rewriter& rw, euf::sgraph& sg, seq::seq_regex& regex)
-        : m_th(th), m(m), m_seq(seq), m_rewriter(rw), m_sg(sg), m_regex(regex), m_trail(m)
+        : m(m), m_seq(seq), m_rewriter(rw), m_sg(sg), m_regex(regex), m_trail(m)
     {}
 
     void seq_model::init(model_generator& mg, seq::nielsen_graph& nielsen, seq_state const& state) {
@@ -39,7 +38,7 @@ namespace smt {
         m_int_model = nullptr;
         m_mg = &mg;
 
-        m_factory = alloc(seq_factory, m, m_th.get_family_id(), mg.get_model());
+        m_factory = alloc(seq_factory, m, m_seq.get_family_id(), mg.get_model());
         mg.register_factory(m_factory);
 
         register_existing_values(nielsen);
diff --git a/src/smt/seq/seq_model.h b/src/smt/seq/seq_model.h
index f36cbbc5b..533d253aa 100644
--- a/src/smt/seq/seq_model.h
+++ b/src/smt/seq/seq_model.h
@@ -31,7 +31,6 @@ Author:
 #include "ast/seq_decl_plugin.h"
 #include "ast/rewriter/seq_rewriter.h"
 #include "ast/euf/euf_sgraph.h"
-#include "smt/smt_types.h"
 #include "smt/seq/seq_nielsen.h"
 #include "model/seq_factory.h"
 
@@ -43,12 +42,12 @@ namespace seq {
 
 namespace smt {
 
-    class theory_nseq;
+    class enode;
+    class model_generator;
     class seq_state;
     class model_value_proc;
 
     class seq_model {
-        theory_nseq&    m_th;
         ast_manager&    m;
         seq_util&       m_seq;
         seq_rewriter&   m_rewriter;
@@ -74,7 +73,7 @@ namespace smt {
         u_map<euf::snode*> m_var_regex;
 
     public:
-        seq_model(theory_nseq& th, ast_manager& m, seq_util& seq,
+        seq_model(ast_manager& m, seq_util& seq,
                    seq_rewriter& rw, euf::sgraph& sg, seq::seq_regex& regex);
 
         // Phase 1: initialize model construction.
diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp
index 952bab29f..a784f582d 100644
--- a/src/smt/theory_nseq.cpp
+++ b/src/smt/theory_nseq.cpp
@@ -37,7 +37,7 @@ namespace smt {
         m_nielsen(m_sgraph, m_context_solver),
         m_state(m_sgraph),
         m_regex(m_sgraph),
-        m_model(*this, ctx.get_manager(), m_seq, m_rewriter, m_sgraph, m_regex)
+        m_model(ctx.get_manager(), m_seq, m_rewriter, m_sgraph, m_regex)
     {}
 
     // -----------------------------------------------------------------------