From 2312f43443e1031d47dd6968123d9f2dfaee973a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 16 Jun 2014 13:00:13 -0700
Subject: [PATCH] fix(kernel/abstract): propagate tags when abstracting

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/abstract.cpp | 4 ++--
 src/kernel/expr.cpp     | 2 +-
 src/kernel/expr.h       | 2 ++
 3 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/src/kernel/abstract.cpp b/src/kernel/abstract.cpp
index 9766e79fa..9c5e63fa6 100644
--- a/src/kernel/abstract.cpp
+++ b/src/kernel/abstract.cpp
@@ -19,7 +19,7 @@ expr abstract(expr const & e, unsigned s, unsigned n, expr const * subst) {
                 while (i > 0) {
                     --i;
                     if (subst[i] == e)
-                        return some_expr(mk_var(offset + s + n - i - 1));
+                        return some_expr(copy_tag(e, mk_var(offset + s + n - i - 1)));
                 }
             }
             return none_expr();
@@ -36,7 +36,7 @@ expr abstract_p(expr const & e, unsigned n, expr const * s) {
                 while (i > 0) {
                     --i;
                     if (is_eqp(s[i], e))
-                        return some_expr(mk_var(offset + n - i - 1));
+                        return some_expr(copy_tag(e, mk_var(offset + n - i - 1)));
                 }
             }
             return none_expr();
diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index 030ffe514..43f26c85b 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -463,7 +463,7 @@ unsigned get_free_var_range(expr const & e) {
 bool operator==(expr const & a, expr const & b) { return expr_eq_fn()(a, b); }
 bool is_bi_equal(expr const & a, expr const & b) { return expr_eq_fn(true)(a, b); }
 
-static expr copy_tag(expr const & e, expr && new_e) {
+expr copy_tag(expr const & e, expr && new_e) {
     tag t = e.get_tag();
     if (t != nulltag)
         new_e.set_tag(t);
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index c91284cfe..70f0f6ac5 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -149,6 +149,8 @@ public:
                     expr const & a7, expr const & a8) const;
 };
 
+expr copy_tag(expr const & e, expr && new_e);
+
 // =======================================
 // Structural equality
 /** \brief Binder information is ignored in the following predicate */