mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

Model completion bug fix

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-08-30 20:35:31 +01:00
parent 1a1c705376
commit d61df6b91f
1 changed files with 8 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/cmd_context/cmd_context.cpp
View file

@ -1701,9 +1701,14 @@ void cmd_context::complete_model() {
func_decl * f = v.get_entry(i);
if (!md->has_interpretation(f)) {
sort * range = f->get_range();
func_interp * fi = alloc(func_interp, m(), f->get_arity());
fi->set_else(m().get_some_value(range));
md->register_decl(f, fi);
expr * some_val = m().get_some_value(range);
if (f->get_arity() > 0) {
func_interp * fi = alloc(func_interp, m(), f->get_arity());
fi->set_else(some_val);
md->register_decl(f, fi);
}
else
md->register_decl(f, some_val);
}
}
}