diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index ea3f3534b..5acf273fe 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -914,7 +914,7 @@ private:
         }
         IF_VERBOSE(1, verbose_stream() << "Verifying solution\n";);
         model_evaluator eval(*mdl);
-        // eval.set_model_completion(false);
+        eval.set_model_completion(true);
         bool all_true = true;
         //unsigned i = 0;
         for (expr * f : m_fmls) {