mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
update registration of built-ins
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
0199c7515f
commit
5d457c95aa
|
@ -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);
|
||||
|
|
Loading…
Reference in a new issue