From d1aaae68560c5ece880171053b201be55f1a09e4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 6 Jul 2026 17:43:01 -0700 Subject: [PATCH] allow lambdas in select positions for model, ignore beta redex incompletness when using arrays for MBQI --- src/smt/theory_array_full.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp index 865d5bca95..86652d12ba 100644 --- a/src/smt/theory_array_full.cpp +++ b/src/smt/theory_array_full.cpp @@ -853,6 +853,8 @@ namespace smt { } bool theory_array_full::has_non_beta_as_array() { + if (ctx.get_fparams().m_array_fake_support) + return false; for (enode* n : m_as_array) { for (enode* p : n->get_parents()) if (ctx.is_relevant(p) && !ctx.is_beta_redex(p, n)) { @@ -862,7 +864,7 @@ namespace smt { } for (enode* n : m_lambdas) for (enode* p : n->get_parents()) - if (ctx.is_relevant(p) && !is_default(p) && !ctx.is_beta_redex(p, n) && !is_congruent_eq(p)) { + if (ctx.is_relevant(p) && !is_default(p) && !is_select(p) && !ctx.is_beta_redex(p, n) && !is_congruent_eq(p)) { TRACE(array, tout << "lambda is not a beta redex " << enode_pp(p, ctx) << "\n"); return true; }