From 54782e68e0a821465b7fb7a4e8d4bef91c74629c Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Wed, 27 May 2026 18:59:00 +0200 Subject: [PATCH] Disequalities over units can be processed differently --- src/smt/seq/seq_nielsen.cpp | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index ebdd3e8be..8ac7c663c 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -1305,6 +1305,15 @@ namespace seq { set_conflict(backtrack_reason::symbol_clash, deq.m_dep); return simplify_result::conflict; } + if (deq.m_lhs->length() == 1 && deq.m_rhs->length() == 1) { + expr* l, *r; + if (graph().seq().str.is_unit(deq.m_lhs->get_expr(), l) && + graph().seq().str.is_unit(deq.m_rhs->get_expr(), r)) { + + add_constraint(constraint(m.mk_not(m.mk_eq(l, r)), deq.m_dep, m)); + continue; + } + } if (deq.m_lhs->is_empty() && !deq.m_rhs->is_empty()) { if (cannot_be_empty(deq.m_rhs)) continue;