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

fix #2720, unsound preprocessing in elim_uncnstr_tactic where datatype properties of eliminated subterms is forgotten

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-11-18 13:34:45 -08:00
parent 05ad90c976
commit 29e1fb67d2
1 changed files with 1 additions and 26 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
src/tactic/core/elim_uncnstr_tactic.cpp
View file

@ -675,18 +675,7 @@ class elim_uncnstr_tactic : public tactic {
}
app * process_datatype_app(func_decl * f, unsigned num, expr * const * args) {
if (m_dt_util.is_recognizer(f)) {
SASSERT(num == 1);
if (uncnstr(args[0])) {
if (!m_mc) {
app * r;
mk_fresh_uncnstr_var_for(f, num, args, r);
return r;
}
// TODO: handle model generation
}
}
else if (m_dt_util.is_accessor(f)) {
if (m_dt_util.is_accessor(f)) {
SASSERT(num == 1);
if (uncnstr(args[0])) {
if (!m_mc) {
@ -713,20 +702,6 @@ class elim_uncnstr_tactic : public tactic {
return u;
}
}
else if (m_dt_util.is_constructor(f)) {
if (uncnstr(num, args)) {
app * u;
if (!mk_fresh_uncnstr_var_for(f, num, args, u))
return u;
if (!m_mc)
return u;
ptr_vector<func_decl> const & accs = *m_dt_util.get_constructor_accessors(f);
for (unsigned i = 0; i < num; i++) {
add_def(args[i], m().mk_app(accs[i], u));
}
return u;
}
}
return nullptr;
}