From 279e524c9e2abbc3b73b73c7a29407fa2e3d2457 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 28 Jul 2013 23:11:35 -0700
Subject: [PATCH] Fix bug in universe levels

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/environment.cpp | 21 +++++++++++----------
 1 file changed, 11 insertions(+), 10 deletions(-)

diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp
index 34a82b9e6..a54ae47d7 100644
--- a/src/kernel/environment.cpp
+++ b/src/kernel/environment.cpp
@@ -82,15 +82,17 @@ struct environment::imp {
         lean_assert(v1 < num);
         lean_assert(v2 < num);
         std::vector<unsigned> & v1_dists = m_uvar_distances[v1];
-        v1_dists[v2] = d;
-        // update forward
-        std::vector<unsigned> & v2_dists = m_uvar_distances[v2];
-        for (uvar v3 = 0; v3 < num; v3++) {
-            if (v2_dists[v3] != uninit) {
-                lean_assert(v1 != v3);
-                unsigned d_v1_v3 = add(d, v2_dists[v3]);
-                if (v1_dists[v3] == uninit || d_v1_v3 >= v1_dists[v3])
-                    v1_dists[v3] = d_v1_v3;
+        if (v1_dists[v2] == uninit || d >= v1_dists[v2]) {
+            v1_dists[v2] = d;
+            // update forward
+            std::vector<unsigned> & v2_dists = m_uvar_distances[v2];
+            for (uvar v3 = 0; v3 < num; v3++) {
+                if (v2_dists[v3] != uninit) {
+                    lean_assert(v1 != v3);
+                    unsigned d_v1_v3 = add(d, v2_dists[v3]);
+                    if (v1_dists[v3] == uninit || d_v1_v3 >= v1_dists[v3])
+                        v1_dists[v3] = d_v1_v3;
+                }
             }
         }
     }
@@ -130,7 +132,6 @@ struct environment::imp {
                                   out << "\n";
                               }
                           }
-                          out << "\n";
                       });
     }