diff --git a/src/cmd_context/eval_cmd.cpp b/src/cmd_context/eval_cmd.cpp
index 8819eb584..70a48da5f 100644
--- a/src/cmd_context/eval_cmd.cpp
+++ b/src/cmd_context/eval_cmd.cpp
@@ -57,6 +57,8 @@ public:
 
     void execute(cmd_context & ctx) override {
         model_ref md;
+        if (ctx.ignore_check())
+            return;
         if (!ctx.is_model_available(md))
             throw cmd_exception("model is not available");
         if (!m_target)
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 4a254ac06..12dfb72b5 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -4192,17 +4192,19 @@ namespace sat {
             m_ext->find_mutexes(_lits, mutexes);
         }
         unsigned_vector ps;
-        for (literal lit : _lits) {
+        for (literal lit : _lits) 
             ps.push_back(lit.index());
-        }
         mc.cliques(ps, _mutexes);
+        vector<vector<literal_vector>> sorted;
         for (auto const& mux : _mutexes) {
             literal_vector clique;
-            for (auto const& idx : mux) {
+            sorted.reserve(mux.size() + 1);
+            for (auto const& idx : mux) 
                 clique.push_back(to_literal(idx));
-            }
-            mutexes.push_back(clique);
+            sorted[mux.size()].push_back(clique);
         }
+        for (unsigned i = sorted.size(); i-- > 0; ) 
+            mutexes.append(sorted[i]);
         return l_true;
     }