diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp
index 062ae0216..d3693f13c 100644
--- a/src/library/unifier.cpp
+++ b/src/library/unifier.cpp
@@ -84,8 +84,12 @@ lbool occurs_context_check(substitution & s, expr const & e, expr const & m, buf
                 }
                 return false; // do not visit type
             } else if (is_meta(e)) {
-                if (!context_check(e, locals) || s.occurs(m, e))
-                    r = l_undef;
+                if (r == l_true) {
+                    if (!context_check(e, locals))
+                        r = l_undef;
+                    if (s.occurs(m, e))
+                        r = l_undef;
+                }
                 if (get_app_fn(e) == m)
                     r = l_false;
                 return false; // do not visit children