From afaef63bfa3915c3b2cb41ab8798c124cecf976e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 24 Jan 2013 12:38:37 -0800
Subject: [PATCH] Fix compilation error when using gcc.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/muz_qe/tab_context.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/muz_qe/tab_context.cpp b/src/muz_qe/tab_context.cpp
index a2c7e6215..e8e524d6d 100644
--- a/src/muz_qe/tab_context.cpp
+++ b/src/muz_qe/tab_context.cpp
@@ -852,7 +852,7 @@ namespace tb {
                         var_ref v(m), w(m);
                         v = m.mk_var(i, vars[i]);
                         w = m.mk_var(j, vars[i]);
-                        m_S2.insert(v, 0, expr_offset(w, 0));
+                        m_S2.insert(v.get(), 0, expr_offset(w, 0));
                         change = true;
                     }
                     ++j;