From 538fbc1b8dd8bbd2c94136f05b1bf2c41d742cbe Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Tue, 24 Mar 2026 13:34:39 +0100 Subject: [PATCH] Added unit (not char) case in apply_const_nielsen --- src/smt/seq/seq_nielsen.cpp | 2 +- src/smt/theory_nseq.cpp | 4 +--- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 308dc8772..98806c37d 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -2011,7 +2011,7 @@ namespace seq { // char vs var: branch 1: var -> ε, branch 2: var -> char·var (depending on direction) // NSB review: add also case var -> unit·var - euf::snode* char_head = lhead->is_char() ? lhead : (rhead->is_char() ? rhead : nullptr); + euf::snode* char_head = (lhead->is_char() || lhead->is_unit()) ? lhead : ((rhead->is_char() || rhead->is_unit()) ? rhead : nullptr); euf::snode* var_head = lhead->is_var() ? lhead : (rhead->is_var() ? rhead : nullptr); if (char_head && var_head) { nielsen_node* child = mk_child(node); diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index 2c7eab148..9f27d7b85 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -185,9 +185,7 @@ namespace smt { if (s1 && s2) { seq::dep_tracker dep = nullptr; ctx.push_trail(restore_vector(m_prop_queue)); - m_prop_queue.push_back(eq_item(s1, s2, get_enode(v1), get_enode(v2), dep)); - std::cout << "Enqueuing equation " << seq::snode_label_html(s1, m) << " = " << seq::snode_label_html(s2, m) << std::endl; - } + m_prop_queue.push_back(eq_item(s1, s2, get_enode(v1), get_enode(v2), dep));} } void theory_nseq::new_diseq_eh(theory_var v1, theory_var v2) {