From 5d457c95aa312c06342d6076a36133f1da812d88 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 26 Feb 2018 21:00:41 +0900 Subject: [PATCH] update registration of built-ins Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 6d49d8883..3462d0cac 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -2013,9 +2013,10 @@ void cmd_context::dt_eh::operator()(sort * dt, pdecl* pd) { for (func_decl * c : *m_dt_util.get_datatype_constructors(dt)) { TRACE("new_dt_eh", tout << "new constructor: " << c->get_name() << "\n";); m_owner.insert(c); - func_decl * r = m_dt_util.get_constructor_recognizer(c); - m_owner.insert(r); - TRACE("new_dt_eh", tout << "new recognizer: " << r->get_name() << "\n";); + // Don't insert recognizer any longer. It is a built-in function. + // func_decl * r = m_dt_util.get_constructor_recognizer(c); + // m_owner.insert(r); + // TRACE("new_dt_eh", tout << "new recognizer: " << r->get_name() << "\n";); for (func_decl * a : *m_dt_util.get_constructor_accessors(c)) { TRACE("new_dt_eh", tout << "new accessor: " << a->get_name() << "\n";); m_owner.insert(a);