diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp
index e2283a11d8..70808c7365 100644
--- a/src/ast/rewriter/seq_monadic.cpp
+++ b/src/ast/rewriter/seq_monadic.cpp
@@ -396,7 +396,7 @@ lbool seq_monadic::decide_dnf(vector<disjunct> const& dnf) {
         obj_map<expr, expr*> local;               // var -> witness for this disjunct
         for (unsigned gi = 0; gi < groups.size(); ++gi) {
             expr_ref w(m);
-            lbool ne = product_nonempty(groups[gi], m_gen_model ? &w : nullptr);
+            lbool ne = product_nonempty(groups[gi], m_config.m_model ? &w : nullptr);
             if (ne == l_false) { has_empty = true; break; }   // this variable has no value
             if (ne == l_undef) { has_undef = true; continue; }
             if (m_gen_model) { m_pin.push_back(w); local.insert(group_var[gi], w.get()); }
@@ -482,7 +482,7 @@ lbool seq_monadic::decide(membership_vec const& memberships) {
 
 void seq_monadic::minimize_core(membership_vec const& memberships) {
     m_core.reset();
-    if (!m_min_core) {
+    if (!m_config.m_min_core) {
         // No minimization: the core is simply every asserted membership's dependency.
         for (auto const& [term, regex, d] : memberships)
             if (d)
diff --git a/src/ast/rewriter/seq_monadic.h b/src/ast/rewriter/seq_monadic.h
index ee8904d00c..44afad23fb 100644
--- a/src/ast/rewriter/seq_monadic.h
+++ b/src/ast/rewriter/seq_monadic.h
@@ -94,6 +94,7 @@ private:
         void maybe_reset(unsigned cap) { if (m_cache.size() > cap) reset(); }
     };
 
+    struct config {
     ast_manager&    m;
     seq_rewriter&   m_rw;
     th_rewriter     m_thrw;                  // normalizes constant-element derivatives (folds
@@ -105,7 +106,6 @@ private:
     expr_ref_vector m_pin;                  // pins derivative states / witnesses referenced later
     unsigned        m_budget = 0;           // global work budget (decompose disjuncts + product pops)
     bool            m_giveup = false;       // set when the budget is exhausted
-    bool            m_gen_model = true;     // whether solve()/check() extract a feasible model
     bool            m_min_core = true;      // whether check() minimizes the unsat core (else: all deps)
     obj_map<expr, expr*> m_model;           // last extracted model (var -> witness); see get_model()
     cofactor_cache  m_cofactors;            // memoizes derivative_cofactors per regex (see class above)