From 09f5d637b06a176836ffc83f543569d877d56a8b Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Tue, 10 Mar 2026 22:44:11 +0000
Subject: [PATCH 1/3] Initial plan


From 0efb7402e80e078e855a762a31ff9043d11a3ec7 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Tue, 10 Mar 2026 22:47:49 +0000
Subject: [PATCH 2/3] Fix build: add dummy_simple_solver to nseq_zipt.cpp
 fixture, fix assert_expr in seq_nielsen.cpp

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/test/nseq_zipt.cpp   | 15 ++++++++++++++-
 src/test/seq_nielsen.cpp |  2 +-
 2 files changed, 15 insertions(+), 2 deletions(-)

diff --git a/src/test/nseq_zipt.cpp b/src/test/nseq_zipt.cpp
index ba2c1d2dd..08014f0af 100644
--- a/src/test/nseq_zipt.cpp
+++ b/src/test/nseq_zipt.cpp
@@ -29,6 +29,18 @@ Abstract:
 #include <functional>
 #include <chrono>
 
+// -----------------------------------------------------------------------
+// Trivial simple_solver stub: optimistically assumes integer constraints
+// are always feasible (returns l_true without actually checking).
+// -----------------------------------------------------------------------
+class 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.
@@ -159,6 +171,7 @@ struct nseq_fixture {
     ast_manager m;
     euf::egraph eg;
     euf::sgraph sg;
+    dummy_simple_solver dummy_solver;
     seq::nielsen_graph ng;
     seq_util su;
     str_builder sb;
@@ -168,7 +181,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), 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); }
diff --git a/src/test/seq_nielsen.cpp b/src/test/seq_nielsen.cpp
index 851dc63ec..c96ebc6ce 100644
--- a/src/test/seq_nielsen.cpp
+++ b/src/test/seq_nielsen.cpp
@@ -27,7 +27,7 @@ public:
     dummy_simple_solver() : seq::simple_solver() {}
     void push() override {}
     void pop(unsigned n) override {}
-    void assert(expr *constraint) override {}
+    void assert_expr(expr *constraint) override {}
     lbool check() override {
         return l_true;
     }

From 3a71f28c6c42f085cfdb10c0081e6587c7c86c3a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 10 Mar 2026 15:49:24 -0700
Subject: [PATCH 3/3] Rename dummy_simple_solver to zipt_dummy_simple_solver

---
 src/test/nseq_zipt.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/test/nseq_zipt.cpp b/src/test/nseq_zipt.cpp
index 08014f0af..b07a636de 100644
--- a/src/test/nseq_zipt.cpp
+++ b/src/test/nseq_zipt.cpp
@@ -33,7 +33,7 @@ Abstract:
 // Trivial simple_solver stub: optimistically assumes integer constraints
 // are always feasible (returns l_true without actually checking).
 // -----------------------------------------------------------------------
-class dummy_simple_solver : public seq::simple_solver {
+class zipt_dummy_simple_solver : public seq::simple_solver {
 public:
     void push() override {}
     void pop(unsigned) override {}
@@ -171,7 +171,7 @@ struct nseq_fixture {
     ast_manager m;
     euf::egraph eg;
     euf::sgraph sg;
-    dummy_simple_solver dummy_solver;
+    zipt_dummy_simple_solver dummy_solver;
     seq::nielsen_graph ng;
     seq_util su;
     str_builder sb;