mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

Fix complete_partial_func for finite domains (#7547)

Browse source
This commit is contained in:
Can Cebeci 2025-02-06 01:14:55 +01:00 committed by GitHub
parent 091984419e
commit af270da785
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 4 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/smt/proto_model/proto_model.cpp
View file

@ -345,14 +345,12 @@ void proto_model::compress() {
void proto_model::complete_partial_func(func_decl * f, bool use_fresh) { void proto_model::complete_partial_func(func_decl * f, bool use_fresh) {
func_interp * fi = get_func_interp(f); func_interp * fi = get_func_interp(f);
if (fi && fi->is_partial()) { if (fi && fi->is_partial()) {
expr * else_value; expr * else_value = nullptr;
if (use_fresh) { if (use_fresh)
else_value = get_fresh_value(f->get_range()); else_value = get_fresh_value(f->get_range());
} if (!else_value)
else {
else_value = fi->get_max_occ_result(); else_value = fi->get_max_occ_result();
} if (!else_value)
if (else_value == nullptr)
else_value = get_some_value(f->get_range()); else_value = get_some_value(f->get_range());
fi->set_else(else_value); fi->set_else(else_value);
} }