From 90eb4de526acf7cc67fdc6841513c7b27deda043 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 23 Jan 2021 10:42:43 -0800 Subject: [PATCH] track reference counts of allocated characters Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 9fb9364fc..4db358431 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1994,7 +1994,9 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) { } else if (m_unicode.enabled() && m_util.is_char(e)) { unsigned ch = m_unicode.get_value(n->get_th_var(get_id())); - return alloc(expr_wrapper_proc, m_util.str.mk_char(ch)); + app* val = m_util.str.mk_char(ch); + m_factory->add_trail(val); + return alloc(expr_wrapper_proc, val); } else { return alloc(expr_wrapper_proc, mk_value(e));