From 3d26b501e78466f49abb889077d4e8f0d8e6b5f2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 14 Feb 2022 10:31:04 +0200 Subject: [PATCH] fix #5827 #5828 --- src/ast/rewriter/func_decl_replace.cpp | 3 ++- src/smt/smt_internalizer.cpp | 1 - src/smt/theory_datatype.cpp | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/ast/rewriter/func_decl_replace.cpp b/src/ast/rewriter/func_decl_replace.cpp index 512a831af..022afc538 100644 --- a/src/ast/rewriter/func_decl_replace.cpp +++ b/src/ast/rewriter/func_decl_replace.cpp @@ -23,7 +23,8 @@ Revision History: expr_ref func_decl_replace::operator()(expr* e) { m_todo.push_back(e); - + m_refs.push_back(e); + while (!m_todo.empty()) { expr* a = m_todo.back(), *b; if (m_cache.contains(a)) { diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 525d0075e..fd55d5fd0 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -375,7 +375,6 @@ namespace smt { } else { SASSERT(is_app(n)); - SASSERT(!gate_ctx); internalize_term(to_app(n)); } } diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index 765513823..1aa8bbea3 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -297,7 +297,7 @@ namespace smt { TRACE("datatype", tout << "internalizing term:\n" << mk_pp(term, m) << "\n";); unsigned num_args = term->get_num_args(); for (unsigned i = 0; i < num_args; i++) - ctx.internalize(term->get_arg(i), has_quantifiers(term)); + ctx.internalize(term->get_arg(i), m.is_bool(term) && has_quantifiers(term)); // the internalization of the arguments may trigger the internalization of term. if (ctx.e_internalized(term)) return true;