From 35481cb045285ba7b8d55965881e00a7387a06fa Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 23 Jul 2014 10:59:53 -0700 Subject: [PATCH] fix(library/unifier): potentially changing flag from l_false ==> l_undef Signed-off-by: Leonardo de Moura --- src/library/unifier.cpp | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) 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