From ad12abcdb43febb2dac1e568a74ec140d8067f4a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 30 Jun 2014 18:22:05 -0700
Subject: [PATCH] fix(library/unifier): bug in process_eq_constraint

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 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 79143530ce..dd54a6d17b 100644
--- a/src/library/unifier.cpp
+++ b/src/library/unifier.cpp
@@ -575,8 +575,12 @@ struct unifier_fn {
         // Update justification using the justification of the instantiated metavariables
         justification new_jst = mk_composite1(mk_composite1(c.get_justification(), lhs_jst.second), rhs_jst.second);
         if (!has_metavar(lhs) && !has_metavar(rhs)) {
-            set_conflict(new_jst);
-            return false; // trivial failure
+            if (!m_tc.is_def_eq(lhs, rhs, new_jst)) {
+                set_conflict(new_jst);
+                return false; // trivial failure
+            } else {
+                return true;
+            }
         }
 
         // Handle higher-order pattern matching.