From aa872bd289ae9a2d7dfe6a2da079baa0400f24a8 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson <5377127+levnach@users.noreply.github.com> Date: Mon, 8 Jun 2026 19:35:49 -0700 Subject: [PATCH] spacer: enable model completion in arith qe_project (#9776) Variables to be projected may not be assigned in the model (e.g. grounded auxiliary variables that are don't-cares). Enable model completion in the arith `qe_project` so their evaluation yields concrete numerals, matching the behavior of the native MBP arith projector. Two call sites in `arith_project_util` (`src/muz/spacer/spacer_qe_project.cpp`) now install a `model::scoped_model_completion` before evaluating projected variables against the model. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/muz/spacer/spacer_qe_project.cpp | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/muz/spacer/spacer_qe_project.cpp b/src/muz/spacer/spacer_qe_project.cpp index d47a09d14..58499c028 100644 --- a/src/muz/spacer/spacer_qe_project.cpp +++ b/src/muz/spacer/spacer_qe_project.cpp @@ -1148,6 +1148,7 @@ class arith_project_util { expr_ref_vector const &lits) { app_ref_vector new_vars(m); expr_ref_vector result(lits); + model::scoped_model_completion _smc(mdl, true); for (unsigned i = 0; i < vars.size(); ++i) { app *v = vars.get(i); m_var = alloc(contains_app, m, v); @@ -1183,6 +1184,12 @@ class arith_project_util { expr_map &map) { app_ref_vector new_vars(m); + // Variables to be projected may not be assigned in the model + // (e.g. grounded auxiliary variables that are don't-cares). Enable + // model completion so their evaluation yields concrete numerals, + // matching the behavior of the native MBP arith projector. + model::scoped_model_completion _smc(mdl, true); + // factor out mod terms by introducing new variables TRACE(qe, tout << "before factoring out mod terms:" << "\n"; tout << mk_pp(fml, m) << "\n"; tout << "mdl:\n";