From 7ec3bf55ffe6a47e8035ef036e3d53a2c2e1fb81 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 7 May 2026 10:48:03 -0400 Subject: [PATCH] merge Signed-off-by: Nikolaj Bjorner --- src/smt/seq/seq_nielsen.cpp | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 283ac3c26..3df48224c 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -4392,11 +4392,15 @@ namespace seq { SASSERT(m_literal_if_false); for (unsigned i = node->m_parent_ic_count; i < node->constraints().size(); ++i) { auto& c = node->constraints()[i]; - m_solver.assert_expr(c.fml, c.dep); auto lit = m_literal_if_false(c.fml); - // std::cout << "Internalizing literal " << mk_pp(c.fml, m) << " [" << (lit == sat::null_literal) << "]" << std::endl; - if (lit != sat::null_literal) + // std::cout << "Internalizing literal " << mk_pp(c.fml, m) << " [" << (lit == sat::null_literal) << "]" << + // std::endl; + if (lit != sat::null_literal) { node->set_external_conflict(lit, c.dep); + return; + } + m_solver.assert_expr(c.fml); + } }