mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

fixup

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-10-16 13:29:38 +02:00
parent cc8bfd7890
commit 26d37c7b30
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/model/finite_set_value_factory.cpp
View file

@ -40,9 +40,10 @@ expr * finite_set_value_factory::get_fresh_value(sort * s) {
register_value(r); register_value(r);
return r; return r;
} }
auto e = md.get_fresh_value(elem_sort); auto e = m_model.get_fresh_value(elem_sort);
if (e) { if (e) {
auto r = u.mk_singleton(e); auto r = u.mk_singleton(e);
register_value(e); // register e so we can access the finite domain within this class
register_value(r); register_value(r);
return r; return r;
} }