From fa342c8ea72d3138cb91c20e70641c2e121b05db Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 20 Aug 2014 16:01:06 -0700 Subject: [PATCH] fix(library/unifier): missing set_conflict Signed-off-by: Leonardo de Moura --- src/library/unifier.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index d843facce..54b8fc91f 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -829,15 +829,18 @@ struct unifier_fn { return Continue; bool contains = occurs_meta(lhs, rhs); if (contains) { - if (is_succ(rhs)) + if (is_succ(rhs)) { + set_conflict(j); return Failed; - else + } else { return Continue; + } } lean_assert(!m_subst.is_assigned(lhs)); if (assign(lhs, rhs, j)) { return Solved; } else { + set_conflict(j); return Failed; } }