From bd9b5337af8517dc5874121624df9cb8622d769d Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Thu, 12 Mar 2026 02:53:14 +0000
Subject: [PATCH 1/2] Initial plan


From dac52ae4e0c6b47d25e0178b3d915b4f82d605ae Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Thu, 12 Mar 2026 03:00:38 +0000
Subject: [PATCH 2/2] remove smt_kernel.h dependency from seq_nielsen.cpp

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/smt/seq/seq_nielsen.cpp | 46 +++++++++++++++----------------------
 1 file changed, 18 insertions(+), 28 deletions(-)

diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index 56a16ac1c..3abca0259 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -23,8 +23,6 @@ Author:
 #include "ast/arith_decl_plugin.h"
 #include "ast/ast_pp.h"
 #include "ast/rewriter/th_rewriter.h"
-#include "smt/smt_kernel.h"
-#include "params/smt_params.h"
 #include "util/hashtable.h"
 #include <algorithm>
 #include <cstdlib>
@@ -3400,34 +3398,25 @@ namespace seq {
         if (m_sat_path.empty() && (!m_sat_node || m_sat_node->int_constraints().empty()))
             return false;
 
-        vector<int_constraint> constraints;
-        collect_path_int_constraints(m_sat_node, m_sat_path, constraints);
-        if (constraints.empty())
-            return false;
-
-        // Use a fresh smt::kernel to solve the integer constraints.
-        // Add constraints incrementally, skipping any that would make the system UNSAT
-        // (the search may have taken contradictory branches).
-        ast_manager& m = m_sg.get_manager();
-        smt_params params;
-        smt::kernel fresh_solver(m, params);
-        IF_VERBOSE(1, verbose_stream() << "solve_sat_path_ints: " << constraints.size() << " constraints\n";);
-        for (auto const& ic : constraints) {
-            expr_ref e = int_constraint_to_expr(ic);
-            IF_VERBOSE(2, verbose_stream() << "  constraint: " << mk_bounded_pp(e, m, 5) << "\n";);
-            fresh_solver.push();
-            fresh_solver.assert_expr(e);
-            if (fresh_solver.check() == l_false) {
-                IF_VERBOSE(1, verbose_stream() << "  SKIPPED (infeasible): " << mk_bounded_pp(e, m, 5) << "\n";);
-                fresh_solver.pop(1);
-            }
-        }
-
-        lbool result = fresh_solver.check();
+        // Re-assert the sat-path constraints into m_solver (which holds only root-level
+        // constraints at this point) and extract a model via the injected simple_solver.
+        // The sat path was found by DFS which verified feasibility at every step via
+        // check_int_feasibility, so all constraints along this path are jointly satisfiable
+        // and do not require incremental skipping.
+        IF_VERBOSE(1, verbose_stream() << "solve_sat_path_ints: sat_path length=" << m_sat_path.size() << "\n";);
+        m_solver.push();
+        for (nielsen_edge* e : m_sat_path)
+            for (auto const& ic : e->side_int())
+                m_solver.assert_expr(int_constraint_to_expr(ic));
+        if (m_sat_node)
+            for (auto const& ic : m_sat_node->int_constraints())
+                m_solver.assert_expr(int_constraint_to_expr(ic));
+        lbool result = m_solver.check();
         IF_VERBOSE(1, verbose_stream() << "solve_sat_path_ints result: " << result << "\n";);
         if (result == l_true) {
-            fresh_solver.get_model(mdl);
-            IF_VERBOSE(1, {
+            m_solver.get_model(mdl);
+            IF_VERBOSE(1, if (mdl) {
+                ast_manager& m = m_sg.get_manager();
                 verbose_stream() << "  int_model:\n";
                 for (unsigned i = 0; i < mdl->get_num_constants(); ++i) {
                     func_decl* fd = mdl->get_constant(i);
@@ -3436,6 +3425,7 @@ namespace seq {
                 }
             });
         }
+        m_solver.pop(1);
         return mdl.get() != nullptr;
     }