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] 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;
     }