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";