From d38979f783416c3b2a3a608640b8cf1e243770d6 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 30 May 2017 10:57:59 -0700
Subject: [PATCH] fix(util/trie): compilation issue

See #1619
---
 src/util/trie.h | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/util/trie.h b/src/util/trie.h
index f1b690ceb..54d0695cd 100644
--- a/src/util/trie.h
+++ b/src/util/trie.h
@@ -66,7 +66,7 @@ class trie : public KeyCMP {
                 } else {
                     trie n1(*c1);
                     new_t1->m_children.erase(k);
-                    new_t1->m_children.insert(k, merge(n1.steal(), c2));
+                    new_t1->m_children.insert(k, trie::merge(n1.steal(), c2));
                 }
             });
         return new_t1;