From e7e686127bbc65834c09fa85686fbe8e1c497adf Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Jul 2026 13:46:23 -0700 Subject: [PATCH] fix signature regression for unit test Signed-off-by: Nikolaj Bjorner --- src/smt/smt_enode.cpp | 4 ++-- src/smt/smt_enode.h | 4 ++-- src/smt/smt_internalizer.cpp | 2 +- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/smt/smt_enode.cpp b/src/smt/smt_enode.cpp index 87b9c64283..96aca24102 100644 --- a/src/smt/smt_enode.cpp +++ b/src/smt/smt_enode.cpp @@ -25,7 +25,7 @@ namespace smt { /** \brief Initialize an enode in the given memory position. */ - enode * enode::init(ast_manager & m, void * mem, app2enode_t const & app2enode, app * owner, + enode * enode::init(ast_manager & m, void * mem, app2enode_t const & app2enode, expr * owner, bool suppress_args, bool merge_tf, unsigned iscope_lvl, bool cgc_enabled, bool update_children_parent) { SASSERT(m.is_bool(owner) || !merge_tf); @@ -63,7 +63,7 @@ namespace smt { return n; } - enode * enode::mk(ast_manager & m, region & r, app2enode_t const & app2enode, app * owner, + enode * enode::mk(ast_manager & m, region & r, app2enode_t const & app2enode, expr * owner, bool suppress_args, bool merge_tf, unsigned iscope_lvl, bool cgc_enabled, bool update_children_parent) { SASSERT(m.is_bool(owner) || !merge_tf); diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h index 07bb99219d..c1ac30929e 100644 --- a/src/smt/smt_enode.h +++ b/src/smt/smt_enode.h @@ -131,7 +131,7 @@ namespace smt { friend class tmp_enode; - static enode * init(ast_manager & m, void * mem, app2enode_t const & app2enode, app * owner, + static enode * init(ast_manager & m, void * mem, app2enode_t const & app2enode, expr * owner, bool suppress_args, bool merge_tf, unsigned iscope_lvl, bool cgc_enabled, bool update_children_parent); public: @@ -140,7 +140,7 @@ namespace smt { return sizeof(enode) + num_args * sizeof(enode*); } - static enode * mk(ast_manager & m, region & r, app2enode_t const & app2enode, app * owner, + static enode * mk(ast_manager & m, region & r, app2enode_t const & app2enode, expr * owner, bool suppress_args, bool merge_tf, unsigned iscope_lvl, bool cgc_enabled, bool update_children_parent); diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index c4afaf43f5..31c3c8486e 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -1060,7 +1060,7 @@ namespace smt { CTRACE(cached_generation, generation != m_generation, tout << "cached_generation: #" << n->get_id() << " " << generation << " " << m_generation << "\n";); } - enode *e = enode::mk(m, get_region(), m_app2enode, to_app(n), suppress_args, merge_tf, m_scope_lvl, + enode *e = enode::mk(m, get_region(), m_app2enode, n, suppress_args, merge_tf, m_scope_lvl, cgc_enabled, true); TRACE(mk_enode_detail, tout << "e.get_num_args() = " << e->get_num_args() << "\n";); if (m.is_unique_value(n))