mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

track reference counts of allocated characters

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-01-23 10:42:43 -08:00
parent 6edabd6c03
commit 90eb4de526
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/smt/theory_seq.cpp
View file

@ -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));