From 917abe5f7aa506626b62d75e72c93844f9e38d3c Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sun, 28 Jun 2026 21:51:49 +0000 Subject: [PATCH] Fix model-finder segfault on invalid AUF variable indices --- src/smt/smt_model_finder.cpp | 86 +++++++++++++++++++++++++++--------- 1 file changed, 64 insertions(+), 22 deletions(-) diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 4ba66a51be..b5e6e5aaa8 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -1179,6 +1179,14 @@ namespace smt { virtual void populate_inst_sets(quantifier* q, func_decl* mhead, ptr_vector& uvar_inst_sets, context* ctx) {} }; + static bool has_uvar(quantifier* q, unsigned i) { + return i < q->get_num_decls(); + } + + static node* get_uvar_if_valid(quantifier* q, unsigned i, auf_solver& s) { + return has_uvar(q, i) ? s.get_uvar(q, i) : nullptr; + } + class f_var : public qinfo { protected: func_decl* m_f; @@ -1204,7 +1212,9 @@ namespace smt { void process_auf(quantifier* q, auf_solver& s, context* ctx) override { node* n1 = s.get_A_f_i(m_f, m_arg_i); - node* n2 = s.get_uvar(q, m_var_j); + node* n2 = get_uvar_if_valid(q, m_var_j, s); + if (!n2) + return; CTRACE(model_finder, n1->get_sort() != n2->get_sort(), tout << "sort bug:\n" << mk_ismt2_pp(q->get_expr(), m) << "\n" << mk_ismt2_pp(q, m) << "\n"; tout << "decl(0): " << q->get_decl_name(0) << "\n"; @@ -1286,17 +1296,22 @@ namespace smt { void process_auf(quantifier* q, auf_solver& s, context* ctx) override { // just create the nodes /* node * A_f_i = */ s.get_A_f_i(m_f, m_arg_i); - /* node * S_j = */ s.get_uvar(q, m_var_j); + /* node * S_j = */ get_uvar_if_valid(q, m_var_j, s); } void populate_inst_sets(quantifier* q, auf_solver& s, context* ctx) override { // S_j is not necessary equal to A_f_i. node* A_f_i = s.get_A_f_i(m_f, m_arg_i)->get_root(); - node* S_j = s.get_uvar(q, m_var_j)->get_root(); + node* S_j = get_uvar_if_valid(q, m_var_j, s); + if (!S_j) + return; + S_j = S_j->get_root(); if (A_f_i == S_j) { // there is no finite fixpoint... we just copy the i-th arguments of A_f_i - m_offset // hope for the best... - node* S_j = s.get_uvar(q, m_var_j); + node* S_j = get_uvar_if_valid(q, m_var_j, s); + if (!S_j) + return; for (enode* n : ctx->enodes_of(m_f)) { if (ctx->is_relevant(n)) { arith_rewriter arith_rw(m); @@ -1360,7 +1375,10 @@ namespace smt { void populate_inst_sets2(quantifier* q, auf_solver& s, context* ctx) override { node* A_f_i = s.get_A_f_i(m_f, m_arg_i)->get_root(); - node* S_j = s.get_uvar(q, m_var_j)->get_root(); + node* S_j = get_uvar_if_valid(q, m_var_j, s); + if (!S_j) + return; + S_j = S_j->get_root(); // If A_f_i == S_j, then there is no finite fixpoint, so we do nothing here. if (A_f_i != S_j) { // enforce @@ -1399,11 +1417,13 @@ namespace smt { } void process_auf(quantifier *q, auf_solver &s, context *ctx) override { - /* node * S_i = */ s.get_uvar(q, m_var_i); + /* node * S_i = */ get_uvar_if_valid(q, m_var_i, s); } void populate_inst_sets(quantifier *q, auf_solver &s, context *ctx) override { - node *S = s.get_uvar(q, m_var_i); + node* S = get_uvar_if_valid(q, m_var_i, s); + if (!S) + return; sort *srt = S->get_sort(); IF_VERBOSE(3, verbose_stream() << "ho_var::populate_inst_sets: " << q->get_id() << " " << mk_pp(srt, m) << "\n";); @@ -1530,7 +1550,9 @@ namespace smt { for (enode* n : arrays) { tout << "#" << n->get_expr_id() << "\n" << mk_pp(n->get_expr(), m) << "\n"; }); - node* n1 = s.get_uvar(q, m_var_j); + node* n1 = get_uvar_if_valid(q, m_var_j, s); + if (!n1) + return; for (enode* n : arrays) { auto ground_array = n->get_expr(); func_decl* f = get_array_func_decl(ground_array, s); @@ -1597,8 +1619,10 @@ namespace smt { char const* get_kind() const override { return "x_eq_y"; } void process_auf(quantifier* q, auf_solver& s, context* ctx) override { - node* n1 = s.get_uvar(q, m_var_i); - node* n2 = s.get_uvar(q, m_var_j); + node* n1 = get_uvar_if_valid(q, m_var_i, s); + node* n2 = get_uvar_if_valid(q, m_var_j, s); + if (!n1 || !n2) + return; n1->insert_avoid(n2); if (n1 != n2) n2->insert_avoid(n1); @@ -1611,8 +1635,10 @@ namespace smt { char const* get_kind() const override { return "x_neq_y"; } void process_auf(quantifier* q, auf_solver& s, context* ctx) override { - node* n1 = s.get_uvar(q, m_var_i); - node* n2 = s.get_uvar(q, m_var_j); + node* n1 = get_uvar_if_valid(q, m_var_i, s); + node* n2 = get_uvar_if_valid(q, m_var_j, s); + if (!n1 || !n2) + return; n1->merge(n2); } }; @@ -1623,8 +1649,10 @@ namespace smt { char const* get_kind() const override { return "x_leq_y"; } void process_auf(quantifier* q, auf_solver& s, context* ctx) override { - node* n1 = s.get_uvar(q, m_var_i); - node* n2 = s.get_uvar(q, m_var_j); + node* n1 = get_uvar_if_valid(q, m_var_i, s); + node* n2 = get_uvar_if_valid(q, m_var_j, s); + if (!n1 || !n2) + return; n1->merge(n2); n1->set_mono_proj(); } @@ -1637,8 +1665,10 @@ namespace smt { char const* get_kind() const override { return "x_sleq_y"; } void process_auf(quantifier* q, auf_solver& s, context* ctx) override { - node* n1 = s.get_uvar(q, m_var_i); - node* n2 = s.get_uvar(q, m_var_j); + node* n1 = get_uvar_if_valid(q, m_var_i, s); + node* n2 = get_uvar_if_valid(q, m_var_j, s); + if (!n1 || !n2) + return; n1->merge(n2); n1->set_mono_proj(); n1->set_signed_proj(); @@ -1673,17 +1703,23 @@ namespace smt { char const* get_kind() const override { return "x_eq_t"; } void process_auf(quantifier* q, auf_solver& s, context* ctx) override { - node* n1 = s.get_uvar(q, m_var_i); + node* n1 = get_uvar_if_valid(q, m_var_i, s); + if (!n1) + return; n1->insert_exception(m_t); } void populate_inst_sets(quantifier* q, auf_solver& slv, context* ctx) override { + if (!has_uvar(q, m_var_i)) + return; unsigned num_vars = q->get_num_decls(); sort* s = q->get_decl_sort(num_vars - m_var_i - 1); if (m.is_uninterp(s)) { // For uninterpreted sorts, we add all terms in the context. // See Section 4.1 in the paper "Complete Quantifier Instantiation" - node* S_q_i = slv.get_uvar(q, m_var_i); + node* S_q_i = get_uvar_if_valid(q, m_var_i, slv); + if (!S_q_i) + return; for (enode* n : ctx->enodes()) { if (ctx->is_relevant(n) && n->get_expr()->get_sort() == s) { S_q_i->insert(n->get_expr(), n->get_generation()); @@ -1701,11 +1737,13 @@ namespace smt { void process_auf(quantifier* q, auf_solver& s, context* ctx) override { // make sure that S_q_i is create. - s.get_uvar(q, m_var_i); + get_uvar_if_valid(q, m_var_i, s); } void populate_inst_sets(quantifier* q, auf_solver& s, context* ctx) override { - node* S_q_i = s.get_uvar(q, m_var_i); + node* S_q_i = get_uvar_if_valid(q, m_var_i, s); + if (!S_q_i) + return; S_q_i->insert(m_t, 0); } }; @@ -1718,12 +1756,16 @@ namespace smt { void process_auf(quantifier* q, auf_solver& s, context* ctx) override { // make sure that S_q_i is create. - node* n1 = s.get_uvar(q, m_var_i); + node* n1 = get_uvar_if_valid(q, m_var_i, s); + if (!n1) + return; n1->set_mono_proj(); } void populate_inst_sets(quantifier* q, auf_solver& s, context* ctx) override { - node* S_q_i = s.get_uvar(q, m_var_i); + node* S_q_i = get_uvar_if_valid(q, m_var_i, s); + if (!S_q_i) + return; S_q_i->insert(m_t, 0); } };