mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-21 17:39:36 +00:00
Code Activity

merge

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-05-07 10:48:03 -04:00
parent 50f471a95b
commit 7ec3bf55ff
1 changed files with 7 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/smt/seq/seq_nielsen.cpp
View file

@ -4392,11 +4392,15 @@ namespace seq {
SASSERT(m_literal_if_false); SASSERT(m_literal_if_false);
for (unsigned i = node->m_parent_ic_count; i < node->constraints().size(); ++i) { for (unsigned i = node->m_parent_ic_count; i < node->constraints().size(); ++i) {
auto& c = node->constraints()[i]; auto& c = node->constraints()[i];
m_solver.assert_expr(c.fml, c.dep);
auto lit = m_literal_if_false(c.fml); auto lit = m_literal_if_false(c.fml);
// std::cout << "Internalizing literal " << mk_pp(c.fml, m) << " [" << (lit == sat::null_literal) << "]" << std::endl; // std::cout << "Internalizing literal " << mk_pp(c.fml, m) << " [" << (lit == sat::null_literal) << "]" <<
if (lit != sat::null_literal) // std::endl;
if (lit != sat::null_literal) {
node->set_external_conflict(lit, c.dep); node->set_external_conflict(lit, c.dep);
return;
}
m_solver.assert_expr(c.fml);
} }
} }