From 238a0dbfba0e6c099f19a84db86e4900a6ff2a18 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 22 Jun 2014 14:09:06 -0700
Subject: [PATCH] fix(library/unifier): memory violation, and missing
 set_conflict

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/library/unifier.cpp | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp
index 77d51e3a3..689be2b66 100644
--- a/src/library/unifier.cpp
+++ b/src/library/unifier.cpp
@@ -221,7 +221,7 @@ struct unifier_fn {
         cnstr_idx_set s;
         name_to_cnstrs & map = MVar ? m_mvar_occs : m_mlvl_occs;
         auto it = map.find(m);
-        if (!it)
+        if (it)
             s = *it;
         if (!s.contains(cidx)) {
             s.insert(cidx);
@@ -472,8 +472,10 @@ struct unifier_fn {
         lean_assert(!is_choice_cnstr(c));
         lazy_list<constraints> alts = m_plugin(c, m_ngen.mk_child());
         auto r = alts.pull();
-        if (!r)
+        if (!r) {
+            set_conflict(c.get_justification());
             return false;
+        }
         // TODO(Leo): create backtracking point
         return true;
     }