From d1fe1286c078c1ed52ec71d20e5ad4135eaacc82 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 27 Jul 2014 17:16:30 -0700
Subject: [PATCH] fix(library/unifier): bug introduced today in
 consume_tc_cnstrs

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

diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp
index 50f3e465c..763c29790 100644
--- a/src/library/unifier.cpp
+++ b/src/library/unifier.cpp
@@ -1382,15 +1382,15 @@ struct unifier_fn {
     }
 
     void consume_tc_cnstrs() {
-        for (unsigned i = 0; i < 2; i++) {
-            while (true) {
-                if (in_conflict())
-                    return;
-                if (auto c = m_tc[i]->next_cnstr()) {
-                    process_constraint(*c);
-                } else {
-                    break;
-                }
+        while (true) {
+            if (in_conflict()) {
+                return;
+            } else if (auto c = m_tc[0]->next_cnstr()) {
+                process_constraint(*c);
+            } else if (auto c = m_tc[1]->next_cnstr()) {
+                process_constraint(*c);
+            } else {
+                break;
             }
         }
     }
@@ -1431,6 +1431,8 @@ struct unifier_fn {
     /** \brief Process the next constraint in the constraint queue m_cnstrs */
     bool process_next() {
         lean_assert(!m_cnstrs.empty());
+        lean_assert(!m_tc[0]->next_cnstr());
+        lean_assert(!m_tc[1]->next_cnstr());
         constraint c = m_cnstrs.min()->first;
         m_cnstrs.erase_min();
         if (is_choice_cnstr(c)) {