mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-19 15:16:29 +00:00
Code Activity

Trivial constraint != satisfied

Browse source
This commit is contained in:
CEisenhofer 2026-05-27 18:20:03 +02:00
parent c640bf2a2b
commit 4fffc267ec
1 changed files with 2 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1776,11 +1776,9 @@ namespace seq {
}
bool nielsen_node::is_satisfied() const {
if (!m_str_deq.empty())
if (!m_str_deq.empty() || !m_str_eq.empty())
return false;
if (any_of(m_str_eq, [](auto const &eq) { return !eq.is_trivial(); }))
return false;
if (any_of(m_str_mem, [this](auto const &m) { return !m.is_trivial(this) && !m.is_primitive();}))
if (any_of(m_str_mem, [](auto const &m) { return !m.is_primitive();}))
return false;
return true;
}