From b84361805117c7fbe61c72c93253e75822d8c4c0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 20 Feb 2022 13:54:15 -0800 Subject: [PATCH] fix #5798 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_array.cpp | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/src/smt/theory_array.cpp b/src/smt/theory_array.cpp index ab1673a9d..2d166c5f6 100644 --- a/src/smt/theory_array.cpp +++ b/src/smt/theory_array.cpp @@ -240,12 +240,16 @@ namespace smt { bool theory_array::internalize_term_core(app * n) { TRACE("array_bug", tout << mk_bounded_pp(n, m) << "\n";); unsigned num_args = n->get_num_args(); - for (unsigned i = 0; i < num_args; i++) - ctx.internalize(n->get_arg(i), false); - if (ctx.e_internalized(n)) { + for (expr* arg : *n) + ctx.internalize(arg, false); + // force merge-tf by re-internalizing expression. + for (expr* arg : *n) + if (m.is_bool(arg)) + ctx.internalize(arg, false); + if (ctx.e_internalized(n)) return false; - } - enode * e = ctx.mk_enode(n, false, false, true); + + enode * e = ctx.mk_enode(n, false, false, true); if (!is_attached_to_var(e)) mk_var(e);