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

patch to fix #5110

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-04-08 11:25:20 -07:00
parent d91eac24b7
commit 44156f9f55
2 changed files with 11 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/ast/datatype_decl_plugin.cpp
View file

@ -641,13 +641,13 @@ namespace datatype {
}
bool util::is_considered_uninterpreted(func_decl * f, unsigned n, expr* const* args) {
if (is_accessor(f)) {
func_decl* c = get_accessor_constructor(f);
SASSERT(n == 1);
if (is_constructor(args[0]))
return to_app(args[0])->get_decl() != c;
if (!is_accessor(f))
return false;
}
func_decl* c = get_accessor_constructor(f);
SASSERT(n == 1);
std::cout << f->get_name() << " " << mk_pp(args[0], m) << "\n";
if (is_constructor(args[0]))
return to_app(args[0])->get_decl() != c;
return false;
}

5
src/model/model_evaluator.cpp
View file

@ -363,12 +363,17 @@ struct evaluator_cfg : public default_rewriter_cfg {
result = m.get_some_value(f->get_range());
return BR_DONE;
}
else if (m_dt.is_accessor(f) && !is_ground(args[0])) {
result = m.mk_app(f, num, args);
return BR_DONE;
}
if (fi) {
if (fi->is_partial())
fi->set_else(m.get_some_value(f->get_range()));
var_subst vs(m, false);
result = vs(fi->get_interp(), num, args);
std::cout << result << "\n";
return BR_REWRITE_FULL;
}