diff --git a/src/test/nseq_zipt.cpp b/src/test/nseq_zipt.cpp
index 4e4ae4825..c70afaf13 100644
--- a/src/test/nseq_zipt.cpp
+++ b/src/test/nseq_zipt.cpp
@@ -38,6 +38,18 @@ public:
     lbool check() override { return l_true; }
 };
 
+// -----------------------------------------------------------------------
+// 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 {
+public:
+    void push() override {}
+    void pop(unsigned) override {}
+    void assert_expr(expr*) override {}
+    lbool check() override { return l_true; }
+};
+
 // -----------------------------------------------------------------------
 // Helper: build a string snode from a notation string.
 // Uppercase = fresh variable, lowercase/digit = concrete character.
@@ -168,7 +180,7 @@ struct nseq_fixture {
     ast_manager m;
     euf::egraph eg;
     euf::sgraph sg;
-    nseq_zipt_dummy_solver solver;
+    zipt_dummy_simple_solver dummy_solver;
     seq::nielsen_graph ng;
     seq_util su;
     str_builder sb;
@@ -178,7 +190,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, solver), su(m), sb(sg), rb(m, su, sg)
+        : eg(init(m)), sg(m, eg), ng(sg, dummy_solver), su(m), sb(sg), rb(m, su, sg)
     {}
 
     euf::snode* S(const char* s) { return sb.parse(s); }