From 57692811fa8f6e66eea3285d6019a16d31f9a946 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 6 May 2026 03:58:23 -0700 Subject: [PATCH] reduce set of assumptions passed into m_core_solver --- src/smt/seq/seq_nielsen.cpp | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 142f7fc07..92b49d7e4 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -4497,13 +4497,21 @@ namespace seq { u_map expr_to_dep; expr_ref_vector assumptions(m); assumptions.resize(n->constraints().size()); - for (unsigned i = 0; i < assumptions.size(); i++) { - auto& c = n->constraints()[i]; + unsigned j = 0; + for (auto const &c : n->constraints()) { + if (expr_to_dep.contains(c.fml->get_id())) + continue; expr_to_dep.insert_if_not_there(c.fml->get_id(), c.dep); - assumptions[i] = c.fml; + assumptions[j++] = c.fml; } + assumptions.shrink(j); expr_ref_vector core(m); lbool res = m_core_solver.check_with_assumptions(assumptions, core); + CTRACE(seq, res != l_false, + tout << "Unexpected satisfiable/unknown result from core solver " + << res << " " << core + << "\nassumptions\n" + << assumptions << "\n"); VERIFY(res == l_false); dep_tracker dep = dep_mgr().mk_empty();