mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 02:42:02 +00:00
Code Activity

add check for root literal assignment

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-01-29 03:14:14 -08:00
parent fe5d17d515
commit 3379155a63
1 changed files with 4 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/sls/sls_context.cpp
View file

@ -142,6 +142,10 @@ namespace sls {
if (m_new_constraint || !unsat().empty()) if (m_new_constraint || !unsat().empty())
return l_undef; return l_undef;
// check if root literals got flipped. is-sat assumes root literals are true
if (any_of(root_literals(), [&](sat::literal lit) { return !is_true(lit); }))
continue;
if (all_of(m_plugins, [&](auto* p) { return !p || p->is_sat(); })) { if (all_of(m_plugins, [&](auto* p) { return !p || p->is_sat(); })) {
VERIFY(unsat().empty() || !m_new_constraint); VERIFY(unsat().empty() || !m_new_constraint);
values2model(); values2model();