fix(kernel/abstract): propagate tags when abstracting

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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();

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);

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 */