diff --git a/regression/systemc/BitvectorSc1/main.cpp b/regression/systemc/BitvectorSc1/main.cpp
index 333c10801cf..de17f4cee01 100644
--- a/regression/systemc/BitvectorSc1/main.cpp
+++ b/regression/systemc/BitvectorSc1/main.cpp
@@ -1,5 +1,3 @@
-#include <cassert>
-
 template <int W>
 class sc_uint {
   public:
@@ -41,8 +39,8 @@ int main(int argc, char** argv)
   x.test1();
   x.test2();
 
-  assert(x.to_uint() == 1);
-  assert(x.to_uint() == 2);
+  __CPROVER_assert(x.to_uint() == 1, "");
+  __CPROVER_assert(x.to_uint() == 2, "");
 
   return 0;
 }
diff --git a/regression/systemc/BitvectorSc2/main.cpp b/regression/systemc/BitvectorSc2/main.cpp
index 6ebf3fd5a8b..f9832777707 100644
--- a/regression/systemc/BitvectorSc2/main.cpp
+++ b/regression/systemc/BitvectorSc2/main.cpp
@@ -1,5 +1,3 @@
-#include <cassert>
-
 template <int W>
 class sc_uint {
   public:
@@ -56,7 +54,7 @@ int main(int argc, char** argv)
   z += y;
 
   sc_uint<10> w(3);
-  assert(z == w);
+  __CPROVER_assert(z == w, "");
 
   return 0;
 }
diff --git a/regression/systemc/BitvectorSc3/test.desc b/regression/systemc/BitvectorSc3/test.desc
index 6666d172f47..91d9cf8b52e 100644
--- a/regression/systemc/BitvectorSc3/test.desc
+++ b/regression/systemc/BitvectorSc3/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/systemc/EqualOp1/main.cpp b/regression/systemc/EqualOp1/main.cpp
index dc0ee0c536d..320c0ab3a99 100644
--- a/regression/systemc/EqualOp1/main.cpp
+++ b/regression/systemc/EqualOp1/main.cpp
@@ -1,5 +1,3 @@
-#include <cassert>
-
 template<class T>
 class myclass
 {
@@ -20,5 +18,5 @@ int main(int argc, char** argv)
   myclass<int> x(0);
   myclass<int> y(1);
   x = y;
-  assert(x == y);
+  __CPROVER_assert(x == y, "");
 }
diff --git a/regression/systemc/EqualOp2/main.cpp b/regression/systemc/EqualOp2/main.cpp
index 1f656bf858d..dacdc8261f9 100644
--- a/regression/systemc/EqualOp2/main.cpp
+++ b/regression/systemc/EqualOp2/main.cpp
@@ -1,5 +1,3 @@
-#include <cassert>
-
 template<class T>
 class myclass
 {
@@ -26,5 +24,5 @@ int main(int argc, char** argv)
   myclass<int> y(1);
   //x = y;
   x += 1;
-  assert(x == y);
+  __CPROVER_assert(x == y, "");
 }
diff --git a/regression/systemc/EqualOp3/main.cpp b/regression/systemc/EqualOp3/main.cpp
index e910b6f2b39..efdbb9d965b 100644
--- a/regression/systemc/EqualOp3/main.cpp
+++ b/regression/systemc/EqualOp3/main.cpp
@@ -1,5 +1,3 @@
-#include <cassert>
-
 template<class T>
 class myclass2;
 
@@ -38,6 +36,6 @@ int main(int argc, char** argv)
   myclass2<int> x(0);
   myclass<int> y(1);
   x = y;
-  assert(x == y);
+  __CPROVER_assert(x == y, "");
   return 0;
 }
diff --git a/regression/systemc/ForwardDecl1/test.desc b/regression/systemc/ForwardDecl1/test.desc
index 6666d172f47..91d9cf8b52e 100644
--- a/regression/systemc/ForwardDecl1/test.desc
+++ b/regression/systemc/ForwardDecl1/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/systemc/FunTempl1/main.cpp b/regression/systemc/FunTempl1/main.cpp
index fda3e04ed39..b4f820963e2 100644
--- a/regression/systemc/FunTempl1/main.cpp
+++ b/regression/systemc/FunTempl1/main.cpp
@@ -1,5 +1,3 @@
-#include <cassert>
-
 template<class T>
 T inc(T x)
 {
@@ -15,5 +13,5 @@ int main(int argc, char** argv)
   x = inc<int>(x);
   y = inc<unsigned char>(y);
 
-  assert(x == y);
+  __CPROVER_assert(x == y, "");
 }
diff --git a/regression/systemc/Mult1/test.desc b/regression/systemc/Mult1/test.desc
index 6666d172f47..c9bf3d90ae3 100644
--- a/regression/systemc/Mult1/test.desc
+++ b/regression/systemc/Mult1/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 main.cpp
-
+--object-bits 10
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/systemc/SimpleSc1/main.cpp b/regression/systemc/SimpleSc1/main.cpp
index 379beb106ec..0b682ec51ef 100644
--- a/regression/systemc/SimpleSc1/main.cpp
+++ b/regression/systemc/SimpleSc1/main.cpp
@@ -1,5 +1,3 @@
-#include <cassert>
-
 template <int W>
 class sc_uint {
   public:
@@ -54,7 +52,7 @@ int main(int argc, char** argv)
   z += y;
 
   sc_uint<10> w(3);
-  assert(z == w);
+  __CPROVER_assert(z == w, "");
 
   return 0;
 }
diff --git a/regression/systemc/Template1/main.cpp b/regression/systemc/Template1/main.cpp
index 5702637542f..b40033fd4d1 100644
--- a/regression/systemc/Template1/main.cpp
+++ b/regression/systemc/Template1/main.cpp
@@ -1,5 +1,3 @@
-#include <cassert>
-
 #define DEF_INSIDE
 
 template<class T>
@@ -35,8 +33,8 @@ int main (int argc, char *argv[])
   my_template<int> x;
   x.set(5);
   int y = x.get();
-  assert(y==5);
-  assert(z.get()==3);
+  __CPROVER_assert(y == 5, "");
+  __CPROVER_assert(z.get() == 3, "");
 
   return 0;
 }
diff --git a/regression/systemc/Tuple1/test.desc b/regression/systemc/Tuple1/test.desc
index 839148c295a..d091759e812 100644
--- a/regression/systemc/Tuple1/test.desc
+++ b/regression/systemc/Tuple1/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.cpp
 -DNO_IO -DNO_STRING
 ^EXIT=0$
diff --git a/regression/systemc/Tuple2/test.desc b/regression/systemc/Tuple2/test.desc
index 839148c295a..d091759e812 100644
--- a/regression/systemc/Tuple2/test.desc
+++ b/regression/systemc/Tuple2/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.cpp
 -DNO_IO -DNO_STRING
 ^EXIT=0$
diff --git a/src/cpp/cpp_declarator_converter.cpp b/src/cpp/cpp_declarator_converter.cpp
index 1991c280556..82fee24d3ff 100644
--- a/src/cpp/cpp_declarator_converter.cpp
+++ b/src/cpp/cpp_declarator_converter.cpp
@@ -64,11 +64,22 @@ symbolt &cpp_declarator_convertert::convert(
     cpp_typecheck_resolve.resolve_scope(
       declarator.name(), base_name, template_args);
 
+    cpp_scopet *friend_scope = nullptr;
+
+    if(is_friend)
+    {
+      friend_scope = &cpp_typecheck.cpp_scopes.current_scope();
+      save_scope.restore();
+    }
+
     scope=&cpp_typecheck.cpp_scopes.current_scope();
 
-    // check the declarator-part of the type, in that scope
+    // check the declarator-part of the type, in the current scope
     if(declarator.value().is_nil() || !cpp_typecheck.has_auto(final_type))
       cpp_typecheck.typecheck_type(final_type);
+
+    if(friend_scope)
+      scope = friend_scope;
   }
 
   is_code=is_code_type(final_type);
@@ -80,9 +91,9 @@ symbolt &cpp_declarator_convertert::convert(
   get_final_identifier();
 
   // first see if it is a member
-  if(scope->id_class==cpp_idt::id_classt::CLASS && !is_friend)
+  if(scope->id_class == cpp_idt::id_classt::CLASS)
   {
-    // it's a member! it must be declared already
+    // it's a member! it must be declared already, unless it's a friend
 
     typet &method_qualifier=
       static_cast<typet &>(declarator.method_qualifier());
@@ -118,7 +129,15 @@ symbolt &cpp_declarator_convertert::convert(
 
       // try again
       maybe_symbol=cpp_typecheck.symbol_table.get_writeable(final_identifier);
-      if(!maybe_symbol)
+      if(!maybe_symbol && is_friend)
+      {
+        symbolt &friend_symbol =
+          convert_new_symbol(storage_spec, member_spec, declarator);
+        // mark it as weak so that the full declaration can replace the symbol
+        friend_symbol.is_weak = true;
+        return friend_symbol;
+      }
+      else if(!maybe_symbol)
       {
         cpp_typecheck.error().source_location=
           declarator.name().source_location();
@@ -411,9 +430,7 @@ void cpp_declarator_convertert::get_final_identifier()
     }
   }
 
-  final_identifier=
-    scope->prefix+
-    identifier;
+  final_identifier = scope->prefix + identifier;
 }
 
 symbolt &cpp_declarator_convertert::convert_new_symbol(
diff --git a/src/cpp/cpp_id.h b/src/cpp/cpp_id.h
index b2efbc27188..92033df82ee 100644
--- a/src/cpp/cpp_id.h
+++ b/src/cpp/cpp_id.h
@@ -70,6 +70,11 @@ class cpp_idt
     return id_class==id_classt::TYPEDEF;
   }
 
+  bool is_template_scope() const
+  {
+    return id_class == id_classt::TEMPLATE_SCOPE;
+  }
+
   irep_idt identifier, base_name;
 
   // if it is a member or method, what class is it in?
diff --git a/src/cpp/cpp_instantiate_template.cpp b/src/cpp/cpp_instantiate_template.cpp
index 40387681230..0f283827c9c 100644
--- a/src/cpp/cpp_instantiate_template.cpp
+++ b/src/cpp/cpp_instantiate_template.cpp
@@ -103,6 +103,40 @@ void cpp_typecheckt::show_instantiation_stack(std::ostream &out)
   }
 }
 
+/// Set up a scope as subscope of the template scope
+cpp_scopet &cpp_typecheckt::sub_scope_for_instantiation(
+  cpp_scopet &template_scope,
+  const std::string &suffix)
+{
+  cpp_scopet::id_sett id_set =
+    template_scope.lookup(suffix, cpp_scopet::SCOPE_ONLY);
+
+  CHECK_RETURN(id_set.size() <= 1);
+
+  if(id_set.size() == 1)
+  {
+    cpp_idt &cpp_id = **id_set.begin();
+    CHECK_RETURN(cpp_id.is_template_scope());
+
+    return static_cast<cpp_scopet &>(cpp_id);
+  }
+  else
+  {
+    cpp_scopet &sub_scope = template_scope.new_scope(suffix);
+    sub_scope.id_class = cpp_idt::id_classt::TEMPLATE_SCOPE;
+    sub_scope.prefix = template_scope.get_parent().prefix;
+    sub_scope.suffix = suffix;
+    sub_scope.add_using_scope(template_scope.get_parent());
+
+    const std::string subscope_name =
+      id2string(template_scope.identifier) + suffix;
+    cpp_scopes.id_map.insert(
+      cpp_scopest::id_mapt::value_type(subscope_name, &sub_scope));
+
+    return sub_scope;
+  }
+}
+
 const symbolt &cpp_typecheckt::class_template_symbol(
   const source_locationt &source_location,
   const symbolt &template_symbol,
@@ -131,10 +165,9 @@ const symbolt &cpp_typecheckt::class_template_symbol(
   INVARIANT_STRUCTURED(
     template_scope!=nullptr, nullptr_exceptiont, "template_scope is null");
 
-  irep_idt identifier=
-    id2string(template_scope->prefix)+
-    "tag-"+id2string(template_symbol.base_name)+
-    id2string(suffix);
+  irep_idt identifier = id2string(template_scope->get_parent().prefix) +
+                        "tag-" + id2string(template_symbol.base_name) +
+                        id2string(suffix);
 
   // already there?
   symbol_tablet::symbolst::const_iterator s_it=
@@ -171,9 +204,8 @@ const symbolt &cpp_typecheckt::class_template_symbol(
 
   id.id_class=cpp_idt::id_classt::CLASS;
   id.is_scope=true;
-  id.prefix=template_scope->prefix+
-            id2string(s_ptr->base_name)+
-            id2string(suffix)+"::";
+  id.prefix = template_scope->get_parent().prefix +
+              id2string(s_ptr->base_name) + id2string(suffix) + "::";
   id.class_identifier=s_ptr->name;
   id.id_class=cpp_idt::id_classt::CLASS;
 
@@ -318,18 +350,12 @@ const symbolt &cpp_typecheckt::instantiate_template(
     class_name=cpp_scopes.current_scope().get_parent().identifier;
 
   // sub-scope for fixing the prefix
-  std::string subscope_name=id2string(template_scope->identifier)+suffix;
+  cpp_scopet &sub_scope = sub_scope_for_instantiation(*template_scope, suffix);
 
   // let's see if we have the instance already
-  cpp_scopest::id_mapt::iterator scope_it=
-    cpp_scopes.id_map.find(subscope_name);
-
-  if(scope_it!=cpp_scopes.id_map.end())
   {
-    cpp_scopet &scope=cpp_scopes.get_scope(subscope_name);
-
-    const auto id_set =
-      scope.lookup(template_symbol.base_name, cpp_scopet::SCOPE_ONLY);
+    cpp_scopet::id_sett id_set =
+      sub_scope.lookup(template_symbol.base_name, cpp_scopet::SCOPE_ONLY);
 
     if(id_set.size()==1)
     {
@@ -349,20 +375,7 @@ const symbolt &cpp_typecheckt::instantiate_template(
         return symb;
     }
 
-    cpp_scopes.go_to(scope);
-  }
-  else
-  {
-    // set up a scope as subscope of the template scope
-    cpp_scopet &sub_scope=
-      cpp_scopes.current_scope().new_scope(subscope_name);
-    sub_scope.id_class=cpp_idt::id_classt::TEMPLATE_SCOPE;
-    sub_scope.prefix=template_scope->get_parent().prefix;
-    sub_scope.suffix=suffix;
-    sub_scope.add_using_scope(template_scope->get_parent());
     cpp_scopes.go_to(sub_scope);
-    cpp_scopes.id_map.insert(
-      cpp_scopest::id_mapt::value_type(subscope_name, &sub_scope));
   }
 
   // store the information that the template has
diff --git a/src/cpp/cpp_scope.h b/src/cpp/cpp_scope.h
index 47426f8e58d..0e94aa6de60 100644
--- a/src/cpp/cpp_scope.h
+++ b/src/cpp/cpp_scope.h
@@ -85,11 +85,6 @@ class cpp_scopet:public cpp_idt
            id_class==id_classt::NAMESPACE;
   }
 
-  bool is_template_scope() const
-  {
-    return id_class==id_classt::TEMPLATE_SCOPE;
-  }
-
   cpp_scopet &get_parent() const
   {
     return static_cast<cpp_scopet &>(cpp_idt::get_parent());
diff --git a/src/cpp/cpp_scopes.cpp b/src/cpp/cpp_scopes.cpp
index aa7ea8c6a99..b913bb153c0 100644
--- a/src/cpp/cpp_scopes.cpp
+++ b/src/cpp/cpp_scopes.cpp
@@ -48,7 +48,6 @@ cpp_idt &cpp_scopest::put_into_scope(
   {
     cpp_save_scopet saved_scope(*this);
     go_to(scope);
-    go_to_global_scope();
 
     cpp_idt &id=current_scope().insert(symbol.base_name);
     id.identifier=symbol.name;
diff --git a/src/cpp/cpp_typecheck.h b/src/cpp/cpp_typecheck.h
index 05b040c158b..c8dbcd8ef4b 100644
--- a/src/cpp/cpp_typecheck.h
+++ b/src/cpp/cpp_typecheck.h
@@ -230,6 +230,10 @@ class cpp_typecheckt:public c_typecheck_baset
   std::string template_suffix(
     const cpp_template_args_tct &template_args);
 
+  cpp_scopet &sub_scope_for_instantiation(
+    cpp_scopet &template_scope,
+    const std::string &suffix);
+
   void
   convert_parameters(const irep_idt &current_mode, code_typet &function_type);
 
diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp
index e21d2625ffc..a49df6d7328 100644
--- a/src/cpp/cpp_typecheck_compound_type.cpp
+++ b/src/cpp/cpp_typecheck_compound_type.cpp
@@ -861,13 +861,9 @@ void cpp_typecheckt::typecheck_friend_declaration(
 
   if(declaration.is_template())
   {
-    return; // TODO
-
-#if 0
     error().source_location=declaration.type().source_location();
     error() << "friend template not supported" << eom;
     throw 0;
-#endif
   }
 
   // we distinguish these whether there is a declarator
@@ -890,11 +886,10 @@ void cpp_typecheckt::typecheck_friend_declaration(
       throw 0;
     }
 
-    // typecheck ftype
-
-    // TODO
-    //    typecheck_type(ftype);
-    //    symbol.type.add("ID_C_friends").move_to_sub(ftype);
+    cpp_save_scopet saved_scope(cpp_scopes);
+    cpp_scopes.go_to_global_scope();
+    typecheck_type(ftype);
+    symbol.type.add(ID_C_friends).move_to_sub(ftype);
 
     return;
   }
@@ -902,39 +897,30 @@ void cpp_typecheckt::typecheck_friend_declaration(
   // It should be a friend function.
   // Do the declarators.
 
+#ifdef DEBUG
+  std::cout << "friend declaration: " << declaration.pretty() << '\n';
+#endif
+
   for(auto &sub_it : declaration.declarators())
   {
-    bool has_value = sub_it.value().is_not_nil();
-
-    if(!has_value)
-    {
-      // If no value is found, then we jump to the
-      // global scope, and we convert the declarator
-      // as if it were declared there
-      cpp_save_scopet saved_scope(cpp_scopes);
-      cpp_scopes.go_to_global_scope();
-      cpp_declarator_convertert cpp_declarator_converter(*this);
-      const symbolt &conv_symb=cpp_declarator_converter.convert(
-          declaration.type(), declaration.storage_spec(),
-          declaration.member_spec(), sub_it);
-      exprt symb_expr=cpp_symbol_expr(conv_symb);
-      symbol.type.add(ID_C_friends).move_to_sub(symb_expr);
-    }
-    else
-    {
-      cpp_declarator_convertert cpp_declarator_converter(*this);
-      cpp_declarator_converter.is_friend=true;
+#ifdef DEBUG
+    std::cout << "decl: " << sub_it.pretty() << "\n with value "
+              << sub_it.value().pretty() << '\n';
+    std::cout << "  scope: " << cpp_scopes.current_scope().prefix << '\n';
+#endif
 
+    if(sub_it.value().is_not_nil())
       declaration.member_spec().set_inline(true);
 
-      const symbolt &conv_symb=cpp_declarator_converter.convert(
-        declaration.type(), declaration.storage_spec(),
-        declaration.member_spec(), sub_it);
-
-      exprt symb_expr=cpp_symbol_expr(conv_symb);
-
-      symbol.type.add(ID_C_friends).move_to_sub(symb_expr);
-    }
+    cpp_declarator_convertert cpp_declarator_converter(*this);
+    cpp_declarator_converter.is_friend = true;
+    const symbolt &conv_symb = cpp_declarator_converter.convert(
+      declaration.type(),
+      declaration.storage_spec(),
+      declaration.member_spec(),
+      sub_it);
+    exprt symb_expr = cpp_symbol_expr(conv_symb);
+    symbol.type.add(ID_C_friends).move_to_sub(symb_expr);
   }
 }
 
@@ -1322,7 +1308,13 @@ void cpp_typecheckt::typecheck_member_function(
   // move early, it must be visible before doing any value
   symbolt *new_symbol;
 
-  if(symbol_table.move(symbol, new_symbol))
+  const bool symbol_exists = symbol_table.move(symbol, new_symbol);
+  if(symbol_exists && new_symbol->is_weak)
+  {
+    // there might have been an earlier friend declaration
+    *new_symbol = std::move(symbol);
+  }
+  else if(symbol_exists)
   {
     error().source_location=symbol.location;
     error() << "failed to insert new method symbol: " << symbol.name << '\n'
diff --git a/src/cpp/cpp_typecheck_conversions.cpp b/src/cpp/cpp_typecheck_conversions.cpp
index 0cac0be741a..c0ae97a8898 100644
--- a/src/cpp/cpp_typecheck_conversions.cpp
+++ b/src/cpp/cpp_typecheck_conversions.cpp
@@ -1251,10 +1251,21 @@ bool cpp_typecheckt::reference_binding(
       return false;
   }
 
-  if(expr.get_bool(ID_C_lvalue))
+  if(expr.get_bool(ID_C_lvalue) || type.subtype().get_bool(ID_C_constant))
   {
     if(reference_compatible(expr, type, rank))
     {
+      if(!expr.get_bool(ID_C_lvalue))
+      {
+        // create temporary object
+        side_effect_exprt tmp{ID_temporary_object,
+                              {std::move(expr)},
+                              type.subtype(),
+                              expr.source_location()};
+        tmp.set(ID_mode, ID_cpp);
+        expr.swap(tmp);
+      }
+
       {
         address_of_exprt tmp(expr, reference_type(expr.type()));
         tmp.add_source_location()=expr.source_location();
diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp
index 56d59221f92..d1ec746a5be 100644
--- a/src/cpp/cpp_typecheck_expr.cpp
+++ b/src/cpp/cpp_typecheck_expr.cpp
@@ -1175,11 +1175,9 @@ void cpp_typecheckt::typecheck_expr_member(
         if(pcomp.is_nil())
         {
           error().source_location=expr.find_source_location();
-          error() << "error: `"
-                  << symbol_expr.get(ID_identifier)
+          error() << "error: `" << symbol_expr.get(ID_identifier)
                   << "' is not static member "
-                  << "of class `" << to_string(type) << "'"
-                  << eom;
+                  << "of class `" << to_string(op0.type()) << "'" << eom;
           throw 0;
         }
       }
diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp
index 5b2e7070626..c56fc46e5a3 100644
--- a/src/cpp/cpp_typecheck_resolve.cpp
+++ b/src/cpp/cpp_typecheck_resolve.cpp
@@ -463,54 +463,44 @@ void cpp_typecheck_resolvet::disambiguate_functions(
     }
   }
 
-  identifiers.clear();
+  old_identifiers.clear();
 
   // put in the top ones
   if(!distance_map.empty())
   {
-    std::size_t distance=distance_map.begin()->first;
-
-    for(std::multimap<std::size_t, exprt>::const_iterator
-        it=distance_map.begin();
-        it!=distance_map.end() && it->first==distance;
-        it++)
-      identifiers.push_back(it->second);
+    auto range = distance_map.equal_range(distance_map.begin()->first);
+    for(auto it = range.first; it != range.second; ++it)
+      old_identifiers.push_back(it->second);
   }
 
-  if(identifiers.size()>1 && fargs.in_use)
+  if(old_identifiers.size() > 1 && fargs.in_use)
   {
     // try to further disambiguate functions
 
-    for(resolve_identifierst::iterator
-        it1=identifiers.begin();
-        it1!=identifiers.end();
-        it1++)
+    for(resolve_identifierst::const_iterator old_it = old_identifiers.begin();
+        old_it != old_identifiers.end();
+        ++old_it)
     {
-      if(it1->type().id()!=ID_code)
+#if 0
+      std::cout << "I1: " << old_it->get(ID_identifier) << '\n';
+#endif
+
+      if(old_it->type().id() != ID_code)
+      {
+        identifiers.push_back(*old_it);
         continue;
+      }
 
-      const code_typet &f1=
-        to_code_type(it1->type());
+      const code_typet &f1 = to_code_type(old_it->type());
 
-      for(resolve_identifierst::iterator it2=
-          identifiers.begin();
-          it2!=identifiers.end();
-          ) // no it2++
+      for(resolve_identifierst::const_iterator resolve_it = old_it + 1;
+          resolve_it != old_identifiers.end();
+          ++resolve_it)
       {
-        if(it1 == it2)
-        {
-          it2++;
+        if(resolve_it->type().id() != ID_code)
           continue;
-        }
 
-        if(it2->type().id()!=ID_code)
-        {
-          it2++;
-          continue;
-        }
-
-        const code_typet &f2 =
-          to_code_type(it2->type());
+        const code_typet &f2 = to_code_type(resolve_it->type());
 
         // TODO: may fail when using ellipsis
         assert(f1.parameters().size() == f2.parameters().size());
@@ -562,14 +552,17 @@ void cpp_typecheck_resolvet::disambiguate_functions(
           }
         }
 
-        resolve_identifierst::iterator prev_it=it2;
-        it2++;
-
-        if(f1_better && !f2_better)
-          identifiers.erase(prev_it);
+        if(!f1_better || f2_better)
+          identifiers.push_back(*resolve_it);
       }
     }
   }
+  else
+  {
+    identifiers.swap(old_identifiers);
+  }
+
+  remove_duplicates(identifiers);
 }
 
 void cpp_typecheck_resolvet::make_constructors(
@@ -1566,8 +1559,8 @@ exprt cpp_typecheck_resolvet::resolve(
     std::cout << '\n';
 #endif
   }
-
-  remove_duplicates(new_identifiers);
+  else
+    remove_duplicates(new_identifiers);
 
 #ifdef DEBUG
   std::cout << "P4 " << base_name << " " << new_identifiers.size() << '\n';
diff --git a/src/cpp/cpp_typecheck_template.cpp b/src/cpp/cpp_typecheck_template.cpp
index a3f2d351e08..53eeeb7e79f 100644
--- a/src/cpp/cpp_typecheck_template.cpp
+++ b/src/cpp/cpp_typecheck_template.cpp
@@ -158,8 +158,10 @@ void cpp_typecheckt::typecheck_class_template(
         previous_declaration.template_type());
     }
 
-    assert(cpp_scopes.id_map[symbol_name]->id_class ==
-           cpp_idt::id_classt::TEMPLATE_SCOPE);
+    INVARIANT(
+      cpp_scopes.id_map[symbol_name]->is_template_scope(),
+      "symbol should be in template scope");
+
     return;
   }
 
@@ -197,8 +199,10 @@ void cpp_typecheckt::typecheck_class_template(
 
   // link the template symbol with the template scope
   cpp_scopes.id_map[symbol_name]=&template_scope;
-  assert(cpp_scopes.id_map[symbol_name]->id_class ==
-         cpp_idt::id_classt::TEMPLATE_SCOPE);
+
+  INVARIANT(
+    cpp_scopes.id_map[symbol_name]->is_template_scope(),
+    "symbol should be in template scope");
 }
 
 /// typecheck function templates
@@ -300,8 +304,9 @@ void cpp_typecheckt::typecheck_function_template(
             id2string(new_symbol->base_name);
 
   // link the template symbol with the template scope
-  assert(template_scope.id_class==cpp_idt::id_classt::TEMPLATE_SCOPE);
   cpp_scopes.id_map[symbol_name] = &template_scope;
+  INVARIANT(
+    template_scope.is_template_scope(), "symbol should be in template scope");
 }
 
 /// typecheck class template members; these can be methods or static members
@@ -714,11 +719,7 @@ cpp_scopet &cpp_typecheckt::typecheck_template_parameters(
   std::string id_suffix="template::"+std::to_string(template_counter++);
 
   // produce a new scope for the template parameters
-  cpp_scopet &template_scope=
-    cpp_scopes.current_scope().new_scope(
-      cpp_scopes.current_scope().prefix+id_suffix);
-
-  template_scope.prefix=template_scope.get_parent().prefix+id_suffix;
+  cpp_scopet &template_scope = cpp_scopes.current_scope().new_scope(id_suffix);
   template_scope.id_class=cpp_idt::id_classt::TEMPLATE_SCOPE;
 
   cpp_scopes.go_to(template_scope);
@@ -821,9 +822,6 @@ cpp_scopet &cpp_typecheckt::typecheck_template_parameters(
     #endif
   }
 
-  // continue without adding to the prefix
-  template_scope.prefix=template_scope.get_parent().prefix;
-
   return template_scope;
 }
 
diff --git a/src/cpp/expr2cpp.cpp b/src/cpp/expr2cpp.cpp
index 1fc04960bd6..0be8f2c12fe 100644
--- a/src/cpp/expr2cpp.cpp
+++ b/src/cpp/expr2cpp.cpp
@@ -190,7 +190,7 @@ std::string expr2cppt::convert_rec(
       if(tag.id() == ID_cpp_name)
         dest += " " + to_cpp_name(tag).to_string();
       else
-        dest += id2string(tag.id());
+        dest += " " + id2string(tag.id());
     }
 
     dest += d;
@@ -209,7 +209,7 @@ std::string expr2cppt::convert_rec(
       if(tag.id() == ID_cpp_name)
         dest += " " + to_cpp_name(tag).to_string();
       else
-        dest += id2string(tag.id());
+        dest += " " + id2string(tag.id());
     }
 
     dest += d;