diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp
index 27d0531af..618394ac1 100644
--- a/src/nlsat/nlsat_explain.cpp
+++ b/src/nlsat/nlsat_explain.cpp
@@ -1744,7 +1744,16 @@ namespace nlsat {
                     solve_eq(x, eq_index, ps);
                 }
                 else {
-                    project_pairs(x, eq_index, ps);
+                    add_zero_assumption(p);
+
+                    for (unsigned j = 0; j < ps.size(); ++j) {
+                        if (j == eq_index)
+                            continue;
+                        p = ps.get(j);
+                        int s = sign(p);
+                        atom::kind k = (s == 0)?(atom::EQ):((s < 0)?(atom::LT):(atom::GT));
+                        add_simple_assumption(k, p, false);
+                    }
                 }
                 return;
             }
diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp
index d81048c3d..8a6f910bc 100644
--- a/src/qe/nlqsat.cpp
+++ b/src/qe/nlqsat.cpp
@@ -480,8 +480,10 @@ namespace qe {
                 num_scopes = 2*(level()/2);
             }
             else {
-                SASSERT(clevel.max() + 2 <= level());
-                num_scopes = level() - clevel.max();
+                if (clevel.max() + 2 <= level())                    
+                    num_scopes = level() - clevel.max();
+                else
+                    num_scopes = 2; // the projection contains auxiliary variables from root objects.
                 SASSERT(num_scopes >= 2);
             }