From 4fffc267ecfc9bc8a7fbc8c4be872076a1e2da4b Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Wed, 27 May 2026 18:20:03 +0200 Subject: [PATCH] Trivial constraint != satisfied --- src/smt/seq/seq_nielsen.cpp | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index beeaeae0f..ebdd3e8be 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -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; }