From 28dad944c57b006f5752225cf5d8066d5b274d40 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 20 Apr 2015 17:35:37 -0700
Subject: [PATCH] fix(library/unifier): cyclic assignment (?M <- ?M)

This was producing nonterminating behavior on example described at issue #489
---
 src/library/unifier.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp
index 0e3bb3b1c..3a9763908 100644
--- a/src/library/unifier.cpp
+++ b/src/library/unifier.cpp
@@ -1998,7 +1998,7 @@ struct unifier_fn {
         buffer<expr> lhs_args, rhs_args;
         expr ml = get_app_args(lhs, lhs_args);
         expr mr = get_app_args(rhs, rhs_args);
-        if (ml == mr) {
+        if (mlocal_name(ml) == mlocal_name(mr)) {
             discard(c);
             return true;
         }