From 6fd303c4b987e1df8d13fe01243edceb701f9a97 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 24 Jun 2026 20:38:15 -0700 Subject: [PATCH] set the auf flag to false in all cases Signed-off-by: Nikolaj Bjorner --- src/smt/smt_model_finder.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 9483faecff..6ef1e55c6e 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -1413,6 +1413,8 @@ namespace smt { // add other possible relevant functions such as equality over srt, Boolean operators ast_mark visited; + tn.add_production(m.mk_true()); + tn.add_production(m.mk_false()); for (enode *n : ctx->enodes()) { if (!ctx->is_relevant(n)) continue; @@ -2187,9 +2189,7 @@ namespace smt { if (m_array_util.is_array(curr)) { insert_qinfo(alloc(ho_var, m, to_var(curr)->get_idx())); } - else { - m_info->m_is_auf = false; // unexpected occurrence of variable. - } + m_info->m_is_auf = false; } else { SASSERT(is_lambda(curr));