From 8b2643ff0214312d615af966fa2eaab1d60cd447 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Tue, 21 Apr 2026 18:37:53 +0200 Subject: [PATCH] Missing unit around symbolic characters --- src/smt/seq/seq_nielsen.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index b0bf0462e..98f3b0696 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -3913,7 +3913,8 @@ namespace seq { SASSERT(var && var->is_var()); th_rewriter rw(m); auto e = get_current_skolem(var); - return skolem(m, rw).mk("char!", e, m_seq.mk_char_sort()); + return expr_ref( + m_seq.str.mk_unit(skolem(m, rw).mk("char!", e, m_seq.mk_char_sort())), m); } expr_ref nielsen_graph::get_or_create_gpower_n_var(euf::snode* var) {