From 29e1fb67d2db3727e7c80529ac8ebcdd70e10aa9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 18 Nov 2019 13:34:45 -0800 Subject: [PATCH] fix #2720, unsound preprocessing in elim_uncnstr_tactic where datatype properties of eliminated subterms is forgotten Signed-off-by: Nikolaj Bjorner --- src/tactic/core/elim_uncnstr_tactic.cpp | 27 +------------------------ 1 file changed, 1 insertion(+), 26 deletions(-) diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp index fd5239236..492e27c9e 100644 --- a/src/tactic/core/elim_uncnstr_tactic.cpp +++ b/src/tactic/core/elim_uncnstr_tactic.cpp @@ -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 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; }