diff --git a/src/library/compiler/emit_bytecode.cpp b/src/library/compiler/emit_bytecode.cpp
index 798f3204ab..3c244fa0d4 100644
--- a/src/library/compiler/emit_bytecode.cpp
+++ b/src/library/compiler/emit_bytecode.cpp
@@ -166,6 +166,17 @@ class emit_bytecode_fn {
         emit(mk_constructor_instr(cidx, get_app_num_args(e)));
     }
 
+    void compile_reuse(expr const & e, unsigned bpz, name_map<unsigned> const & m) {
+        buffer<expr> args;
+        expr const & fn = get_app_args(e, args);
+        lean_assert(is_llnf_reuse(fn));
+        unsigned cidx, ssz;
+        is_llnf_reuse(fn, cidx, ssz);
+        if (ssz != 0) throw_no_unboxed_support();
+        compile_args(args.size(), args.data(), bpz, m);
+        emit(mk_reuse_instr(cidx, get_app_num_args(e) - 1));
+    }
+
     void compile_external(name const & n, buffer<expr> & args, unsigned bpz, name_map<unsigned> const & m) {
         // Not sure if this is the best approach, trying to lazy load the required
         // dynamic libraries.
@@ -208,34 +219,13 @@ class emit_bytecode_fn {
         emit(mk_proj_instr(idx));
     }
 
-    void compile_updt(expr const & e, unsigned bpz, name_map<unsigned> const & m) {
-        expr fn = app_fn(app_fn(e));
-        expr s  = app_arg(app_fn(e));
-        expr v  = app_arg(e);
-        unsigned idx;
-        is_llnf_updt(fn, idx);
-        compile(s, bpz, m);
-        bpz++;
-        compile(v, bpz, m);
-        emit(mk_updt_instr(idx));
-    }
-
-    void compile_updt_cidx(expr const & e, unsigned bpz, name_map<unsigned> const & m) {
-        expr fn = app_fn(e);
-        expr s  = app_arg(e);
-        unsigned idx;
-        is_llnf_updt_cidx(fn, idx);
-        compile(s, bpz, m);
-        emit(mk_updt_cidx_instr(idx));
-    }
-
     void compile_reset(expr const & e, unsigned bpz, name_map<unsigned> const & m) {
         expr fn = app_fn(e);
         expr s  = app_arg(e);
-        unsigned idx;
-        is_llnf_reset(fn, idx);
+        unsigned n;
+        is_llnf_reset(fn, n);
         compile(s, bpz, m);
-        emit(mk_reset_instr(idx));
+        emit(mk_reset_instr(n));
     }
 
     void compile_app(expr const & e, unsigned bpz, name_map<unsigned> const & m) {
@@ -244,12 +234,10 @@ class emit_bytecode_fn {
             compile_cases_on(e, bpz, m);
         } else if (is_llnf_cnstr(fn)) {
             compile_cnstr(e, bpz, m);
+        } else if (is_llnf_reuse(fn)) {
+            compile_reuse(e, bpz, m);
         } else if (is_llnf_proj(fn)) {
             compile_proj(e, bpz, m);
-        } else if (is_llnf_updt(fn)) {
-            compile_updt(e, bpz, m);
-        } else if (is_llnf_updt_cidx(fn)) {
-            compile_updt_cidx(e, bpz, m);
         } else if (is_llnf_reset(fn)) {
             compile_reset(e, bpz, m);
         } else if (is_sorry(e)) {
diff --git a/src/library/compiler/llnf.cpp b/src/library/compiler/llnf.cpp
index 19631ec376..bb00c5b247 100644
--- a/src/library/compiler/llnf.cpp
+++ b/src/library/compiler/llnf.cpp
@@ -17,6 +17,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 static name * g_cnstr     = nullptr;
+static name * g_reuse     = nullptr;
 static name * g_reset     = nullptr;
 static name * g_updt      = nullptr;
 static name * g_updt_cidx = nullptr;
@@ -52,14 +53,11 @@ static bool is_llnf_binary_primitive(expr const & e, name const & prefix, unsign
 expr mk_llnf_cnstr(unsigned cidx, unsigned scalar_sz) { return mk_constant(name(name(*g_cnstr, cidx), scalar_sz)); }
 bool is_llnf_cnstr(expr const & e, unsigned & cidx, unsigned & ssz) { return is_llnf_binary_primitive(e, *g_cnstr, cidx, ssz); }
 
-expr mk_llnf_reset(unsigned i) { return mk_constant(name(*g_reset, i)); }
-bool is_llnf_reset(expr const & e, unsigned & i) { return is_llnf_unary_primitive(e, *g_reset, i); }
+expr mk_llnf_reuse(unsigned cidx, unsigned scalar_sz) { return mk_constant(name(name(*g_reuse, cidx), scalar_sz)); }
+bool is_llnf_reuse(expr const & e, unsigned & cidx, unsigned & ssz) { return is_llnf_binary_primitive(e, *g_reuse, cidx, ssz); }
 
-expr mk_llnf_updt(unsigned i) { return mk_constant(name(*g_updt, i)); }
-bool is_llnf_updt(expr const & e, unsigned & i) { return is_llnf_unary_primitive(e, *g_updt, i); }
-
-expr mk_llnf_updt_cidx(unsigned cidx) { return mk_constant(name(*g_updt_cidx, cidx)); }
-bool is_llnf_updt_cidx(expr const & e, unsigned & cidx) { return is_llnf_unary_primitive(e, *g_updt_cidx, cidx); }
+expr mk_llnf_reset(unsigned n) { return mk_constant(name(*g_reset, n)); }
+bool is_llnf_reset(expr const & e, unsigned & n) { return is_llnf_unary_primitive(e, *g_reset, n); }
 
 expr mk_llnf_updt_u8(unsigned offset) { return mk_constant(name(*g_updt_u8, offset)); }
 bool is_llnf_updt_u8(expr const & e, unsigned & offset) { return is_llnf_unary_primitive(e, *g_updt_u8, offset); }
@@ -384,55 +382,22 @@ class to_llnf_fn {
         return mk_app(mk_llnf_reset(idx), major);
     }
 
-    expr mk_updt(expr const & major, unsigned idx, expr const & v) {
-        return mk_app(mk_llnf_updt(idx), major, v);
+    bool is_reuse_app(expr const & e) {
+        unsigned i, s;
+        return is_llnf_reuse(get_app_fn(e), i, s) && get_app_num_args(e) == 2;
     }
 
-    expr mk_updt_cidx(expr const & major, unsigned cidx) {
-        return mk_app(mk_llnf_updt_cidx(cidx), major);
-    }
-
-    bool is_updt_app(expr const & e) {
+    bool is_updt_scalar(expr const & e) {
         unsigned x;
-        return is_llnf_updt(get_app_fn(e), x) && get_app_num_args(e) == 2;
+        return
+            is_llnf_updt_u8(e, x) ||
+            is_llnf_updt_u16(e, x) ||
+            is_llnf_updt_u32(e, x) ||
+            is_llnf_updt_u64(e, x);
     }
 
-    bool is_updt_cidx_app(expr const & e) {
-        unsigned x;
-        return is_llnf_updt_cidx(get_app_fn(e), x) && get_app_num_args(e) == 1;
-    }
-
-    expr find(expr const & e) const {
-        if (is_fvar(e)) {
-            if (optional<local_decl> decl = m_lctx.find_local_decl(e)) {
-                optional<expr> v = decl->get_value();
-                if (v) return find(*v);
-            }
-        } else if (is_mdata(e)) {
-            return find(mdata_expr(e));
-        }
-        return e;
-    }
-
-    /* Return true if `a` is of the form `_proj.<idx> e` */
-    bool is_proj_of(expr a, expr const & e, unsigned idx) {
-        a = find(a);
-        unsigned a_idx;
-        return is_app(a) && is_llnf_proj(app_fn(a), a_idx) && a_idx == idx && app_arg(a) == e;
-    }
-
-    /* Return true if `a` is of the form `_proj_u<size>.<offset> e` */
-    bool is_scalar_proj_of(expr a, expr const & e, unsigned size, unsigned offset) {
-        a = find(a);
-        unsigned a_offset;
-        if (!is_app(a) || app_arg(a) != e) return false;
-        switch (size) {
-        case 1: return is_llnf_proj_u8(app_fn(a), a_offset) && a_offset == offset;
-        case 2: return is_llnf_proj_u16(app_fn(a), a_offset) && a_offset == offset;
-        case 4: return is_llnf_proj_u32(app_fn(a), a_offset) && a_offset == offset;
-        case 8: return is_llnf_proj_u64(app_fn(a), a_offset) && a_offset == offset;
-        }
-        return false;
+    bool is_updt_scalar_app(expr const & e) {
+        return is_updt_scalar(get_app_fn(e)) && get_app_num_args(e) == 1;
     }
 
     /* Auxiliary functor for replacing constructor applications with update operations. */
@@ -440,8 +405,6 @@ class to_llnf_fn {
         to_llnf_fn &         m_owner;
         expr const &         m_major;
         cnstr_info const &   m_cinfo;
-        /* `m_used_fields[i]` is true if the field `i` is used in the minor premise. */
-        buffer<bool> const & m_to_reset_fields;
         /* `m_major` may be replaced/reused many times in different branches, but we
            only have to reset fields once. */
         bool                 m_reset{false};
@@ -450,6 +413,32 @@ class to_llnf_fn {
 
         environment const & env() { return m_owner.env(); }
 
+        expr find(expr const & e) const {
+            if (is_fvar(e)) {
+                if (optional<local_decl> decl = m_owner.m_lctx.find_local_decl(e)) {
+                    optional<expr> v = decl->get_value();
+                    if (v) return find(*v);
+                }
+            } else if (is_mdata(e)) {
+                return find(mdata_expr(e));
+            }
+            return e;
+        }
+
+        /* Return true if `a` is of the form `_proj_u<size>.<offset> e` */
+        bool is_scalar_proj_of(expr a, expr const & e, unsigned size, unsigned offset) {
+            a = find(a);
+            unsigned a_offset;
+            if (!is_app(a) || app_arg(a) != e) return false;
+            switch (size) {
+            case 1: return is_llnf_proj_u8(app_fn(a), a_offset) && a_offset == offset;
+            case 2: return is_llnf_proj_u16(app_fn(a), a_offset) && a_offset == offset;
+            case 4: return is_llnf_proj_u32(app_fn(a), a_offset) && a_offset == offset;
+            case 8: return is_llnf_proj_u64(app_fn(a), a_offset) && a_offset == offset;
+            }
+            return false;
+        }
+
         expr visit_constructor(expr const & e) {
             buffer<expr> args;
             expr const & k = get_app_args(e, args);
@@ -465,62 +454,31 @@ class to_llnf_fn {
             }
             constructor_val k_val  = env().get(const_name(k)).to_constructor_val();
             unsigned nparams       = k_val.get_nparams();
-            /* See `mark_to_reset_fields` */
-            expr r;
             if (!m_reset) {
-                r               = m_major;
-                unsigned j      = nparams;
-                unsigned i      = 0;
-                unsigned idx    = 0;
-                for (field_info const & info : k_info.m_field_info) {
-                    lean_assert(j == i + nparams);
-                    if (info.m_kind == field_info::Object) {
-                        if (m_to_reset_fields[i]) {
-                            expr new_updt = m_owner.mk_reset(r, idx);
-                            r             = m_owner.mk_let_decl(mk_enf_object_type(), new_updt);
-                        }
-                        idx++;
-                    }
-                    i++;
-                    j++;
-                }
+                m_major_after_reset = m_owner.mk_reset(m_major, k_info.m_num_objs);
+                m_major_after_reset = m_owner.mk_let_decl(mk_enf_object_type(), m_major_after_reset);
                 m_reset             = true;
-                m_major_after_reset = r;
-            } else {
-                r = m_major_after_reset;
             }
+            expr r = m_major_after_reset;
             /* Remark: note that we do not create let-declarations here for the following updates.
                We will flatten them later when we visit the minor premise. */
-
-            /* Update constructor cidx if needed. */
-            if (k_info.m_cidx != m_cinfo.m_cidx) {
-                r = m_owner.mk_updt_cidx(r, k_info.m_cidx);
-            }
-            /* Update fields with new values. */
-            unsigned offset = k_info.m_num_objs * sizeof(void*);
+            buffer<expr> obj_args;
             unsigned j      = nparams;
-            unsigned i      = 0;
-            unsigned idx    = 0;
             for (field_info const & info : k_info.m_field_info) {
-                lean_assert(j == i + nparams);
-                switch (info.m_kind) {
-                case field_info::Irrelevant:
-                    break;
-                case field_info::Object:
-                    if (m_to_reset_fields[i] || !m_owner.is_proj_of(args[j], m_major, idx)) {
-                        r = m_owner.mk_updt(r, idx, args[j]);
-                    }
-                    idx++;
-                    break;
-                case field_info::Scalar:
-                    if (!m_owner.is_scalar_proj_of(args[j], m_major, info.m_size, offset)) {
+                if (info.m_kind == field_info::Object) {
+                    obj_args.push_back(args[j]);
+                }
+                j++;
+            }
+            r = mk_app(mk_app(mk_llnf_reuse(k_info.m_cidx, k_info.m_scalar_sz), r), obj_args);
+            unsigned offset = k_info.m_num_objs * sizeof(void*);
+            for (field_info const & info : k_info.m_field_info) {
+                if (info.m_kind == field_info::Scalar) {
+                    if (!is_scalar_proj_of(args[j], m_major, info.m_size, offset)) {
                         r = m_owner.mk_scalar_updt(r, info.m_size, offset, args[j]);
                     }
                     offset += info.m_size;
-                    break;
                 }
-                j++;
-                i++;
             }
             m_replaced = true;
             return r;
@@ -575,98 +533,16 @@ class to_llnf_fn {
         }
 
     public:
-        replace_cnstr_fn(to_llnf_fn & owner, expr const & major, cnstr_info const & cinfo, buffer<bool> const & to_reset_fields):
-            m_owner(owner), m_major(major), m_cinfo(cinfo), m_to_reset_fields(to_reset_fields) {}
+        replace_cnstr_fn(to_llnf_fn & owner, expr const & major, cnstr_info const & cinfo):
+            m_owner(owner), m_major(major), m_cinfo(cinfo) {}
         expr operator()(expr const & e) { return visit(e); }
     };
 
-    /* Auxiliary methods used to implement `try_update_opt`. We say a field needs to be reset at the beginning of a major
-       premise if it is used in a non tail call.
-       We "reset" the field to create new opportunites for destructive updates.
-       For example, consider the following sequence of instructions in low-level normal form without `reset` operations.
-       ```
-       map_add_1 :=
-       λ xs, @list.cases_on xs
-         _cnstr.0.0
-         (let _x_1 := _proj.0 xs,
-              _x_2 := _proj.1 xs,
-              _x_5 := nat.add _x_1 1,
-              _x_6 := map_add_1 _x_2,
-              _x_7 := _updt.0 xs _x_5
-              in _updt.1 _x_7 _x_6)
-       ```
-       After the instruction `_x_2 := _proj.1 xs`, there are at least two references to the tail of `xs`: `_x_2` and the one
-       on `xs`. So, the recursive call `map_add_1 _x_2` will not be able to perform destructive updates.
-       Now consider the version that uses `reset` operations.
-       ```
-       map_add_1 :=
-       λ xs, @list.cases_on xs
-         _cnstr.0.0
-         (let _x_1 := _proj.0 xs,
-              _x_2 := _proj.1 xs,
-              _x_3 := _reset.0 xs,
-              _x_4 := _reset.1 _x_3,
-              _x_5 := nat.add _x_1 1,
-              _x_6 := map_add_1 _x_2,
-              _x_7 := _updt.0 _x_4_x_5
-              in _updt.1 _x_7 _x_6)
-       ```
-       The reset operations will decrease the reference counter of `xs` head and tail.
-       Note that the operation `_x_3 := _reset.0 xs` is wasteful since `nat.add` never performs destructive updates.
-       In the future, we may consider a better `mark_to_reset_fields` that avoids these unnecessary reset operations.
-
-       Remark: `reset` operations may also help to reduce memory contention.
-    */
-    void mark_to_reset_fields(expr const & e0, buffer<expr> const & fields, buffer<bool> & result) {
-        buffer<pair<expr, bool>> todo;
-        todo.emplace_back(e0, true);
-        expr e; bool tail;
-        while (!todo.empty()) {
-            std::tie(e, tail) = todo.back();
-            todo.pop_back();
-            if (!has_fvar(e))
-                continue;
-            switch (e.kind()) {
-            case expr_kind::FVar:
-                if (!tail) {
-                    for (unsigned i = 0; i < fields.size(); i++) {
-                        if (is_fvar(fields[i]) && e == fields[i])
-                            result[i] = true;
-                    }
-                }
-                break;
-            case expr_kind::Let:
-                todo.emplace_back(let_body(e), tail);
-                todo.emplace_back(let_value(e), false);
-                break;
-            case expr_kind::Lambda:
-                todo.emplace_back(binding_body(e), tail);
-                break;
-            case expr_kind::Proj:
-                todo.emplace_back(proj_expr(e), tail);
-                break;
-            case expr_kind::App: {
-                buffer<expr> args;
-                expr const & fn = get_app_args(e, args);
-                todo.emplace_back(fn, tail);
-                for (expr const & arg : args)
-                    todo.emplace_back(arg, tail);
-                break;
-            }
-            default:
-                break;
-            }
-        }
-    }
-
-    expr try_update_opt(expr const & minor, expr const & major, cnstr_info const & cinfo, buffer<expr> const & fields) {
+    expr try_update_opt(expr const & minor, expr const & major, cnstr_info const & cinfo) {
         if (cinfo.m_num_objs == 0 && cinfo.m_scalar_sz == 0) return minor;
         if (!is_fvar(major)) return minor;
         if (has_fvar(minor, major)) return minor;
-        buffer<bool> to_reset_fields;
-        to_reset_fields.resize(fields.size(), false);
-        mark_to_reset_fields(minor, fields, to_reset_fields);
-        return replace_cnstr_fn(*this, major, cinfo, to_reset_fields)(minor);
+        return replace_cnstr_fn(*this, major, cinfo)(minor);
     }
 
     expr visit_cases(expr const & e) {
@@ -724,7 +600,7 @@ class to_llnf_fn {
                 minor = binding_body(minor);
             }
             minor     = instantiate_rev(minor, fields.size(), fields.data());
-            minor     = try_update_opt(minor, major, cinfo, fields);
+            minor     = try_update_opt(minor, major, cinfo);
             minor     = visit(minor);
             if (!is_enf_unreachable(minor)) {
                 /* If `minor` is not the constructor `i`, then this "cases_on" application is not the identity. */
@@ -869,9 +745,9 @@ class to_llnf_fn {
             return visit_cases(e);
         } else if (is_constructor_app(env(), e)) {
             return visit_constructor(e);
-        } else if (is_updt_app(e)) {
+        } else if (is_updt_scalar_app(e)) {
             return flat_app(e);
-        } else if (is_updt_cidx_app(e)) {
+        } else if (is_reuse_app(e)) {
             return flat_app(e);
         } else {
             return visit_app_default(e);
@@ -906,6 +782,7 @@ expr to_llnf(environment const & env, expr const & e, bool unboxed) {
 
 void initialize_llnf() {
     g_cnstr     = new name("_cnstr");
+    g_reuse     = new name("_reuse");
     g_reset     = new name("_reset");
     g_updt      = new name("_updt");
     g_updt_cidx = new name("_updt_cidx");
@@ -927,6 +804,7 @@ void initialize_llnf() {
 
 void finalize_llnf() {
     delete g_cnstr;
+    delete g_reuse;
     delete g_reset;
     delete g_updt;
     delete g_updt_u8;
diff --git a/src/library/compiler/llnf.h b/src/library/compiler/llnf.h
index a3c7533307..4c72d773e7 100644
--- a/src/library/compiler/llnf.h
+++ b/src/library/compiler/llnf.h
@@ -13,16 +13,14 @@ namespace lean {
 expr to_llnf(environment const & env, expr const & e, bool unboxed_data = false);
 
 bool is_llnf_cnstr(expr const & e, unsigned & cidx, unsigned & ssz);
-bool is_llnf_reset(expr const & e, unsigned & i);
+bool is_llnf_reuse(expr const & e, unsigned & cidx, unsigned & ssz);
+bool is_llnf_reset(expr const & e, unsigned & n);
 bool is_llnf_proj(expr const & e, unsigned & idx);
-bool is_llnf_updt(expr const & e, unsigned & i);
-bool is_llnf_updt_cidx(expr const & e, unsigned & cidx);
 
 inline bool is_llnf_cnstr(expr const & e) { unsigned d1, d2; return is_llnf_cnstr(e, d1, d2); }
+inline bool is_llnf_reuse(expr const & e) { unsigned d1, d2; return is_llnf_reuse(e, d1, d2); }
 inline bool is_llnf_reset(expr const & e) { unsigned i; return is_llnf_reset(e, i); }
 inline bool is_llnf_proj(expr const & e) { unsigned d; return is_llnf_proj(e, d); }
-inline bool is_llnf_updt(expr const & e) { unsigned i; return is_llnf_updt(e, i); }
-inline bool is_llnf_updt_cidx(expr const & e) { unsigned i; return is_llnf_updt_cidx(e, i); }
 
 void initialize_llnf();
 void finalize_llnf();
diff --git a/src/library/vm/optimize.cpp b/src/library/vm/optimize.cpp
index 614e50db09..e30151e1da 100644
--- a/src/library/vm/optimize.cpp
+++ b/src/library/vm/optimize.cpp
@@ -102,7 +102,7 @@ class live_vars_fn {
         case opcode::Proj: case opcode::Apply: case opcode::InvokeGlobal:
         case opcode::InvokeBuiltin: case opcode::InvokeCFun:
         case opcode::Closure: case opcode::Expr: case opcode::LocalInfo:
-        case opcode::Reset: case opcode::Updt: case opcode::UpdtCidx:
+        case opcode::Reset: case opcode::Reuse:
             s = collect(pc+1);
             break;
         case opcode::Push: case opcode::Move:
diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp
index 0d94d8ae34..417f3e8e67 100644
--- a/src/library/vm/vm.cpp
+++ b/src/library/vm/vm.cpp
@@ -525,14 +525,13 @@ void vm_instr::display(std::ostream & out) const {
     switch (m_op) {
     case opcode::Push:          out << "push " << m_idx; break;
     case opcode::Move:          out << "move " << m_idx; break;
-    case opcode::Reset:         out << "reset " << m_idx; break;
-    case opcode::Updt:          out << "updt " << m_idx; break;
-    case opcode::UpdtCidx:      out << "updt_cidx " << m_idx; break;
+    case opcode::Reset:         out << "reset " << m_num; break;
     case opcode::Ret:           out << "ret"; break;
     case opcode::Drop:          out << "drop " << m_num; break;
     case opcode::Goto:          out << "goto " << m_pc[0]; break;
     case opcode::SConstructor:  out << "scnstr #" << m_cidx; break;
     case opcode::Constructor:   out << "cnstr #" << m_cidx << " " << m_nfields; break;
+    case opcode::Reuse:         out << "reuse #" << m_cidx << " " << m_nfields; break;
     case opcode::Num:           out << "num " << *m_mpz; break;
     case opcode::String:        out << "str_lit \"" << *m_str << "\""; break;
     case opcode::Unreachable:   out << "unreachable"; break;
@@ -621,21 +620,9 @@ vm_instr mk_move_instr(unsigned idx) {
     return r;
 };
 
-vm_instr mk_reset_instr(unsigned idx) {
+vm_instr mk_reset_instr(unsigned n) {
     vm_instr r(opcode::Reset);
-    r.m_idx = idx;
-    return r;
-};
-
-vm_instr mk_updt_instr(unsigned idx) {
-    vm_instr r(opcode::Updt);
-    r.m_idx = idx;
-    return r;
-};
-
-vm_instr mk_updt_cidx_instr(unsigned idx) {
-    vm_instr r(opcode::UpdtCidx);
-    r.m_idx = idx;
+    r.m_num = n;
     return r;
 };
 
@@ -670,6 +657,13 @@ vm_instr mk_constructor_instr(unsigned cidx, unsigned nfields) {
     return r;
 }
 
+vm_instr mk_reuse_instr(unsigned cidx, unsigned nfields) {
+    vm_instr r(opcode::Reuse);
+    r.m_cidx    = cidx;
+    r.m_nfields = nfields;
+    return r;
+}
+
 vm_instr mk_num_instr(mpz const & v) {
     if (v < LEAN_VM_MAX_SMALL_NAT) {
         vm_instr r(opcode::SConstructor);
@@ -781,10 +775,9 @@ void vm_instr::copy_args(vm_instr const & i) {
         m_nargs  = i.m_nargs;
         break;
     case opcode::Push:  case opcode::Move: case opcode::Proj:
-    case opcode::Reset: case opcode::Updt: case opcode::UpdtCidx:
         m_idx  = i.m_idx;
         break;
-    case opcode::Drop:
+    case opcode::Drop: case opcode::Reset:
         m_num = i.m_num;
         break;
     case opcode::Goto:
@@ -802,7 +795,7 @@ void vm_instr::copy_args(vm_instr const & i) {
     case opcode::SConstructor:
         m_cidx = i.m_cidx;
         break;
-    case opcode::Constructor:
+    case opcode::Constructor: case opcode::Reuse:
         m_cidx    = i.m_cidx;
         m_nfields = i.m_nfields;
         break;
@@ -895,10 +888,9 @@ void vm_instr::serialize(serializer & s, std::function<name(unsigned)> const & i
         s << idx2name(m_fn_idx) << m_nargs;
         break;
     case opcode::Push:  case opcode::Move: case opcode::Proj:
-    case opcode::Reset: case opcode::Updt: case opcode::UpdtCidx:
         s << m_idx;
         break;
-    case opcode::Drop:
+    case opcode::Drop: case opcode::Reset:
         s << m_num;
         break;
     case opcode::Goto:
@@ -916,7 +908,7 @@ void vm_instr::serialize(serializer & s, std::function<name(unsigned)> const & i
     case opcode::SConstructor:
         s << m_cidx;
         break;
-    case opcode::Constructor:
+    case opcode::Constructor: case opcode::Reuse:
         s << m_cidx << m_nfields;
         break;
     case opcode::Num:
@@ -968,10 +960,6 @@ static vm_instr read_vm_instr(deserializer & d) {
         return mk_move_instr(d.read_unsigned());
     case opcode::Reset:
         return mk_reset_instr(d.read_unsigned());
-    case opcode::Updt:
-        return mk_updt_instr(d.read_unsigned());
-    case opcode::UpdtCidx:
-        return mk_updt_cidx_instr(d.read_unsigned());
     case opcode::Proj:
         return mk_proj_instr(d.read_unsigned());
     case opcode::Drop:
@@ -991,6 +979,9 @@ static vm_instr read_vm_instr(deserializer & d) {
     case opcode::Constructor:
         idx = d.read_unsigned();
         return mk_constructor_instr(idx, d.read_unsigned());
+    case opcode::Reuse:
+        idx = d.read_unsigned();
+        return mk_reuse_instr(idx, d.read_unsigned());
     case opcode::Num:
         return mk_num_instr(d.read_mpz());
     case opcode::String:
@@ -2848,54 +2839,22 @@ void vm_state::run() {
             goto main_loop;
         }
         case opcode::Reset: {
-            /* Instruction: reset idx
+            /* Instruction: reset n
 
                stack before,   after
                ...           ...
-               s             s'  (s.idx := ())
+               s             s'
             */
-            unsigned idx = instr.get_idx();
+            unsigned n = instr.get_num();
             vm_obj & s = m_stack.back();
             if (s.raw()->get_rc() > 1) {
-                s = mk_vm_constructor(cidx(s), csize(s), cfields(s));
+                s = mk_vm_simple(0);
+            } else {
+                vm_obj * fields = const_cast<vm_obj*>(to_composite(s)->fields());
+                for (unsigned i = 0; i < n; i++) {
+                    fields[i] = mk_vm_simple(0);
+                }
             }
-            const_cast<vm_obj*>(to_composite(s)->fields())[idx] = mk_vm_simple(0);
-            m_pc++;
-            goto main_loop;
-        }
-        case opcode::Updt: {
-            /* Instruction: updt idx
-
-               stack before,   after
-               ...           ...
-               s             s'  (s.idx := v)
-               v       ==>
-            */
-            unsigned idx = instr.get_idx();
-            unsigned sz  = m_stack.size();
-            vm_obj & s   = m_stack[sz-2];
-            vm_obj & v   = m_stack[sz-1];
-            if (s.raw()->get_rc() > 1) {
-                s = mk_vm_constructor(cidx(s), csize(s), cfields(s));
-            }
-            std::swap(const_cast<vm_obj*>(to_composite(s)->fields())[idx], v);
-            m_stack.pop_back();
-            m_pc++;
-            goto main_loop;
-        }
-        case opcode::UpdtCidx: {
-            /* Instruction: updt_cidx cidx
-
-               stack before,   after
-               ...           ...
-               s       ==>   s'  (s.cidx := cidx)
-            */
-            unsigned idx = instr.get_idx();
-            vm_obj & s    = m_stack.back();
-            if (s.raw()->get_rc() > 1) {
-                s = mk_vm_constructor(cidx(s), csize(s), cfields(s));
-            }
-            const_cast<vm_composite*>(to_composite(s))->m_idx = idx;
             m_pc++;
             goto main_loop;
         }
@@ -2933,7 +2892,37 @@ void vm_state::run() {
             vm_obj new_value = mk_vm_constructor(instr.get_cidx(), nfields, m_stack.data() + sz - nfields);
             m_stack.resize(sz - nfields + 1);
             swap(m_stack.back(), new_value);
-            if (m_debugging) shrink_stack_info();
+            m_pc++;
+            goto main_loop;
+        }
+        case opcode::Reuse: {
+            /** Instruction: reuse i n
+
+                stack before,      after
+                ...                ...
+                v      ==>         v
+                cell               (#i a_1 ... a_n)
+                a_1
+                ...
+                a_n
+            */
+            unsigned nfields   = instr.get_nfields();
+            unsigned sz        = m_stack.size();
+            lean_vm_check(nfields + 1 <= sz);
+            vm_obj & cell      = m_stack[sz - nfields - 1];
+            vm_obj * src       = m_stack.data() + sz - nfields;
+            if (is_simple(cell)) {
+                vm_obj new_value = mk_vm_constructor(instr.get_cidx(), nfields, src);
+                m_stack.resize(sz - nfields);
+                swap(m_stack.back(), new_value);
+            } else {
+                const_cast<vm_composite*>(to_composite(cell))->m_idx = instr.get_cidx();
+                vm_obj * fields = const_cast<vm_obj*>(to_composite(cell)->fields());
+                for (unsigned i = 0; i < nfields; i++) {
+                    swap(fields[i], src[i]);
+                }
+                m_stack.resize(sz - nfields);
+            }
             m_pc++;
             goto main_loop;
         }
diff --git a/src/library/vm/vm.h b/src/library/vm/vm.h
index 8ec2edc670..e718a57196 100644
--- a/src/library/vm/vm.h
+++ b/src/library/vm/vm.h
@@ -315,7 +315,7 @@ enum class opcode {
     Cases2, CasesN, Proj,
     Apply, InvokeGlobal, InvokeBuiltin, InvokeCFun,
     Closure, Unreachable, Expr, LocalInfo,
-    Reset, Updt, UpdtCidx
+    Reset, Reuse
 };
 
 /** \brief VM instructions */
@@ -326,9 +326,9 @@ class vm_instr {
             unsigned m_fn_idx;  /* InvokeGlobal, InvokeBuiltin, InvokeCFun and Closure. */
             unsigned m_nargs;   /* Closure */
         };
-        /* Push, Move, Proj, Reset, Updt, UpdtCidx */
+        /* Push, Move, Proj */
         unsigned m_idx;
-        /* Drop */
+        /* Drop, Reset */
         unsigned m_num;
         /* Goto and Cases2 */
         struct {
@@ -338,10 +338,10 @@ class vm_instr {
         struct {
             unsigned * m_npcs;
         };
-        /* Constructor, SConstructor */
+        /* Constructor, SConstructor, Reuse */
         struct {
             unsigned m_cidx;
-            unsigned m_nfields; /* only used by Constructor */
+            unsigned m_nfields; /* only used by Constructor and Reuse */
         };
         /* Num */
         mpz * m_mpz;
@@ -363,6 +363,7 @@ class vm_instr {
     friend vm_instr mk_goto_instr(unsigned pc);
     friend vm_instr mk_sconstructor_instr(unsigned cidx);
     friend vm_instr mk_constructor_instr(unsigned cidx, unsigned nfields);
+    friend vm_instr mk_reuse_instr(unsigned cidx, unsigned nfields);
     friend vm_instr mk_num_instr(mpz const & v);
     friend vm_instr mk_string_instr(std::string const & v);
     friend vm_instr mk_ret_instr();
@@ -376,9 +377,7 @@ class vm_instr {
     friend vm_instr mk_closure_instr(unsigned fn_idx, unsigned n);
     friend vm_instr mk_expr_instr(expr const &e);
     friend vm_instr mk_local_info_instr(unsigned idx, name const & n, optional<expr> const & e);
-    friend vm_instr mk_updt_instr(unsigned idx);
-    friend vm_instr mk_reset_instr(unsigned idx);
-    friend vm_instr mk_updt_cidx_instr(unsigned cidx);
+    friend vm_instr mk_reset_instr(unsigned n);
 
     void release_memory();
     void copy_args(vm_instr const & i);
@@ -406,13 +405,12 @@ public:
     }
 
     unsigned get_idx() const {
-        lean_assert(m_op == opcode::Push || m_op == opcode::Move || m_op == opcode::Proj ||
-                    m_op == opcode::Reset || m_op == opcode::Updt || m_op == opcode::UpdtCidx);
+        lean_assert(m_op == opcode::Push || m_op == opcode::Move || m_op == opcode::Proj);
         return m_idx;
     }
 
     unsigned get_num() const {
-        lean_assert(m_op == opcode::Drop);
+        lean_assert(m_op == opcode::Drop || m_op == opcode::Reset);
         return m_num;
     }
 
@@ -456,12 +454,12 @@ public:
     }
 
     unsigned get_cidx() const {
-        lean_assert(m_op == opcode::Constructor || m_op == opcode::SConstructor);
+        lean_assert(m_op == opcode::Constructor || m_op == opcode::SConstructor || m_op == opcode::Reuse);
         return m_cidx;
     }
 
     unsigned get_nfields() const {
-        lean_assert(m_op == opcode::Constructor);
+        lean_assert(m_op == opcode::Constructor || m_op == opcode::Reuse);
         return m_nfields;
     }
 
@@ -506,6 +504,7 @@ vm_instr mk_proj_instr(unsigned n);
 vm_instr mk_goto_instr(unsigned pc);
 vm_instr mk_sconstructor_instr(unsigned cidx);
 vm_instr mk_constructor_instr(unsigned cidx, unsigned nfields);
+vm_instr mk_reuse_instr(unsigned cidx, unsigned nfields);
 vm_instr mk_num_instr(mpz const & v);
 vm_instr mk_string_instr(std::string const & v);
 vm_instr mk_ret_instr();
@@ -519,9 +518,7 @@ vm_instr mk_invoke_builtin_instr(unsigned fn_idx);
 vm_instr mk_closure_instr(unsigned fn_idx, unsigned n);
 vm_instr mk_expr_instr(expr const &e);
 vm_instr mk_local_info_instr(unsigned idx, name const & n, optional<expr> const & e);
-vm_instr mk_reset_instr(unsigned idx);
-vm_instr mk_updt_instr(unsigned idx);
-vm_instr mk_updt_cidx_instr(unsigned cidx);
+vm_instr mk_reset_instr(unsigned n);
 
 class vm_state;
 class vm_instr;