mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

Use register_value instead of direct set insertion

Browse source 
Replaced direct insertion into set with register_value calls.
This commit is contained in:
Nikolaj Bjorner 2025-10-16 12:56:05 +02:00 • committed by GitHub
parent 48a8269a8d
commit d3e262af85
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/model/finite_set_value_factory.cpp
View file

@ -36,13 +36,13 @@ expr * finite_set_value_factory::get_fresh_value(sort * s) {
// If no values have been generated yet, use get_some_value
if (set->empty()) {
auto r = u.mk_empty(s);
set->insert(r);
register_value(r);
return r;
}
auto e = md.get_fresh_value(elem_sort);
if (e) {
auto r = u.mk_singleton(e);
set->insert(r);
register_value(r);
return r;
}