diff --git a/regression/cbmc-cpp/cpp1/test.desc b/regression/cbmc-cpp/cpp1/test.desc
index 7ad0d9caff4..e6c5f4f102d 100644
--- a/regression/cbmc-cpp/cpp1/test.desc
+++ b/regression/cbmc-cpp/cpp1/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.cpp
-
+--unwind 1 --unwinding-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/src/cpp/cpp_declarator_converter.cpp b/src/cpp/cpp_declarator_converter.cpp
index 4f58318c421..1991c280556 100644
--- a/src/cpp/cpp_declarator_converter.cpp
+++ b/src/cpp/cpp_declarator_converter.cpp
@@ -104,10 +104,15 @@ symbolt &cpp_declarator_convertert::convert(
     {
       // adjust type if it's a non-static member function
       if(final_type.id()==ID_code)
+      {
+        cpp_save_scopet save_scope(cpp_typecheck.cpp_scopes);
+        cpp_typecheck.cpp_scopes.go_to(*scope);
+
         cpp_typecheck.add_this_to_method_type(
           cpp_typecheck.lookup(scope->identifier),
           to_code_type(final_type),
           method_qualifier);
+      }
 
       get_final_identifier();
 
diff --git a/src/cpp/cpp_typecheck.cpp b/src/cpp/cpp_typecheck.cpp
index bd76880f14d..e8163e38270 100644
--- a/src/cpp/cpp_typecheck.cpp
+++ b/src/cpp/cpp_typecheck.cpp
@@ -54,10 +54,10 @@ void cpp_typecheckt::typecheck()
   for(auto &item : cpp_parse_tree.items)
     convert(item);
 
-  typecheck_method_bodies();
-
   static_and_dynamic_initialization();
 
+  typecheck_method_bodies();
+
   do_not_typechecked();
 
   clean_up();
@@ -276,13 +276,10 @@ void cpp_typecheckt::clean_up()
 
     const symbolt &symbol=cur_it->second;
 
-    // erase templates
-    if(symbol.type.get_bool(ID_is_template) ||
-       // Remove all symbols that have not been converted.
-       //   In particular this includes symbols created for functions
-       //   during template instantiation that are never called,
-       //   and hence, their bodies have not been converted.
-       contains_cpp_name(symbol.value))
+    // erase templates and all member functions that have not been converted
+    if(
+      symbol.type.get_bool(ID_is_template) ||
+      deferred_typechecking.find(symbol.name) != deferred_typechecking.end())
     {
       symbol_table.erase(cur_it);
       continue;
diff --git a/src/cpp/cpp_typecheck.h b/src/cpp/cpp_typecheck.h
index a66b92f3481..05b040c158b 100644
--- a/src/cpp/cpp_typecheck.h
+++ b/src/cpp/cpp_typecheck.h
@@ -12,10 +12,10 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #ifndef CPROVER_CPP_CPP_TYPECHECK_H
 #define CPROVER_CPP_CPP_TYPECHECK_H
 
-#include <cassert>
-#include <set>
 #include <list>
 #include <map>
+#include <set>
+#include <unordered_set>
 
 #include <util/std_code.h>
 #include <util/std_types.h>
@@ -257,7 +257,7 @@ class cpp_typecheckt:public c_typecheck_baset
 
   void default_dtor(const symbolt &symb, cpp_declarationt &dtor);
 
-  codet dtor(const symbolt &symb);
+  codet dtor(const symbolt &symb, const symbol_exprt &this_expr);
 
   void check_member_initializers(
     const struct_typet::basest &bases,
@@ -588,6 +588,7 @@ class cpp_typecheckt:public c_typecheck_baset
   typedef std::list<irep_idt> dynamic_initializationst;
   dynamic_initializationst dynamic_initializations;
   bool disable_access_control;           // Disable protect and private
+  std::unordered_set<irep_idt> deferred_typechecking;
 };
 
 #endif // CPROVER_CPP_CPP_TYPECHECK_H
diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp
index d9e0fe6fa85..e21d2625ffc 100644
--- a/src/cpp/cpp_typecheck_compound_type.cpp
+++ b/src/cpp/cpp_typecheck_compound_type.cpp
@@ -1335,8 +1335,7 @@ void cpp_typecheckt::typecheck_member_function(
   // Is this in a class template?
   // If so, we defer typechecking until used.
   if(cpp_scopes.current_scope().get_parent().is_template_scope())
-  {
-  }
+    deferred_typechecking.insert(new_symbol->name);
   else // remember for later typechecking of body
     add_method_body(new_symbol);
 }
@@ -1360,9 +1359,11 @@ void cpp_typecheckt::add_this_to_method_type(
     subtype.set(ID_C_volatile, true);
 
   code_typet::parametert parameter(pointer_type(subtype));
-  parameter.set_identifier(ID_this); // check? Not qualified
+  parameter.set_identifier(ID_this);
   parameter.set_base_name(ID_this);
   parameter.set_this();
+  if(!cpp_scopes.current_scope().get_parent().is_template_scope())
+    convert_parameter(compound_symbol.mode, parameter);
 
   code_typet::parameterst &parameters = type.parameters();
   parameters.insert(parameters.begin(), parameter);
diff --git a/src/cpp/cpp_typecheck_conversions.cpp b/src/cpp/cpp_typecheck_conversions.cpp
index 2376f86d7f2..0cac0be741a 100644
--- a/src/cpp/cpp_typecheck_conversions.cpp
+++ b/src/cpp/cpp_typecheck_conversions.cpp
@@ -576,15 +576,13 @@ bool cpp_typecheckt::standard_conversion_pointer_to_member(
       code_typet code1=to_code_type(expr.type().subtype());
       assert(!code1.parameters().empty());
       code_typet::parametert this1=code1.parameters()[0];
-      INVARIANT(
-        this1.get_base_name() == ID_this, "first parameter should be `this'");
+      INVARIANT(this1.get_this(), "first parameter should be `this'");
       code1.parameters().erase(code1.parameters().begin());
 
       code_typet code2=to_code_type(type.subtype());
       assert(!code2.parameters().empty());
       code_typet::parametert this2=code2.parameters()[0];
-      INVARIANT(
-        this2.get_base_name() == ID_this, "first parameter should be `this'");
+      INVARIANT(this2.get_this(), "first parameter should be `this'");
       code2.parameters().erase(code2.parameters().begin());
 
       if(this2.type().subtype().get_bool(ID_C_constant) &&
diff --git a/src/cpp/cpp_typecheck_destructor.cpp b/src/cpp/cpp_typecheck_destructor.cpp
index d7e097a564f..d90ccc54a45 100644
--- a/src/cpp/cpp_typecheck_destructor.cpp
+++ b/src/cpp/cpp_typecheck_destructor.cpp
@@ -47,7 +47,7 @@ void cpp_typecheckt::default_dtor(
 }
 
 /// produces destructor code for a class object
-codet cpp_typecheckt::dtor(const symbolt &symbol)
+codet cpp_typecheckt::dtor(const symbolt &symbol, const symbol_exprt &this_expr)
 {
   assert(symbol.type.id()==ID_struct ||
          symbol.type.id()==ID_union);
@@ -85,7 +85,7 @@ codet cpp_typecheckt::dtor(const symbolt &symbol)
 
       exprt ptrmember(ID_ptrmember);
       ptrmember.set(ID_component_name, c.get_name());
-      ptrmember.operands().push_back(exprt("cpp-this"));
+      ptrmember.operands().push_back(this_expr);
 
       code_assignt assign(ptrmember, address);
       block.add(assign);
@@ -113,8 +113,7 @@ codet cpp_typecheckt::dtor(const symbolt &symbol)
 
     exprt member(ID_ptrmember, type);
     member.set(ID_component_cpp_name, cppname);
-    member.operands().push_back(
-      symbol_exprt(ID_this, pointer_type(symbol.type)));
+    member.operands().push_back(this_expr);
     member.add_source_location() = source_location;
 
     const bool disabled_access_control = disable_access_control;
@@ -139,8 +138,7 @@ codet cpp_typecheckt::dtor(const symbolt &symbol)
     DATA_INVARIANT(bit->id() == ID_base, "base class expression expected");
     const symbolt &psymb = lookup(bit->type());
 
-    symbol_exprt this_ptr(ID_this, pointer_type(symbol.type));
-    dereference_exprt object(this_ptr, psymb.type);
+    dereference_exprt object{this_expr, psymb.type};
     object.add_source_location() = source_location;
 
     const bool disabled_access_control = disable_access_control;
diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp
index 3ee7d3756d3..56d59221f92 100644
--- a/src/cpp/cpp_typecheck_expr.cpp
+++ b/src/cpp/cpp_typecheck_expr.cpp
@@ -698,7 +698,7 @@ void cpp_typecheckt::typecheck_expr_address_of(exprt &expr)
     code_typet &code_type=to_code_type(op.type().subtype());
 
     code_typet::parameterst &args=code_type.parameters();
-    if(!args.empty() && args[0].get_base_name() == ID_this)
+    if(!args.empty() && args.front().get_this())
     {
       // it's a pointer to member function
       const struct_tag_typet symbol(code_type.get(ID_C_member_name));
@@ -2192,7 +2192,7 @@ void cpp_typecheckt::typecheck_side_effect_function_call(
       to_code_type(expr.function().type()).parameters();
 
     if(
-      !parameters.empty() && parameters.front().get_base_name() == ID_this &&
+      !parameters.empty() && parameters.front().get_this() &&
       !expr.arguments().empty())
     {
       const code_typet::parametert &parameter = parameters.front();
diff --git a/src/cpp/cpp_typecheck_fargs.cpp b/src/cpp/cpp_typecheck_fargs.cpp
index c795425e348..bec0d3c1ff8 100644
--- a/src/cpp/cpp_typecheck_fargs.cpp
+++ b/src/cpp/cpp_typecheck_fargs.cpp
@@ -97,7 +97,7 @@ bool cpp_typecheck_fargst::match(
 
     // "this" is a special case -- we turn the pointer type
     // into a reference type to do the type matching
-    if(it == ops.begin() && parameter.get_base_name() == ID_this)
+    if(it == ops.begin() && parameter.get_this())
     {
       type.set(ID_C_reference, true);
       type.set(ID_C_this, true);
diff --git a/src/cpp/cpp_typecheck_function.cpp b/src/cpp/cpp_typecheck_function.cpp
index 597d57991a8..3ea088bb419 100644
--- a/src/cpp/cpp_typecheck_function.cpp
+++ b/src/cpp/cpp_typecheck_function.cpp
@@ -31,6 +31,7 @@ void cpp_typecheckt::convert_parameter(
     parameter.set_base_name(base_name);
   }
 
+  PRECONDITION(!cpp_scopes.current_scope().prefix.empty());
   irep_idt identifier=cpp_scopes.current_scope().prefix+
                       id2string(base_name);
 
@@ -90,22 +91,6 @@ void cpp_typecheckt::convert_function(symbolt &symbol)
   if(symbol.value.is_nil())
     return;
 
-  // if it is a destructor, add the implicit code
-  if(to_code_type(symbol.type).return_type().id() == ID_destructor)
-  {
-    const symbolt &msymb=lookup(symbol.type.get(ID_C_member_name));
-
-    assert(symbol.value.id()==ID_code);
-    assert(symbol.value.get(ID_statement)==ID_block);
-
-    if(
-      !symbol.value.has_operands() || !symbol.value.op0().has_operands() ||
-      symbol.value.op0().op0().id() != ID_already_typechecked)
-    {
-      symbol.value.copy_to_operands(dtor(msymb));
-    }
-  }
-
   // enter appropriate scope
   cpp_save_scopet saved_scope(cpp_scopes);
   cpp_scopet &function_scope=cpp_scopes.set_scope(symbol.name);
@@ -123,13 +108,29 @@ void cpp_typecheckt::convert_function(symbolt &symbol)
     code_typet::parameterst &parameters=function_type.parameters();
     assert(parameters.size()>=1);
     code_typet::parametert &this_parameter_expr=parameters.front();
-    function_scope.this_expr=exprt(ID_symbol, this_parameter_expr.type());
-    function_scope.this_expr.set(
-      ID_identifier, this_parameter_expr.get_identifier());
+    function_scope.this_expr = symbol_exprt{
+      this_parameter_expr.get_identifier(), this_parameter_expr.type()};
   }
   else
     function_scope.this_expr.make_nil();
 
+  // if it is a destructor, add the implicit code
+  if(to_code_type(symbol.type).return_type().id() == ID_destructor)
+  {
+    const symbolt &msymb = lookup(symbol.type.get(ID_C_member_name));
+
+    PRECONDITION(symbol.value.id() == ID_code);
+    PRECONDITION(symbol.value.get(ID_statement) == ID_block);
+
+    if(
+      !symbol.value.has_operands() || !symbol.value.op0().has_operands() ||
+      symbol.value.op0().op0().id() != ID_already_typechecked)
+    {
+      symbol.value.copy_to_operands(
+        dtor(msymb, to_symbol_expr(function_scope.this_expr)));
+    }
+  }
+
   // do the function body
   start_typecheck_code();
 
@@ -147,6 +148,8 @@ void cpp_typecheckt::convert_function(symbolt &symbol)
   symbol.value.type()=symbol.type;
 
   return_type = old_return_type;
+
+  deferred_typechecking.erase(symbol.name);
 }
 
 /// for function overloading
@@ -171,8 +174,7 @@ irep_idt cpp_typecheckt::function_identifier(const typet &type)
   code_typet::parameterst::const_iterator it=
     parameters.begin();
 
-  if(it!=parameters.end() &&
-     it->get_identifier()==ID_this)
+  if(it != parameters.end() && it->get_this())
   {
     const typet &pointer=it->type();
     const typet &symbol =pointer.subtype();
diff --git a/src/cpp/cpp_typecheck_initializer.cpp b/src/cpp/cpp_typecheck_initializer.cpp
index 081c44c19f5..971a1880ceb 100644
--- a/src/cpp/cpp_typecheck_initializer.cpp
+++ b/src/cpp/cpp_typecheck_initializer.cpp
@@ -94,7 +94,7 @@ void cpp_typecheckt::convert_initializer(symbolt &symbol)
         exprt new_object(ID_new_object, parameter.type());
         new_object.set(ID_C_lvalue, true);
 
-        if(parameter.get_base_name() == ID_this)
+        if(parameter.get_this())
         {
           fargs.has_object = true;
           new_object.type() = parameter.type().subtype();
diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp
index 6590838142d..5b2e7070626 100644
--- a/src/cpp/cpp_typecheck_resolve.cpp
+++ b/src/cpp/cpp_typecheck_resolve.cpp
@@ -2075,7 +2075,7 @@ void cpp_typecheck_resolvet::apply_template_args(
 
     if(
       !code_type.parameters().empty() &&
-      code_type.parameters()[0].get_base_name() == ID_this)
+      code_type.parameters().front().get_this())
     {
       // do we have an object?
       if(fargs.has_object)
@@ -2129,9 +2129,7 @@ bool cpp_typecheck_resolvet::disambiguate_functions(
       const code_typet::parameterst &parameters=type.parameters();
       const code_typet::parametert &parameter=parameters.front();
 
-      INVARIANT(
-        parameter.get_base_name() == ID_this,
-        "first parameter should be `this'");
+      INVARIANT(parameter.get_this(), "first parameter should be `this'");
 
       if(type.return_type().id() == ID_constructor)
       {
diff --git a/src/cpp/cpp_typecheck_type.cpp b/src/cpp/cpp_typecheck_type.cpp
index bc5e61a4ae8..ecb9a326183 100644
--- a/src/cpp/cpp_typecheck_type.cpp
+++ b/src/cpp/cpp_typecheck_type.cpp
@@ -106,11 +106,12 @@ void cpp_typecheckt::typecheck_type(typet &type)
         code_typet::parameterst &parameters =
           to_code_type(type.subtype()).parameters();
 
-        if(parameters.empty() || parameters.front().get_base_name() != ID_this)
+        if(parameters.empty() || !parameters.front().get_this())
         {
           // Add 'this' to the parameters
           code_typet::parametert a0(pointer_type(class_object));
           a0.set_base_name(ID_this);
+          a0.set_this();
           parameters.insert(parameters.begin(), a0);
         }
       }