From 4d2338133faa8dba88a82dcf4adae720d985d27a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 10 Sep 2025 10:54:55 -0700 Subject: [PATCH] pop to search level when finding split atoms Signed-off-by: Nikolaj Bjorner --- src/math/lp/cross_nested.h | 1 + src/smt/smt_parallel2.cpp | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/math/lp/cross_nested.h b/src/math/lp/cross_nested.h index b232db604..192480226 100644 --- a/src/math/lp/cross_nested.h +++ b/src/math/lp/cross_nested.h @@ -63,6 +63,7 @@ public: void run(nex *e) { + TRACE(nla_cn, tout << *e << "\n";); SASSERT(m_nex_creator.is_simplified(*e)); m_e = e; diff --git a/src/smt/smt_parallel2.cpp b/src/smt/smt_parallel2.cpp index f12f5ed7a..4404387d2 100644 --- a/src/smt/smt_parallel2.cpp +++ b/src/smt/smt_parallel2.cpp @@ -350,7 +350,7 @@ namespace smt { expr_ref result(m); double score = 0; unsigned n = 0; - + ctx->pop_to_search_lvl(); for (bool_var v = 0; v < ctx->get_num_bool_vars(); ++v) { if (ctx->get_assignment(v) != l_undef) continue;