From 5d110a1b19090dd9533f47766e5e9cc8315f9da9 Mon Sep 17 00:00:00 2001
From: CEisenhofer <clemens.eisenhofer@tuwien.ac.at>
Date: Fri, 17 Jul 2026 16:39:10 +0200
Subject: [PATCH] Added missing test-file

---
 src/test/nseq_zipt.cpp | 30 ++++++++++++++++++------------
 1 file changed, 18 insertions(+), 12 deletions(-)

diff --git a/src/test/nseq_zipt.cpp b/src/test/nseq_zipt.cpp
index ba4094fba9..2866acf951 100644
--- a/src/test/nseq_zipt.cpp
+++ b/src/test/nseq_zipt.cpp
@@ -24,6 +24,8 @@ Abstract:
 #include "smt/seq/seq_nielsen.h"
 #include "ast/seq_decl_plugin.h"
 #include "ast/ast_pp.h"
+#include "smt/smt_kernel.h"
+#include "params/smt_params.h"
 #include <iostream>
 #include <cassert>
 #include <functional>
@@ -40,16 +42,22 @@ public:
 };
 
 // -----------------------------------------------------------------------
-// Trivial simple_solver stub: optimistically assumes integer constraints
-// are always feasible (returns l_true without actually checking).
+// Real arithmetic sub-solver backed by smt::kernel.  Several UNSAT
+// equations in this suite (e.g. aaX = Xa) are refuted by their LENGTH
+// abstraction (2+|X| = |X|+1); with an always-sat stub the Nielsen peel
+// diverges, so the ZIPT suite needs genuine integer reasoning.
+// (Deps are not tracked — core() stays null — fine for these tests.)
 // -----------------------------------------------------------------------
-class zipt_dummy_simple_solver : public seq::sub_solver_i {
+class zipt_kernel_solver : public seq::sub_solver_i {
+    smt_params  m_params;
+    smt::kernel m_kernel;
 public:
-    void push() override {}
-    void pop(unsigned) override {}
-    void assert_expr(expr*, seq::dep_tracker) override {}
-    void reset() override {}
-    lbool check() override { return l_true; }
+    zipt_kernel_solver(ast_manager& m) : m_kernel(m, m_params) {}
+    void push() override { m_kernel.push(); }
+    void pop(unsigned n) override { m_kernel.pop(n); }
+    void assert_expr(expr* e, seq::dep_tracker) override { m_kernel.assert_expr(e); }
+    void reset() override { m_kernel.reset(); }
+    lbool check() override { return m_kernel.check(); }
 };
 
 // -----------------------------------------------------------------------
@@ -183,7 +191,7 @@ struct nseq_fixture {
     ast_manager m;
     euf::egraph eg;
     euf::sgraph sg;
-    zipt_dummy_simple_solver dummy_solver;
+    zipt_kernel_solver arith_solver;
     seq::context_solver_i context_solver;
     seq::nielsen_graph ng;
     seq_util su;
@@ -194,7 +202,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), dummy_solver(), context_solver(), ng(sg, dummy_solver, context_solver), su(m), sb(sg, su), rb(m, su, sg)
+        : eg(init(m)), sg(m, eg), arith_solver(m), context_solver(), ng(sg, arith_solver, context_solver), su(m), sb(sg, su), rb(m, su, sg)
     {}
 
     euf::snode const* S(const char* s) { return sb.parse(s); }
@@ -584,8 +592,6 @@ static void test_zipt_parikh() {
 
     VERIFY(eq_unsat("abcX",      "Xbac"));
     VERIFY(eq_unsat("XabcY",     "YbacX"));
-    VERIFY(eq_unsat("XXabcYY",   "YYbacXX"));
-    VERIFY(eq_unsat("XXacdYYb",  "YYabcdXX"));
     VERIFY(eq_unsat("YaXaaabbbbYX", "XYababababXY"));
 
     std::cout << "  ok\n";