From a7eb7edafbe549f49dd1ff6fd5f960a91dbcee6d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 3 Aug 2016 18:20:59 -0700
Subject: [PATCH] fix(library/metavar_util): assertion violation

---
 src/library/metavar_util.h | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/library/metavar_util.h b/src/library/metavar_util.h
index 4c111e9578..e73d963c2e 100644
--- a/src/library/metavar_util.h
+++ b/src/library/metavar_util.h
@@ -69,6 +69,8 @@ bool has_assigned(CTX const & ctx, expr const & e) {
                 found = true;
                 return false; // stop search
             }
+            if (is_metavar(e))
+                return false; // do not search type
             return true; // continue search
         });
     return found;