diff --git a/CHANGELOG b/CHANGELOG
index ba9ceda5549..0f15c3d5081 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -20,6 +20,9 @@
 * GOTO-CC: GCC-style error/warning messages
 * GOTO-CC: New options --native-compiler and --native-linker to select the
   compiler/linker to be used when building combined native/goto object files.
+* CBMC, SYMEX, GOTO-INSTRUMENT: New option --drop-unused-functions. Removed
+  ambiguous --show-reachable-properties.
+* CBMC: New option --no-built-in-assertions
 
 
 5.6
diff --git a/regression/cbmc/Pointer_byte_extract9/main.c b/regression/cbmc/Pointer_byte_extract9/main.c
index 931f165c405..0b76b78021f 100644
--- a/regression/cbmc/Pointer_byte_extract9/main.c
+++ b/regression/cbmc/Pointer_byte_extract9/main.c
@@ -1,3 +1,5 @@
+#include <assert.h>
+
 int main()
 {
   int N;
diff --git a/regression/cbmc/graphml_witness1/test.desc b/regression/cbmc/graphml_witness1/test.desc
index 9e7f5b42724..bfd4cf4f3f4 100644
--- a/regression/cbmc/graphml_witness1/test.desc
+++ b/regression/cbmc/graphml_witness1/test.desc
@@ -46,29 +46,29 @@ main.c
   <graph edgedefault="directed">
     <data key="sourcecodelang">C</data>
     <node id="sink"/>
-    <node id="33.22">
+    <node id="[0-9\.]*">
       <data key="entry">true</data>
     </node>
     <edge source="33.22" target="4.29">
       <data key="originfile">main.c</data>
       <data key="startline">21</data>
     </edge>
-    <node id="4.29"/>
-    <edge source="4.29" target="29.31">
+    <node id="[0-9\.]*"/>
+    <edge source="[0-9\.]*" target="[0-9\.]*">
       <data key="originfile">main.c</data>
       <data key="startline">29</data>
       <data key="assumption.scope">main</data>
     </edge>
-    <node id="29.31"/>
-    <edge source="29.31" target="5.33">
+    <node id="[0-9\.]*"/>
+    <edge source="[0-9\.]*" target="[0-9\.]*">
       <data key="originfile">main.c</data>
       <data key="startline">15</data>
       <data key="assumption.scope">remove_one</data>
     </edge>
-    <node id="5.33">
+    <node id="[0-9\.]*">
       <data key="violation">true</data>
     </node>
-    <edge source="5.33" target="sink">
+    <edge source="[0-9\.]*" target="sink">
       <data key="originfile">main.c</data>
       <data key="startline">31</data>
     </edge>
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index caf0795e640..721520e48fa 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -946,7 +946,7 @@ bool cbmc_parse_optionst::process_goto_program(
     if(cmdline.isset("drop-unused-functions"))
     {
       // Entry point will have been set before and function pointers removed
-      status() << "Removing Unused Functions" << eom;
+      status() << "Removing unused functions" << eom;
       remove_unused_functions(goto_functions, ui_message_handler);
     }
 
@@ -1096,7 +1096,6 @@ void cbmc_parse_optionst::help()
     " --property id                only check one specific property\n"
     " --stop-on-fail               stop analysis once a failed property is detected\n" // NOLINT(*)
     " --trace                      give a counterexample trace for failed properties\n" //NOLINT(*)
-    " --drop-unused-functions      drop functions trivially unreachable from main function\n" // NOLINT(*)
     "\n"
     "C/C++ frontend options:\n"
     " -I path                      set include path (C/C++)\n"
@@ -1142,6 +1141,7 @@ void cbmc_parse_optionst::help()
     " --show-parse-tree            show parse tree\n"
     " --show-symbol-table          show symbol table\n"
     HELP_SHOW_GOTO_FUNCTIONS
+    " --drop-unused-functions      drop functions trivially unreachable from main function\n" // NOLINT(*)
     "\n"
     "Program instrumentation options:\n"
     HELP_GOTO_CHECK
@@ -1199,5 +1199,6 @@ void cbmc_parse_optionst::help()
     " --xml-ui                     use XML-formatted output\n"
     " --xml-interface              bi-directional XML interface\n"
     " --json-ui                    use JSON-formatted output\n"
+    " --verbosity #                verbosity level\n"
     "\n";
 }
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index d2173398e4f..21000a78da6 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -744,6 +744,14 @@ int goto_instrument_parse_optionst::doit()
       return 0;
     }
 
+    if(cmdline.isset("drop-unused-functions"))
+    {
+      do_indirect_call_and_rtti_removal();
+
+      status() << "Removing unused functions" << eom;
+      remove_unused_functions(goto_functions, get_message_handler());
+    }
+
     // write new binary?
     if(cmdline.args.size()==2)
     {
@@ -1182,6 +1190,9 @@ void goto_instrument_parse_optionst::instrument_goto_program()
 
   if(cmdline.isset("string-abstraction"))
   {
+    do_indirect_call_and_rtti_removal();
+    do_remove_returns();
+
     status() << "String Abstraction" << eom;
     string_abstraction(
       symbol_table,
diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h
index d3efb975767..180eeb7a2f5 100644
--- a/src/goto-instrument/goto_instrument_parse_options.h
+++ b/src/goto-instrument/goto_instrument_parse_options.h
@@ -45,6 +45,7 @@ Author: Daniel Kroening, kroening@kroening.com
   "(stack-depth):(nondet-static)" \
   "(function-enter):(function-exit):(branch):" \
   OPT_SHOW_GOTO_FUNCTIONS \
+  "(drop-unused-functions)" \
   "(show-value-sets)" \
   "(show-global-may-alias)" \
   "(show-local-bitvector-analysis)(show-custom-bitvector-analysis)" \
diff --git a/src/solvers/flattening/boolbv_floatbv_op.cpp b/src/solvers/flattening/boolbv_floatbv_op.cpp
index 087faa0485a..e4926dc617e 100644
--- a/src/solvers/flattening/boolbv_floatbv_op.cpp
+++ b/src/solvers/flattening/boolbv_floatbv_op.cpp
@@ -138,7 +138,7 @@ bvt boolbvt::convert_floatbv_op(const exprt &expr)
     else if(expr.id()==ID_floatbv_rem)
       return float_utils.rem(bv0, bv1);
     else
-      assert(false);
+      throw "unexpected operator "+expr.id_string();
   }
   else if(type.id()==ID_vector || type.id()==ID_complex)
   {
diff --git a/src/solvers/floatbv/float_utils.cpp b/src/solvers/floatbv/float_utils.cpp
index c277e51e6b0..a772ae0b8a7 100644
--- a/src/solvers/floatbv/float_utils.cpp
+++ b/src/solvers/floatbv/float_utils.cpp
@@ -206,7 +206,7 @@ bvt float_utilst::to_integer(
     return result;
   }
   else
-    assert(0);
+    throw "unsupported rounding mode";
 }
 
 /*******************************************************************\
diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp
index 2b3f00a9bed..a3f671f0fd9 100644
--- a/src/symex/symex_parse_options.cpp
+++ b/src/symex/symex_parse_options.cpp
@@ -386,7 +386,7 @@ bool symex_parse_optionst::process_goto_program(const optionst &options)
     if(cmdline.isset("drop-unused-functions"))
     {
       // Entry point will have been set before and function pointers removed
-      status() << "Removing Unused Functions" << eom;
+      status() << "Removing unused functions" << eom;
       remove_unused_functions(goto_model.goto_functions, ui_message_handler);
     }
 
@@ -690,7 +690,6 @@ void symex_parse_optionst::help()
     " --stop-on-fail               stop analysis once a failed property is detected\n"
     // NOLINTNEXTLINE(whitespace/line_length)
     " --trace                      give a counterexample trace for failed properties\n"
-    " --drop-unused-functions      drop functions trivially unreachable from main function\n" // NOLINT(*)
     "\n"
     "Frontend options:\n"
     " -I path                      set include path (C/C++)\n"
@@ -705,6 +704,7 @@ void symex_parse_optionst::help()
     " --show-parse-tree            show parse tree\n"
     " --show-symbol-table          show symbol table\n"
     HELP_SHOW_GOTO_FUNCTIONS
+    " --drop-unused-functions      drop functions trivially unreachable from main function\n" // NOLINT(*)
     " --ppc-macos                  set MACOS/PPC architecture\n"
     " --mm model                   set memory model (default: sc)\n"
     " --arch                       set architecture (default: "
@@ -738,5 +738,6 @@ void symex_parse_optionst::help()
     "Other options:\n"
     " --version                    show version and exit\n"
     " --xml-ui                     use XML-formatted output\n"
+    " --verbosity #                verbosity level\n"
     "\n";
 }
diff --git a/src/util/irep.h b/src/util/irep.h
index af0b68ac26e..6dd15df0983 100644
--- a/src/util/irep.h
+++ b/src/util/irep.h
@@ -283,11 +283,7 @@ class irept
 
     void clear()
     {
-      #ifdef USE_DSTRING
       data.clear();
-      #else
-      data="";
-      #endif
       sub.clear();
       named_sub.clear();
       comments.clear();
diff --git a/src/util/json_irep.cpp b/src/util/json_irep.cpp
index 403247c1d04..2740228d1db 100644
--- a/src/util/json_irep.cpp
+++ b/src/util/json_irep.cpp
@@ -164,8 +164,8 @@ void json_irept::convert_from_json(const jsont &in, irept &out) const
   }
 
   for(const auto &named_sub : in["namedSub"].object)
-    convert_from_json(named_sub.second, out.get_named_sub()[named_sub.first]);
+    convert_from_json(named_sub.second, out.add(named_sub.first));
 
   for(const auto &comment : in["comment"].object)
-    convert_from_json(comment.second, out.get_comments()[comment.first]);
+    convert_from_json(comment.second, out.add(comment.first));
 }
diff --git a/src/util/rename_symbol.cpp b/src/util/rename_symbol.cpp
index 55a9a7ff484..c6930a01d87 100644
--- a/src/util/rename_symbol.cpp
+++ b/src/util/rename_symbol.cpp
@@ -133,6 +133,9 @@ Function: rename_symbolt::have_to_rename
 
 bool rename_symbolt::have_to_rename(const exprt &dest) const
 {
+  if(expr_map.empty() && type_map.empty())
+    return false;
+
   // first look at type
 
   if(have_to_rename(dest.type()))
@@ -274,6 +277,9 @@ Function: rename_symbolt::have_to_rename
 
 bool rename_symbolt::have_to_rename(const typet &dest) const
 {
+  if(expr_map.empty() && type_map.empty())
+    return false;
+
   if(dest.has_subtype())
     if(have_to_rename(dest.subtype()))
       return true;