From 577ca128a1d02b0e5e2c12d82af2be5005d9a649 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 29 Oct 2013 03:01:17 -0700
Subject: [PATCH] fix(library/elaborator): add missing conflict justification

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/library/elaborator/elaborator.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp
index 90549c205..aa6ce89a4 100644
--- a/src/library/elaborator/elaborator.cpp
+++ b/src/library/elaborator/elaborator.cpp
@@ -1158,6 +1158,7 @@ class elaborator::imp {
                             push_front(mk_eq_constraint(ctx, arg(a, i), arg(b, i), new_jst));
                         return true;
                     } else {
+                        m_conflict = justification(new unification_failure_justification(c));
                         return false;
                     }
                 }