diff --git a/src/smt/nseq_context_solver.h b/src/smt/nseq_context_solver.h
index 2c2b07616..b704dcf84 100644
--- a/src/smt/nseq_context_solver.h
+++ b/src/smt/nseq_context_solver.h
@@ -45,10 +45,9 @@ namespace smt {
      *
      * Assertions with dep == nullptr are asserted directly (always active).
      */
-    class context_solver : public seq::simple_solver {
+    class sub_solver : public seq::sub_solver_i {
         smt_params      m_params;    // must be declared before m_kernel
         kernel          m_kernel;
-        arith_value     m_arith_value;
 
         // Tracked assumption literals.
         // m_assump_lits[i] and m_frame_bounds together encode a stack of
@@ -69,12 +68,10 @@ namespace smt {
         }
 
     public:
-        context_solver(ast_manager& m) :
+        sub_solver(ast_manager& m) :
             m_params(make_seq_len_params()),
             m_kernel(m, m_params),
-            m_arith_value(m),
             m_assump_lits(m) {
-            m_arith_value.init(&m_kernel.get_context());
         }
 
         lbool check() override {
@@ -137,23 +134,8 @@ namespace smt {
 
         seq::dep_tracker core() override { return m_last_core; }
 
-        bool lower_bound(expr* e, rational& lo, literal_vector& lits, enode_pair_vector& eqs) const override {
-            bool is_strict = true;
-            return m_arith_value.get_lo(e, lo, is_strict, lits, eqs) && !is_strict && lo.is_int();
-        }
-
-        bool upper_bound(expr* e, rational& hi, literal_vector& lits, enode_pair_vector& eqs) const override {
-            bool is_strict = true;
-            return m_arith_value.get_up(e, hi, is_strict, lits, eqs) && !is_strict && hi.is_int();
-        }
-
-        bool current_value(expr* e, rational& v) const override {
-            return m_arith_value.get_value(e, v) && v.is_int();
-        }
-
         void reset() override {
             m_kernel.reset();
-            m_arith_value.init(&m_kernel.get_context());
             m_assump_lits.reset();
             m_assump_lit2id.reset();
             m_frame_bounds.reset();
@@ -163,4 +145,55 @@ namespace smt {
         }
     };
 
+    class context_solver : public seq::context_solver_i {
+        smt::context &ctx;
+        arith_value m_arith_value;
+    public:
+        context_solver(smt::context& ctx): 
+            ctx(ctx), 
+            m_arith_value(ctx.get_manager()) {
+            m_arith_value.init(&ctx);
+        }
+
+        bool lower_bound(expr *e, rational &lo, literal_vector &lits, enode_pair_vector &eqs) const override {
+            bool is_strict = true;
+            return m_arith_value.get_lo(e, lo, is_strict, lits, eqs) && !is_strict && lo.is_int();
+        }
+
+        bool upper_bound(expr *e, rational &hi, literal_vector &lits, enode_pair_vector &eqs) const override {
+            bool is_strict = true;
+            return m_arith_value.get_up(e, hi, is_strict, lits, eqs) && !is_strict && hi.is_int();
+        }
+
+        bool current_value(expr *e, rational &v) const override {
+            return m_arith_value.get_value(e, v) && v.is_int();
+        }
+
+        sat::literal literal_if_false(expr *e) {
+            bool is_not = ctx.get_manager().is_not(e, e);
+            if (m_should_internalize && !ctx.b_internalized(e)) {
+                // it can happen that the element is not internalized, but as soon as we do it, it becomes false.
+                // In case we just skip one of those uninternalized expressions,
+                // adding the Nielsen assumption later will fail
+                // Alternatively, we could just retry Nielsen saturation in case
+                // adding the Nielsen assumption yields the assumption being false after internalizing
+                ctx.internalize(to_app(e), false);
+            }
+
+            if (!ctx.b_internalized(e))
+                return sat::null_literal;
+
+            literal lit = ctx.get_literal(e);
+            if (is_not)
+                lit.neg();
+            if (ctx.get_assignment(lit) == l_false) {
+                // TRACE(seq, tout << "literal_if_false: " << lit << " " << mk_pp(e, m) << " is assigned false\n");
+                return lit;
+            }
+            // TRACE(seq, tout << "literal_if_false: " << mk_pp(e, m) << " is assigned " << ctx.get_assignment(lit) <<
+            // "\n");
+            return sat::null_literal;
+        }
+    };
+
 }
diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index 4c4430570..183dd7dc9 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -284,7 +284,7 @@ namespace seq {
         enode_pair_vector eqs;
         if (m_graph.a.is_numeral(e, lo))
             return true;
-        if (!m_graph.m_solver.lower_bound(e, lo, lits, eqs)) 
+        if (!m_graph.m_context_solver.lower_bound(e, lo, lits, eqs)) 
             return false;
         for (auto lit : lits)
             dep = m_graph.dep_mgr().mk_join(dep, m_graph.dep_mgr().mk_leaf(lit));
@@ -301,7 +301,7 @@ namespace seq {
         enode_pair_vector eqs;
         if (m_graph.a.is_numeral(e, up))
             return true;
-        if (!m_graph.m_solver.upper_bound(e, up, lits, eqs)) 
+        if (!m_graph.m_context_solver.upper_bound(e, up, lits, eqs)) 
             return false;
         for (auto lit : lits)
             dep = m_graph.dep_mgr().mk_join(dep, m_graph.dep_mgr().mk_leaf(lit));
@@ -432,12 +432,13 @@ namespace seq {
     // nielsen_graph
     // -----------------------------------------------
 
-    nielsen_graph::nielsen_graph(euf::sgraph &sg, simple_solver &solver):
+    nielsen_graph::nielsen_graph(euf::sgraph &sg, sub_solver_i &solver, context_solver_i& ctx_solver):
         m(sg.get_manager()),
         a(sg.get_manager()),
         m_seq(sg.get_seq_util()),
         m_sg(sg),
-        m_solver(solver),
+        m_length_solver(solver),
+        m_context_solver(ctx_solver),
         m_parikh(alloc(seq_parikh, sg)),
         m_seq_regex(alloc(seq::seq_regex, sg)) {}
 
@@ -550,7 +551,7 @@ namespace seq {
         m_length_trail.reset();
         m_length_info.reset();
         m_dep_mgr.reset();
-        m_solver.reset();
+        m_length_solver.reset();
         SASSERT(m_nodes.empty());
         SASSERT(m_edges.empty());
         SASSERT(m_root == nullptr);
@@ -1891,7 +1892,7 @@ namespace seq {
             // constraints.  The child's own new constraints will be asserted
             // inside the recursive call (above).  On return, pop the scope so
             // that backtracking removes those assertions.
-            m_solver.push();
+            m_length_solver.push();
 
             // Lazily compute substitution length constraints (|x| = |u|) on first
             // traversal. This must happen before asserting side_constraints and before
@@ -1916,7 +1917,7 @@ namespace seq {
             // Restore modification counts on backtrack.
             dec_edge_mod_counts(e);
 
-            m_solver.pop(1);
+            m_length_solver.pop(1);
             if (r == search_result::sat)
                 return search_result::sat;
             cur_path.pop_back();
@@ -4501,11 +4502,11 @@ namespace seq {
     }
 
     void nielsen_graph::assert_to_subsolver(const constraint& c) {
-        m_solver.assert_expr(c.fml, c.dep);
+        m_length_solver.assert_expr(c.fml, c.dep);
     }
 
     void nielsen_graph::assert_to_subsolver(expr* e) {
-        m_solver.assert_expr(e);
+        m_length_solver.assert_expr(e);
     }
 
     void nielsen_graph::assert_node_new_int_constraints(nielsen_node* node) {
@@ -4514,10 +4515,9 @@ namespace seq {
         // already present in the enclosing solver scope; asserting them again would
         // be redundant (though harmless).  This is called by search_dfs right after
         // simplify_and_init, which is where new constraints are produced.
-        SASSERT(m_literal_if_false);
         for (unsigned i = node->m_parent_ic_count; i < node->constraints().size(); ++i) {
             auto& c = node->constraints()[i];
-            auto lit = m_literal_if_false(c.fml);
+            auto lit = m_context_solver.literal_if_false(c.fml);
             // std::cout << "Internalizing literal " << mk_pp(c.fml, m) << " [" << (lit == sat::null_literal) << "]" <<
             // std::endl;
             if (lit != sat::null_literal) {
@@ -4584,13 +4584,13 @@ namespace seq {
         // (root length constraints at the base level, edge side_constraints and node
         // constraints pushed/popped as the DFS descends and backtracks).
         // A plain check() is therefore sufficient.
-        return m_solver.check() != l_false;
+        return m_length_solver.check() != l_false;
     }
 
     dep_tracker nielsen_graph::get_subsolver_dependency(nielsen_node* /*n*/) {
         // check_int_feasibility() already called m_solver.check() which computed
         // the UNSAT core in terms of tracked assumption literals and their deps.
-        return m_solver.core();
+        return m_length_solver.core();
     }
 
     bool nielsen_graph::check_lp_le(expr* lhs, expr* rhs, nielsen_node* n, dep_tracker& dep) {
@@ -4599,8 +4599,8 @@ namespace seq {
         rational lhs_lo, rhs_up;
         literal_vector lits;
         enode_pair_vector eqs;
-        if (m_solver.lower_bound(lhs, lhs_lo, lits, eqs) && 
-            m_solver.upper_bound(rhs, rhs_up, lits, eqs) && lhs_lo > rhs_up)
+        if (m_context_solver.lower_bound(lhs, lhs_lo, lits, eqs) && 
+            m_context_solver.upper_bound(rhs, rhs_up, lits, eqs) && lhs_lo > rhs_up)
             return false;
 
         // lhs <= lhs_up <= rhs_lo <= rhs
@@ -4609,8 +4609,8 @@ namespace seq {
         lits.reset();
         eqs.reset();
         rational rhs_lo, lhs_up;
-        if (m_solver.upper_bound(lhs, lhs_up, lits, eqs) && 
-            m_solver.lower_bound(rhs, rhs_lo, lits, eqs) &&
+        if (m_context_solver.upper_bound(lhs, lhs_up, lits, eqs) && 
+            m_context_solver.lower_bound(rhs, rhs_lo, lits, eqs) &&
             lhs_up <= rhs_lo) {
             for (auto lit : lits)
                 dep = m_dep_mgr.mk_join(dep, m_dep_mgr.mk_leaf(lit));
@@ -4629,12 +4629,12 @@ namespace seq {
         expr_ref one(a.mk_int(1), m);
         expr_ref rhs_plus_one(a.mk_add(rhs, one), m);
 
-        m_solver.push();
+        m_length_solver.push();
         assert_to_subsolver(a.mk_ge(lhs, rhs_plus_one));
-        lbool result = m_solver.check();
+        lbool result = m_length_solver.check();
         if (result == l_false)
-            dep = m_solver.core();
-        m_solver.pop(1);
+            dep = m_length_solver.core();
+        m_length_solver.pop(1);
         if (result == l_false) {
             n->add_constraint(constraint(a.mk_le(lhs, rhs), dep, m));
             return true;
diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h
index e48fe9c79..940448565 100644
--- a/src/smt/seq/seq_nielsen.h
+++ b/src/smt/seq/seq_nielsen.h
@@ -316,7 +316,6 @@ namespace seq {
     using enode_pair = std::pair<smt::enode *, smt::enode *>;
     using literal_vector = svector<sat::literal>;
     using enode_pair_vector = svector<enode_pair>;
-
     using dep_source = std::variant<sat::literal, enode_pair>;
 
 
@@ -338,21 +337,39 @@ namespace seq {
      * to serve as the arithmetic back-end.  When no solver is provided,
      * integer feasibility checks are skipped (optimistically assumed feasible).
      */
-    class simple_solver {
+    class sub_solver_i {
     public:
-        virtual ~simple_solver() {}
+        virtual ~sub_solver_i() {}
         virtual lbool       check() = 0;
         virtual void        assert_expr(expr* e, dep_tracker dep = nullptr) = 0;
         virtual void        push() = 0;
         virtual void        pop(unsigned num_scopes) = 0;
         virtual void        get_model(model_ref& mdl) { mdl = nullptr; }
         virtual dep_tracker core() { return nullptr; }
+        virtual void        reset() = 0;
+    };
+
+    class context_solver_i {
+    public:
+        virtual ~context_solver_i() {}
+
+        bool m_should_internalize = false;
+
         // Optional bound queries on arithmetic expressions (non-strict integer bounds).
         // Default implementation reports "unsupported".
-        virtual bool        lower_bound(expr* e, rational& l, literal_vector& lits, enode_pair_vector& eqs) const { return false; }
-        virtual bool        upper_bound(expr* e, rational& hi, literal_vector& lits, enode_pair_vector& eqs) const { return false; }
-        virtual bool        current_value(expr* e, rational& v) const { return false; }
-        virtual void        reset() = 0;
+        virtual bool lower_bound(expr *e, rational &l, literal_vector &lits, enode_pair_vector &eqs) const {
+            return false;
+        }
+        virtual bool upper_bound(expr *e, rational &hi, literal_vector &lits, enode_pair_vector &eqs) const {
+            return false;
+        }
+        virtual bool current_value(expr *e, rational &v) const {
+            return false;
+        }
+        virtual sat::literal literal_if_false(expr* e) {
+            return sat::null_literal;
+        }
+
     };
 
     // partition dep_source leaves from deps into enode pairs, sat literals,
@@ -840,10 +857,13 @@ namespace seq {
 
         // -----------------------------------------------
         // Integer subsolver (abstract interface)
-        // When m_solver is null, check_int_feasibility skips arithmetic checking
-        // and optimistically assumes feasibility.
         // -----------------------------------------------
-        simple_solver&                m_solver;
+        sub_solver_i& m_length_solver;
+
+        // -----------------------------------------------
+        // Interface to solver context
+        // -----------------------------------------------
+        context_solver_i &m_context_solver;
 
         // Constraint.Shared: guards re-assertion of root-level constraints.
         // Set to true after assert_root_constraints_to_solver() is first called.
@@ -857,9 +877,6 @@ namespace seq {
         // inclusion, derivatives. Allocated in the constructor; owned by this graph.
         seq::seq_regex*              m_seq_regex = nullptr;
 
-        // Callback to check that literals assumed in branches are not already assigned to false.
-        // returns the literal that is assigned to false, otherwise returns a null_literal
-        std::function<sat::literal(expr *)> m_literal_if_false;
 
         // Maps each variable to its current length term
 
@@ -886,12 +903,9 @@ namespace seq {
     public:
         // Construct with a caller-supplied solver.  Ownership is NOT transferred;
         // the caller is responsible for keeping the solver alive.
-        nielsen_graph(euf::sgraph& sg, simple_solver& solver);
+        nielsen_graph(euf::sgraph& sg, sub_solver_i& solver, context_solver_i& ctx);
         ~nielsen_graph();
 
-        void set_literal_if_false(std::function<sat::literal(expr* e)> const& lif) {
-            m_literal_if_false = lif;
-        }
 
         ast_manager &get_manager() {
             return m;
diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp
index 9c395fbdc..d7d81a119 100644
--- a/src/smt/theory_nseq.cpp
+++ b/src/smt/theory_nseq.cpp
@@ -33,8 +33,9 @@ namespace smt {
         m_arith_value(m),
         m_egraph(m),
         m_sgraph(m, m_egraph),
-        m_context_solver(m),
-        m_nielsen(m_sgraph, m_context_solver),
+        m_length_solver(m),
+        m_context_solver(ctx),
+        m_nielsen(m_sgraph, m_length_solver, m_context_solver),
         m_axioms(m_th_rewriter),
         m_regex(m_sgraph),
         m_model(m, ctx, m_seq, m_rewriter, m_sgraph),
@@ -82,34 +83,8 @@ namespace smt {
         m_axioms.set_ensure_digits(ensure_digit_axiom);
         m_axioms.set_mark_no_diseq(mark_no_diseq);
 
-        m_should_internalize = true; // delete this if using internalize as fallback
-        std::function<sat::literal(expr*)> literal_if_false = [&](expr* e) {
-            bool is_not = m.is_not(e, e);
-            if (m_should_internalize && !ctx.b_internalized(e)) {
-                // it can happen that the element is not internalized, but as soon as we do it, it becomes false.
-                // In case we just skip one of those uninternalized expressions,
-                // adding the Nielsen assumption later will fail
-                // Alternatively, we could just retry Nielsen saturation in case
-                // adding the Nielsen assumption yields the assumption being false after internalizing
-                ctx.internalize(to_app(e), false);
-            }
-
-            if (!ctx.b_internalized(e))
-                return sat::null_literal;
-
-            literal lit = ctx.get_literal(e);
-            if (is_not)
-                lit.neg();
-            if (ctx.get_assignment(lit) == l_false) {
-                // TRACE(seq, tout << "literal_if_false: " << lit << " " << mk_pp(e, m) << " is assigned false\n");
-                return lit;
-            }
-            // TRACE(seq, tout << "literal_if_false: " << mk_pp(e, m) << " is assigned " << ctx.get_assignment(lit) << "\n");
-            return sat::null_literal;
-        };
-
-        
-        m_nielsen.set_literal_if_false(literal_if_false);
+        m_context_solver.m_should_internalize = true; // delete this if using internalize as fallback
+       
     }
 
     // -----------------------------------------------------------------------
@@ -848,12 +823,11 @@ namespace smt {
                 break;
             case l_false: 
                 // this should not happen because nielsen checks for this before returning a satisfying path.
-                // or maybe it can happen if we have a "le" dependency
                 TRACE(seq, tout << "nseq final_check: nielsen assumption " << c.fml << " is false; internalized - " << ctx.e_internalized(c.fml) << "\n");
                 all_sat = false;
                 // std::cout << "False [" << lit << "]: " << mk_pp(c.fml, m) << std::endl;
-                ctx.push_trail(value_trail(m_should_internalize));
-                m_should_internalize = true;
+                ctx.push_trail(value_trail(m_context_solver.m_should_internalize));
+                m_context_solver.m_should_internalize = true;
                 break;
             }    
             // use assumptions to bound search
diff --git a/src/smt/theory_nseq.h b/src/smt/theory_nseq.h
index 7995686c8..9e90e3473 100644
--- a/src/smt/theory_nseq.h
+++ b/src/smt/theory_nseq.h
@@ -44,12 +44,12 @@ namespace smt {
         euf::sgraph    m_sgraph;  // private sgraph
         // m_context_solver must be declared before m_nielsen: its address is passed
         // to the m_nielsen constructor and must remain stable for the object's lifetime.
+        sub_solver m_length_solver;
         context_solver m_context_solver;
         seq::nielsen_graph m_nielsen;
         seq::axioms m_axioms;
         seq::seq_regex     m_regex;   // regex membership pre-processing
         seq_model     m_model;   // model construction helper
-        bool m_should_internalize = false;
 
         // propagation queue items (variant over the distinct propagation cases)
         using eq_item   = tracked_str_eq;    // string equality
diff --git a/src/test/nseq_basic.cpp b/src/test/nseq_basic.cpp
index 760e35fb4..ee3d8167c 100644
--- a/src/test/nseq_basic.cpp
+++ b/src/test/nseq_basic.cpp
@@ -22,7 +22,7 @@ Abstract:
 #include <iostream>
 
 // Trivial solver that always returns sat and ignores all assertions.
-class nseq_basic_dummy_solver : public seq::simple_solver {
+class nseq_basic_dummy_solver : public seq::sub_solver_i {
 public:
     void push() override {}
     void pop(unsigned) override {}
@@ -40,7 +40,8 @@ static void test_nseq_instantiation() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
     nseq_basic_dummy_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     SASSERT(ng.root() == nullptr);
     SASSERT(ng.num_nodes() == 0);
     std::cout << "  ok\n";
@@ -97,7 +98,8 @@ static void test_nseq_simplification() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
     nseq_basic_dummy_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     // Add a trivial equality: empty = empty
     euf::snode* empty1 = sg.mk_empty_seq(su.str.mk_string_sort());
@@ -120,7 +122,8 @@ static void test_nseq_node_satisfied() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
     nseq_basic_dummy_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     seq::nielsen_node *node = ng.mk_node();
     // empty node has no constraints => satisfied
@@ -149,7 +152,8 @@ static void test_nseq_symbol_clash() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
     nseq_basic_dummy_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* a = sg.mk_char('a');
     euf::snode* b = sg.mk_char('b');
@@ -176,7 +180,8 @@ static void test_nseq_var_eq_self() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
     nseq_basic_dummy_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     ng.add_str_eq(x, x);
@@ -194,7 +199,8 @@ static void test_nseq_prefix_clash() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
     nseq_basic_dummy_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* a = sg.mk_char('a');
@@ -216,7 +222,8 @@ static void test_nseq_const_nielsen_solvable() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
     nseq_basic_dummy_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
@@ -239,8 +246,8 @@ static void test_nseq_length_mismatch() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
     nseq_basic_dummy_solver solver;
-    seq::nielsen_graph ng(sg, solver);
-
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     euf::snode* a = sg.mk_char('a');
     euf::snode* b = sg.mk_char('b');
     euf::snode* ab = sg.mk_concat(a, b);
diff --git a/src/test/nseq_zipt.cpp b/src/test/nseq_zipt.cpp
index 01a04b80b..c802122ca 100644
--- a/src/test/nseq_zipt.cpp
+++ b/src/test/nseq_zipt.cpp
@@ -30,7 +30,7 @@ Abstract:
 #include <chrono>
 
 // Trivial solver that always returns sat and ignores all assertions.
-class nseq_zipt_dummy_solver : public seq::simple_solver {
+class nseq_zipt_dummy_solver : public seq::sub_solver_i {
 public:
     void push() override {}
     void pop(unsigned) override {}
@@ -43,7 +43,7 @@ public:
 // Trivial simple_solver stub: optimistically assumes integer constraints
 // are always feasible (returns l_true without actually checking).
 // -----------------------------------------------------------------------
-class zipt_dummy_simple_solver : public seq::simple_solver {
+class zipt_dummy_simple_solver : public seq::sub_solver_i {
 public:
     void push() override {}
     void pop(unsigned) override {}
@@ -184,6 +184,7 @@ struct nseq_fixture {
     euf::egraph eg;
     euf::sgraph sg;
     zipt_dummy_simple_solver dummy_solver;
+    seq::context_solver_i context_solver;
     seq::nielsen_graph ng;
     seq_util su;
     str_builder sb;
@@ -193,7 +194,7 @@ struct nseq_fixture {
     static ast_manager& init(ast_manager& m) { reg_decl_plugins(m); return m; }
 
     nseq_fixture()
-        : eg(init(m)), sg(m, eg), ng(sg, dummy_solver), su(m), sb(sg, su), rb(m, su, sg)
+        : eg(init(m)), sg(m, eg), dummy_solver(), context_solver(), ng(sg, dummy_solver, context_solver), su(m), sb(sg, su), rb(m, su, sg)
     {}
 
     euf::snode* S(const char* s) { return sb.parse(s); }
diff --git a/src/test/seq_nielsen.cpp b/src/test/seq_nielsen.cpp
index 7a676ef36..b8a489673 100644
--- a/src/test/seq_nielsen.cpp
+++ b/src/test/seq_nielsen.cpp
@@ -22,9 +22,9 @@ Abstract:
 #include "ast/ast_pp.h"
 #include <iostream>
 
-class dummy_simple_solver : public seq::simple_solver {
+class dummy_simple_solver : public seq::sub_solver_i {
 public:
-    dummy_simple_solver() : seq::simple_solver() {}
+    dummy_simple_solver() : seq::sub_solver_i() {}
     void push() override {}
     void pop(unsigned n) override {}
     void assert_expr(expr *e, seq::dep_tracker dep) override {}
@@ -184,7 +184,8 @@ static void test_nielsen_node() {
     sort_ref str_sort(seq.str.mk_string_sort(), m);
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
@@ -227,7 +228,8 @@ static void test_nielsen_edge() {
     euf::sgraph sg(m, eg);
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
@@ -263,7 +265,8 @@ static void test_nielsen_graph_populate() {
     sort_ref str_sort(seq.str.mk_string_sort(), m);
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
@@ -302,7 +305,8 @@ static void test_nielsen_subst_apply() {
     sort_ref str_sort(seq.str.mk_string_sort(), m);
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
@@ -337,7 +341,8 @@ static void test_nielsen_graph_reset() {
     euf::sgraph sg(m, eg);
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
@@ -362,7 +367,8 @@ static void test_nielsen_expansion() {
     seq_util seq(m);
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
@@ -412,7 +418,8 @@ static void test_run_idx() {
     euf::sgraph sg(m, eg);
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     SASSERT(ng.run_idx() == 0);
 
     ng.inc_run_idx();
@@ -433,7 +440,8 @@ static void test_multiple_memberships() {
     sort_ref str_sort(seq.str.mk_string_sort(), m);
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
 
@@ -468,7 +476,8 @@ static void test_backedge() {
     euf::sgraph sg(m, eg);
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
@@ -492,7 +501,8 @@ static void test_eq_split_basic() {
     euf::sgraph sg(m, eg);
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
@@ -523,7 +533,8 @@ static void test_eq_split_solve_sat() {
     euf::sgraph sg(m, eg);
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
@@ -545,8 +556,9 @@ static void test_eq_split_solve_unsat() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    dummy_simple_solver solver;    
-    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver; 
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
@@ -569,7 +581,8 @@ static void test_eq_split_same_var_det() {
     euf::sgraph sg(m, eg);
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* a = sg.mk_char('A');
@@ -591,8 +604,9 @@ static void test_eq_split_commutation_sat() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    dummy_simple_solver solver;    
-    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
@@ -615,7 +629,8 @@ static void test_const_nielsen_char_var() {
     euf::sgraph sg(m, eg);
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* a = sg.mk_char('A');
     euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
@@ -639,7 +654,8 @@ static void test_const_nielsen_var_char() {
     euf::sgraph sg(m, eg);
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* b = sg.mk_char('B');
@@ -665,7 +681,8 @@ static void test_const_nielsen_solve_sat() {
     euf::sgraph sg(m, eg);
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* a = sg.mk_char('A');
     euf::snode* b = sg.mk_char('B');
@@ -687,7 +704,8 @@ static void test_const_nielsen_solve_unsat() {
     euf::sgraph sg(m, eg);
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* a = sg.mk_char('A');
     euf::snode* b = sg.mk_char('B');
@@ -710,7 +728,8 @@ static void test_const_nielsen_priority_over_eq_split() {
     euf::sgraph sg(m, eg);
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* a = sg.mk_char('A');
     euf::snode* b = sg.mk_char('B');
@@ -740,7 +759,8 @@ static void test_const_nielsen_tail_char_var() {
     euf::sgraph sg(m, eg);
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* w = sg.mk_var(symbol("w"), sg.get_str_sort());
@@ -788,7 +808,8 @@ static void test_const_nielsen_not_applicable_both_vars() {
     euf::sgraph sg(m, eg);
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
@@ -815,8 +836,8 @@ static void test_const_nielsen_multi_char_solve() {
     euf::sgraph sg(m, eg);
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
-
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     euf::snode* a = sg.mk_char('A');
     euf::snode* b = sg.mk_char('B');
     euf::snode* c = sg.mk_char('C');
@@ -844,7 +865,8 @@ static void test_regex_char_split_basic() {
     sort_ref str_sort(seq.str.mk_string_sort(), m);
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
 
@@ -880,8 +902,8 @@ static void test_regex_char_split_solve_sat() {
     sort_ref str_sort(seq.str.mk_string_sort(), m);
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
-
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
 
     expr_ref ch_a(seq.str.mk_char('A'), m);
@@ -905,8 +927,8 @@ static void test_regex_char_split_solve_multi_char() {
     sort_ref str_sort(seq.str.mk_string_sort(), m);
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
-
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
 
     expr_ref ch_a(seq.str.mk_char('A'), m);
@@ -933,8 +955,8 @@ static void test_regex_char_split_union() {
     sort_ref str_sort(seq.str.mk_string_sort(), m);
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
-
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
 
     expr_ref ch_a(seq.str.mk_char('A'), m);
@@ -962,8 +984,8 @@ static void test_regex_char_split_star_sat() {
     sort_ref str_sort(seq.str.mk_string_sort(), m);
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
-
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
 
     expr_ref ch_a(seq.str.mk_char('A'), m);
@@ -988,8 +1010,8 @@ static void test_regex_char_split_concat_str() {
     sort_ref str_sort(seq.str.mk_string_sort(), m);
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
-
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
     euf::snode* xy = sg.mk_concat(x, y);
@@ -1018,7 +1040,8 @@ static void test_regex_char_split_with_eq() {
     sort_ref str_sort(seq.str.mk_string_sort(), m);
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
@@ -1046,7 +1069,8 @@ static void test_regex_char_split_ground_skip() {
     sort_ref str_sort(seq.str.mk_string_sort(), m);
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* a = sg.mk_char('A');
 
@@ -1075,7 +1099,8 @@ static void test_var_nielsen_basic() {
     euf::sgraph sg(m, eg);
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
@@ -1099,7 +1124,8 @@ static void test_var_nielsen_same_var_det() {
     euf::sgraph sg(m, eg);
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* a = sg.mk_char('A');
@@ -1122,7 +1148,8 @@ static void test_var_nielsen_not_applicable_char() {
     euf::sgraph sg(m, eg);
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* a = sg.mk_char('A');
     euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
@@ -1145,7 +1172,8 @@ static void test_var_nielsen_solve_sat() {
     euf::sgraph sg(m, eg);
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
@@ -1168,7 +1196,8 @@ static void test_var_nielsen_solve_unsat() {
     euf::sgraph sg(m, eg);
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
@@ -1191,8 +1220,8 @@ static void test_var_nielsen_commutation_sat() {
     euf::sgraph sg(m, eg);
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
-
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
     euf::snode* a = sg.mk_char('A');
@@ -1213,8 +1242,9 @@ static void test_var_nielsen_priority() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
-
+    dummy_simple_solver solver;    
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
 
@@ -1238,7 +1268,9 @@ static void test_generate_extensions_det_priority() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;   
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);  
 
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
@@ -1262,7 +1294,10 @@ static void test_generate_extensions_no_applicable() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;    
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
+    
 
     euf::snode* a = sg.mk_char('A');
     euf::snode* b = sg.mk_char('B');
@@ -1286,8 +1321,9 @@ static void test_generate_extensions_regex_only() {
     euf::sgraph sg(m, eg);
     seq_util seq(m);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
-
+    dummy_simple_solver solver;    
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     // Build regex to_re("A")
     expr_ref ch_a(seq.str.mk_char('A'), m);
@@ -1316,7 +1352,9 @@ static void test_generate_extensions_mixed_det_first() {
     euf::sgraph sg(m, eg);
     seq_util seq(m);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;    
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
@@ -1350,7 +1388,9 @@ static void test_solve_empty_graph() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;    
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     SASSERT(!ng.root());
     auto result = ng.solve();
     SASSERT(result == seq::nielsen_graph::search_result::sat);
@@ -1364,7 +1404,9 @@ static void test_solve_trivially_satisfied() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;    
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     ng.add_str_eq(x, x);
     auto result = ng.solve();
@@ -1379,7 +1421,9 @@ static void test_solve_node_status_unsat() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;   
+        seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     euf::snode* a = sg.mk_char('A');
     euf::snode* b = sg.mk_char('B');
     // A = B is an immediate conflict
@@ -1401,7 +1445,9 @@ static void test_solve_conflict_deps() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     euf::snode* a = sg.mk_char('A');
     euf::snode* b = sg.mk_char('B');
     // Add two constraints: A = B (unsat) and a dummy x = x
@@ -1481,7 +1527,9 @@ static void test_explain_conflict_single_eq() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;    
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     euf::snode* a = sg.mk_char('A');
     euf::snode* b = sg.mk_char('B');
     // eq[0]: A = B (conflict)
@@ -1507,7 +1555,9 @@ static void test_explain_conflict_multi_eq() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     euf::snode* a = sg.mk_char('A');
     euf::snode* b = sg.mk_char('B');
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
@@ -1535,7 +1585,9 @@ static void test_solve_node_extended_flag() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;    
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
     euf::snode* xy = sg.mk_concat(x, y);
@@ -1562,7 +1614,9 @@ static void test_solve_mixed_eq_mem_sat() {
     euf::sgraph sg(m, eg);
     seq_util seq(m);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;    
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
     euf::snode* a = sg.mk_char('A');
@@ -1591,7 +1645,9 @@ static void test_solve_children_failed_reason() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;    
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
     euf::snode* a = sg.mk_char('A');
@@ -1613,7 +1669,9 @@ static void test_solve_eval_idx_tracking() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;    
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* a = sg.mk_char('A');
     // x = A·x would be infinite without depth bound, but
@@ -1646,7 +1704,8 @@ static void test_simplify_prefix_cancel() {
     euf::sgraph sg(m, eg);
 
     dummy_simple_solver solver;   
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     euf::snode* a = sg.mk_char('A');
     euf::snode* b = sg.mk_char('B');
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
@@ -1677,7 +1736,8 @@ static void test_simplify_suffix_cancel_rtl() {
     euf::sgraph sg(m, eg);
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     euf::snode* a = sg.mk_char('A');
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
@@ -1705,7 +1765,9 @@ static void test_simplify_symbol_clash() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;    
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     euf::snode* a = sg.mk_char('A');
     euf::snode* b = sg.mk_char('B');
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
@@ -1734,7 +1796,9 @@ static void test_simplify_empty_propagation() {
     euf::sgraph sg(m, eg);
     seq_util seq(m);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;    
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     euf::snode* e = sg.mk_empty_seq(seq.str.mk_string_sort());
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
@@ -1758,7 +1822,9 @@ static void test_simplify_empty_vs_char() {
     euf::sgraph sg(m, eg);
     seq_util seq(m);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;    
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     euf::snode* e = sg.mk_empty_seq(seq.str.mk_string_sort());
     euf::snode* a = sg.mk_char('A');
 
@@ -1780,7 +1846,9 @@ static void test_simplify_multi_pass_clash() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;    
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     euf::snode* a = sg.mk_char('A');
     euf::snode* b = sg.mk_char('B');
     euf::snode* c = sg.mk_char('C');
@@ -1807,7 +1875,9 @@ static void test_simplify_trivial_removal() {
     euf::sgraph sg(m, eg);
     seq_util seq(m);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;    
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
     euf::snode* e = sg.mk_empty_seq(seq.str.mk_string_sort());
@@ -1831,7 +1901,9 @@ static void test_simplify_all_trivial_satisfied() {
     euf::sgraph sg(m, eg);
     seq_util seq(m);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;    
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* e = sg.mk_empty_seq(seq.str.mk_string_sort());
 
@@ -1853,7 +1925,9 @@ static void test_simplify_regex_infeasible() {
     euf::sgraph sg(m, eg);
     seq_util seq(m);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;    
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     euf::snode* e = sg.mk_empty_seq(seq.str.mk_string_sort());
 
     expr_ref ch_a(seq.str.mk_char('A'), m);
@@ -1880,7 +1954,9 @@ static void test_simplify_nullable_removal() {
     euf::sgraph sg(m, eg);
     seq_util seq(m);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;    
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     euf::snode* e = sg.mk_empty_seq(seq.str.mk_string_sort());
 
     expr_ref ch_a(seq.str.mk_char('A'), m);
@@ -1908,7 +1984,9 @@ static void test_simplify_brzozowski_sat() {
     euf::sgraph sg(m, eg);
     seq_util seq(m);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;    
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     euf::snode* a = sg.mk_char('A');
     euf::snode* e = sg.mk_empty_seq(seq.str.mk_string_sort());
 
@@ -1936,7 +2014,8 @@ static void test_simplify_brzozowski_rtl_suffix() {
     seq_util seq(m);
 
     dummy_simple_solver solver;    
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* a = sg.mk_char('A');
     euf::snode* xa = sg.mk_concat(x, a);
@@ -1974,7 +2053,9 @@ static void test_simplify_multiple_eqs() {
     euf::sgraph sg(m, eg);
     seq_util seq(m);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;    
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     euf::snode* a = sg.mk_char('A');
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
@@ -2012,7 +2093,9 @@ static void test_det_cancel_child_eq() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* a = sg.mk_char('A');
     euf::snode* b = sg.mk_char('B');
@@ -2034,7 +2117,9 @@ static void test_const_nielsen_child_substitutions() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     euf::snode* a = sg.mk_char('A');
     euf::snode* b = sg.mk_char('B');
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
@@ -2070,7 +2155,9 @@ static void test_var_nielsen_substitution_types() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;    
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
 
@@ -2100,7 +2187,9 @@ static void test_explain_conflict_mem_only() {
     euf::sgraph sg(m, eg);
     seq_util seq(m);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     euf::snode* e = sg.mk_empty_seq(seq.str.mk_string_sort());
 
     expr_ref ch_a(seq.str.mk_char('A'), m);
@@ -2128,7 +2217,9 @@ static void test_explain_conflict_mixed_eq_mem() {
     euf::sgraph sg(m, eg);
     seq_util seq(m);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;    
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     euf::snode* a = sg.mk_char('A');
     euf::snode* b = sg.mk_char('B');
     euf::snode* e = sg.mk_empty_seq(seq.str.mk_string_sort());
@@ -2162,7 +2253,9 @@ static void test_subsumption_pruning_unsat() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;    
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     euf::snode* a = sg.mk_char('A');
     euf::snode* b = sg.mk_char('B');
 
@@ -2184,7 +2277,9 @@ static void test_subsumption_reason_set() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;    
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
     euf::snode* a = sg.mk_char('A');
@@ -2234,7 +2329,9 @@ static void test_length_constraints_basic() {
     euf::snode* lhs = sg.mk_concat(x, y);
     euf::snode* rhs = sg.mk_concat(a, b);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;    
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     ng.add_str_eq(lhs, rhs);
 
     vector<seq::length_constraint> constraints;
@@ -2269,7 +2366,9 @@ static void test_length_constraints_trivial_skip() {
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
 
     // trivial equation: x = x (same snode)
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     ng.add_str_eq(x, x);
 
     vector<seq::length_constraint> constraints;
@@ -2288,8 +2387,9 @@ static void test_length_constraints_empty() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
-
+    dummy_simple_solver solver;    
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     vector<seq::length_constraint> constraints;
     ng.generate_length_constraints(constraints);
 
@@ -2317,7 +2417,9 @@ static void test_length_constraints_concat_chain() {
     euf::snode* lhs = sg.mk_concat(sg.mk_concat(x, y), z);
     euf::snode* rhs = sg.mk_concat(sg.mk_concat(a, b), c);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;    
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     ng.add_str_eq(lhs, rhs);
 
     vector<seq::length_constraint> constraints;
@@ -2345,7 +2447,9 @@ static void test_length_constraints_multi_eq() {
     euf::snode* a = sg.mk_char('A');
     euf::snode* b = sg.mk_char('B');
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     ng.add_str_eq(x, a);           // x = A
     ng.add_str_eq(y, b);           // y = B
 
@@ -2378,7 +2482,9 @@ static void test_length_constraints_shared_var() {
     euf::snode* lhs = sg.mk_concat(x, a);
     euf::snode* rhs = sg.mk_concat(a, x);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;    
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     ng.add_str_eq(lhs, rhs);
 
     vector<seq::length_constraint> constraints;
@@ -2403,7 +2509,9 @@ static void test_length_constraints_deps() {
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* a = sg.mk_char('A');
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;    
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     ng.add_str_eq(x, a);  // eq index 0
 
     vector<seq::length_constraint> constraints;
@@ -2429,7 +2537,9 @@ static void test_length_constraints_empty_side() {
     euf::snode* e = sg.mk_empty_seq(seq.str.mk_string_sort());
 
     // x = ε
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     ng.add_str_eq(x, e);
 
     vector<seq::length_constraint> constraints;
@@ -2463,7 +2573,9 @@ static void test_length_kind_tagging() {
     euf::snode* a = sg.mk_char('A');
 
     // equation: x = a (one eq + one nonneg)
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     ng.add_str_eq(x, a);
 
     // membership: y in to_re("AB") (bounds + nonneg)
@@ -2517,7 +2629,9 @@ static void test_power_epsilon_no_power() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* a = sg.mk_char('A');
@@ -2541,7 +2655,9 @@ static void test_num_cmp_no_power() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
@@ -2566,7 +2682,9 @@ static void test_star_intr_no_backedge() {
     seq_util seq(m);
     sort_ref str_sort(seq.str.mk_string_sort(), m);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     expr_ref ch_a(seq.str.mk_char('A'), m);
@@ -2599,7 +2717,9 @@ static void test_star_intr_with_backedge() {
     seq_util seq(m);
     sort_ref str_sort(seq.str.mk_string_sort(), m);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     expr_ref ch_a(seq.str.mk_char('A'), m);
@@ -2638,7 +2758,9 @@ static void test_gpower_intr_self_cycle() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* a1 = sg.mk_char('A');
@@ -2666,7 +2788,9 @@ static void test_gpower_intr_no_cycle() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
@@ -2696,7 +2820,9 @@ static void test_regex_var_split_basic() {
     seq_util seq(m);
     sort_ref str_sort(seq.str.mk_string_sort(), m);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
 
@@ -2731,7 +2857,9 @@ static void test_power_split_no_power() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
@@ -2757,7 +2885,9 @@ static void test_var_num_unwinding_no_power() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
@@ -2780,8 +2910,9 @@ static void test_const_num_unwinding_no_power() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
-
+    dummy_simple_solver solver;
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     euf::snode* a = sg.mk_char('A');
     euf::snode* b = sg.mk_char('B');
 
@@ -2807,7 +2938,9 @@ static void test_priority_chain_order() {
     {
         euf::egraph eg(m);
         euf::sgraph sg(m, eg);
-        dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+        dummy_simple_solver solver;
+        seq::context_solver_i context_solver;
+        seq::nielsen_graph ng(sg, solver, context_solver);
 
         euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
         euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
@@ -2824,7 +2957,9 @@ static void test_priority_chain_order() {
     {
         euf::egraph eg(m);
         euf::sgraph sg(m, eg);
-        dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+        dummy_simple_solver solver;
+        seq::context_solver_i context_solver;
+        seq::nielsen_graph ng(sg, solver, context_solver);
 
         euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
         euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
@@ -2840,7 +2975,9 @@ static void test_priority_chain_order() {
     {
         euf::egraph eg(m);
         euf::sgraph sg(m, eg);
-        dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+        dummy_simple_solver solver;
+        seq::context_solver_i context_solver;
+        seq::nielsen_graph ng(sg, solver, context_solver);
 
         euf::snode* a = sg.mk_char('A');
         euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
@@ -2861,7 +2998,9 @@ static void test_gpower_intr_solve_sat() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* a1 = sg.mk_char('A');
@@ -2899,7 +3038,9 @@ static void test_parikh_exact_length() {
     expr_ref to_re_ab(seq.re.mk_to_re(ab), m);
     euf::snode* regex = sg.mk(to_re_ab);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     ng.add_str_mem(x, regex);
 
     vector<seq::length_constraint> constraints;
@@ -2946,7 +3087,9 @@ static void test_parikh_star_unbounded() {
     expr_ref re_star(seq.re.mk_star(to_re_a), m);
     euf::snode* regex = sg.mk(re_star);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     ng.add_str_mem(x, regex);
 
     vector<seq::length_constraint> constraints;
@@ -3001,7 +3144,9 @@ static void test_parikh_union_interval() {
     expr_ref re_union(seq.re.mk_union(to_re_ab, to_re_cde), m);
     euf::snode* regex = sg.mk(re_union);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     ng.add_str_mem(x, regex);
 
     vector<seq::length_constraint> constraints;
@@ -3040,7 +3185,9 @@ static void test_parikh_loop_bounded() {
     expr_ref re_loop(seq.re.mk_loop(to_re_a, 3, 5), m);
     euf::snode* regex = sg.mk(re_loop);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     ng.add_str_mem(x, regex);
 
     vector<seq::length_constraint> constraints;
@@ -3076,7 +3223,9 @@ static void test_parikh_empty_regex() {
     expr_ref re_empty(seq.re.mk_empty(seq.re.mk_re(str_sort)), m);
     euf::snode* regex = sg.mk(re_empty);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     ng.add_str_mem(x, regex);
 
     vector<seq::length_constraint> constraints;
@@ -3115,7 +3264,9 @@ static void test_parikh_full_char() {
     expr_ref re_range(seq.re.mk_range(unit_a, unit_z), m);
     euf::snode* regex = sg.mk(re_range);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     ng.add_str_mem(x, regex);
 
     vector<seq::length_constraint> constraints;
@@ -3151,7 +3302,9 @@ static void test_parikh_mixed_eq_mem() {
     euf::snode* a = sg.mk_char('A');
 
     // equation: x = A
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     ng.add_str_eq(x, a);
 
     // membership: y in to_re("BC")
@@ -3199,7 +3352,9 @@ static void test_parikh_full_seq_no_bounds() {
     expr_ref re_all(seq.re.mk_full_seq(str_sort), m);
     euf::snode* regex = sg.mk(re_all);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     ng.add_str_mem(x, regex);
 
     vector<seq::length_constraint> constraints;
@@ -3236,7 +3391,9 @@ static void test_parikh_dep_tracking() {
     expr_ref to_re_a(seq.re.mk_to_re(unit_a), m);
     euf::snode* regex = sg.mk(to_re_a);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
+    dummy_simple_solver solver;
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     ng.add_str_mem(x, regex);
 
     vector<seq::length_constraint> constraints;
@@ -3256,7 +3413,7 @@ static void test_parikh_dep_tracking() {
 // -----------------------------------------------------------------------
 
 // tracking solver: records assert_expr calls for inspection
-class tracking_solver : public seq::simple_solver {
+class tracking_solver : public seq::sub_solver_i {
 public:
     vector<expr_ref> asserted;
     ast_manager& m;
@@ -3321,7 +3478,8 @@ static void test_add_lower_int_bound_basic() {
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     ng.add_str_eq(x, x);  // create root node
 
     seq::nielsen_node* node = ng.root();
@@ -3360,7 +3518,8 @@ static void test_add_upper_int_bound_basic() {
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     ng.add_str_eq(x, x);
 
     seq::nielsen_node* node = ng.root();
@@ -3396,7 +3555,8 @@ static void test_add_bound_lb_gt_ub_conflict() {
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     ng.add_str_eq(x, x);
 
     seq::nielsen_node* node = ng.root();
@@ -3421,7 +3581,8 @@ static void test_bounds_cloned() {
     euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     ng.add_str_eq(x, y);
 
     seq::nielsen_node* parent = ng.root();
@@ -3460,7 +3621,8 @@ static void test_subst_does_not_propagate_bounds_single_var() {
     euf::snode* a = sg.mk_char('a');
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     ng.add_str_eq(x, y);
 
     seq::nielsen_node* node = ng.root();
@@ -3495,7 +3657,8 @@ static void test_subst_no_immediate_bound_conflict() {
     euf::snode* b = sg.mk_char('b');
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     ng.add_str_eq(x, a);
 
     seq::nielsen_node* node = ng.root();
@@ -3534,7 +3697,8 @@ static void test_simplify_does_not_add_local_parikh_bounds() {
     euf::snode* regex = sg.mk(re_ab);
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     ng.add_str_mem(x, regex);
 
     seq::nielsen_node* node = ng.root();
@@ -3564,7 +3728,8 @@ static void test_assert_root_constraints_to_solver() {
     euf::snode* ab = sg.mk_concat(a, b);
 
     tracking_solver ts(m);
-    seq::nielsen_graph ng(sg, ts);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, ts, context_solver);
     // equation: x = a·b → generates len(x) = 2 and len(x) >= 0
     ng.add_str_eq(x, ab);
 
@@ -3593,7 +3758,8 @@ static void test_assert_root_constraints_once() {
     euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
 
     tracking_solver ts(m);
-    seq::nielsen_graph ng(sg, ts);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, ts, context_solver);
     ng.add_str_eq(x, y);
 
     // solve is called (iterative deepening runs multiple iterations)
@@ -3624,7 +3790,8 @@ static void test_subst_does_not_propagate_bounds_multi_var() {
     euf::snode* z = sg.mk_var(symbol("z"), sg.get_str_sort());
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     ng.add_str_eq(x, y);
 
     seq::nielsen_node* node = ng.root();
@@ -3655,7 +3822,8 @@ static void test_simplify_unit_prefix_split() {
     seq_util seq(m);
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     // create symbolic char variables a, b (non-concrete -> s_unit)
     sort* char_sort = seq.mk_char_sort();
@@ -3705,7 +3873,8 @@ static void test_simplify_unit_prefix_split_empty_rest() {
     seq_util seq(m);
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     sort* char_sort = seq.mk_char_sort();
     expr_ref sym_a(m.mk_const(symbol("a"), char_sort), m);
@@ -3741,7 +3910,8 @@ static void test_simplify_unit_suffix_split() {
     seq_util seq(m);
 
     dummy_simple_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
 
     sort* char_sort = seq.mk_char_sort();
     expr_ref sym_a(m.mk_const(symbol("a"), char_sort), m);
diff --git a/src/test/seq_parikh.cpp b/src/test/seq_parikh.cpp
index 0b1a25f70..50adb23da 100644
--- a/src/test/seq_parikh.cpp
+++ b/src/test/seq_parikh.cpp
@@ -38,7 +38,7 @@ Author:
 // ---------------------------------------------------------------------------
 // Minimal solver stub (no-op)
 // ---------------------------------------------------------------------------
-class parikh_test_solver : public seq::simple_solver {
+class parikh_test_solver : public seq::sub_solver_i {
 public:
     void push() override {}
     void pop(unsigned) override {}
@@ -486,7 +486,8 @@ static void test_apply_to_node_adds_constraints() {
     euf::sgraph sg(m, eg);
     seq_util seq(m);
     parikh_test_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     seq::seq_parikh parikh(sg);
 
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
@@ -518,7 +519,8 @@ static void test_apply_to_node_stride_one_no_constraints() {
     seq_util seq(m);
     sort_ref str_sort(seq.str.mk_string_sort(), m);
     parikh_test_solver solver;
-    seq::nielsen_graph ng(sg, solver);
+    seq::context_solver_i context_solver;
+    seq::nielsen_graph ng(sg, solver, context_solver);
     seq::seq_parikh parikh(sg);
 
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());