diff --git a/lib/cbmc b/lib/cbmc
index 7ac49c6c1..6275632e7 160000
--- a/lib/cbmc
+++ b/lib/cbmc
@@ -1 +1 @@
-Subproject commit 7ac49c6c1d53c7689d586b54945949fd3b8ad51e
+Subproject commit 6275632e75a46a4ee8b87009ce8e7693878f1db9
diff --git a/regression/memsafety/built_from_end_false/test.desc b/regression/memsafety/built_from_end_false/test.desc
index a91a719ec..e100b955f 100644
--- a/regression/memsafety/built_from_end_false/test.desc
+++ b/regression/memsafety/built_from_end_false/test.desc
@@ -4,4 +4,4 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-\[main.pointer_dereference.11\] dereference failure: deallocated dynamic object in \*p: FAILURE
+\[main.pointer_dereference.15\] dereference failure: deallocated dynamic object in \*p: FAILURE
diff --git a/regression/memsafety/simple_false/test.desc b/regression/memsafety/simple_false/test.desc
index 8efda9ea8..f091cf7f8 100644
--- a/regression/memsafety/simple_false/test.desc
+++ b/regression/memsafety/simple_false/test.desc
@@ -4,4 +4,4 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-\[main.pointer_dereference.23\] dereference failure: deallocated dynamic object in \*p: FAILURE
+\[main.pointer_dereference.33\] dereference failure: deallocated dynamic object in \*p: FAILURE
diff --git a/src/2ls/2ls_parse_options.cpp b/src/2ls/2ls_parse_options.cpp
index 933847401..80a748b7e 100644
--- a/src/2ls/2ls_parse_options.cpp
+++ b/src/2ls/2ls_parse_options.cpp
@@ -125,7 +125,7 @@ void twols_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("slice", false);
 
   // all checks supported by goto_check
-  GOTO_CHECK_PARSE_OPTIONS(cmdline, options);
+  PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
 
   // check assertions
   if(cmdline.isset("no-assertions"))
@@ -1087,10 +1087,14 @@ bool twols_parse_optionst::process_goto_program(
       goto_inlinet goto_inline(
         goto_model.goto_functions,
         ns,
-        ui_message_handler);
+        ui_message_handler,
+        false);
       goto_inline();
 #if IGNORE_RECURSION
       recursion_detected=goto_inline.recursion_detected();
+      // since CBMC 5.7, inlining doesn't update location and loop numbers
+      goto_model.goto_functions.update();
+      goto_model.goto_functions.compute_loop_numbers();
 #endif
     }
 
@@ -1559,7 +1563,7 @@ void twols_parse_optionst::help()
     " --round-to-zero              IEEE floating point rounding mode\n"
     "\n"
     "Program instrumentation options:\n"
-    GOTO_CHECK_HELP
+    HELP_GOTO_CHECK
     " --error-label label          check that label is unreachable\n"
     " --show-properties            show the properties\n"
     " --no-assertions              ignore user assertions\n"
diff --git a/src/2ls/2ls_parse_options.h b/src/2ls/2ls_parse_options.h
index 272399fb7..99a53af82 100644
--- a/src/2ls/2ls_parse_options.h
+++ b/src/2ls/2ls_parse_options.h
@@ -31,7 +31,7 @@ class optionst;
   "(function):" \
   "D:I:" \
   "(depth):(context-bound):(unwind):" \
-  GOTO_CHECK_OPTIONS \
+  OPT_GOTO_CHECK \
   "(non-incremental)" \
   "(no-assertions)(no-assumptions)" \
   "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
diff --git a/src/2ls/dynamic_cfg.h b/src/2ls/dynamic_cfg.h
index 3d8a9537c..928e4dbbf 100644
--- a/src/2ls/dynamic_cfg.h
+++ b/src/2ls/dynamic_cfg.h
@@ -14,7 +14,6 @@ Author: Peter Schrammel
 
 #include <util/std_expr.h>
 #include <util/graph.h>
-#include <util/i2string.h>
 #include <goto-programs/goto_program.h>
 
 #include <ssa/ssa_unwinder.h>
@@ -35,9 +34,9 @@ struct dynamic_cfg_idt
   std::string to_string() const
   {
     std::ostringstream sid;
-    sid << i2string(pc->location_number);
+    sid << std::to_string(pc->location_number);
     for(const auto &i : iteration_stack)
-      sid << "." <<i2string(i);
+      sid << "." <<std::to_string(i);
     return sid.str();
   }
 };
@@ -51,7 +50,7 @@ struct dynamic_cfg_nodet:public graph_nodet<dynamic_cfg_edget>
   exprt assumption;
 };
 
-class dynamic_cfgt:public graph<dynamic_cfg_nodet>
+class dynamic_cfgt:public grapht<dynamic_cfg_nodet>
 {
 public:
   inline dynamic_cfg_nodet& operator[](const dynamic_cfg_idt &id)
diff --git a/src/2ls/preprocessing_util.cpp b/src/2ls/preprocessing_util.cpp
index 59f1e29a1..a4cd73134 100644
--- a/src/2ls/preprocessing_util.cpp
+++ b/src/2ls/preprocessing_util.cpp
@@ -190,7 +190,7 @@ void twols_parse_optionst::remove_multiple_dereferences(
       {
         symbolt new_symbol;
         new_symbol.type=member_expr.type();
-        new_symbol.name="$deref"+i2string(var_counter++);
+        new_symbol.name="$deref"+std::to_string(var_counter++);
         new_symbol.base_name=new_symbol.name;
         new_symbol.pretty_name=new_symbol.name;
         goto_model.symbol_table.add(new_symbol);
@@ -465,7 +465,7 @@ void twols_parse_optionst::split_same_symbolic_object_assignments(
           {
             symbolt tmp_symbol;
             tmp_symbol.type=assign.lhs().type();
-            tmp_symbol.name="$symderef_tmp"+i2string(counter++);
+            tmp_symbol.name="$symderef_tmp"+std::to_string(counter++);
             tmp_symbol.base_name=tmp_symbol.name;
             tmp_symbol.pretty_name=tmp_symbol.name;
 
diff --git a/src/2ls/show.cpp b/src/2ls/show.cpp
index fe40e9b0e..ea90a8805 100644
--- a/src/2ls/show.cpp
+++ b/src/2ls/show.cpp
@@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/options.h>
 #include <util/find_symbols.h>
-#include <util/i2string.h>
 #include <util/string2int.h>
 
 #include <goto-programs/read_goto_binary.h>
diff --git a/src/2ls/summary_checker_base.cpp b/src/2ls/summary_checker_base.cpp
index 6e7cff796..06d200440 100644
--- a/src/2ls/summary_checker_base.cpp
+++ b/src/2ls/summary_checker_base.cpp
@@ -12,7 +12,6 @@ Author: Peter Schrammel
 #include <iostream>
 
 #include <util/options.h>
-#include <util/i2string.h>
 #include <util/simplify_expr.h>
 #include <langapi/language_util.h>
 #include <util/prefix.h>
diff --git a/src/2ls/summary_checker_nonterm.cpp b/src/2ls/summary_checker_nonterm.cpp
index e7e404d03..e6564719e 100644
--- a/src/2ls/summary_checker_nonterm.cpp
+++ b/src/2ls/summary_checker_nonterm.cpp
@@ -11,7 +11,6 @@ Author: Stefan Marticek
 
 #include "summary_checker_nonterm.h"
 
-#include <util/i2string.h>
 #include <util/simplify_expr.h>
 #include <util/prefix.h>
 
diff --git a/src/2ls/version.h b/src/2ls/version.h
index 467e36dc8..e1bf8e3c4 100644
--- a/src/2ls/version.h
+++ b/src/2ls/version.h
@@ -12,6 +12,6 @@ Author: Peter Schrammel
 #ifndef CPROVER_2LS_2LS_VERSION_H
 #define CPROVER_2LS_2LS_VERSION_H
 
-#define TWOLS_VERSION "0.9.1"
+#define TWOLS_VERSION "0.9.2"
 
 #endif
diff --git a/src/domains/domain.h b/src/domains/domain.h
index 1b6fd060f..f90bac393 100644
--- a/src/domains/domain.h
+++ b/src/domains/domain.h
@@ -16,7 +16,6 @@ Author: Peter Schrammel
 #include <set>
 
 #include <util/std_expr.h>
-#include <util/i2string.h>
 #include <langapi/language_util.h>
 #include <util/replace_expr.h>
 #include <util/namespace.h>
diff --git a/src/domains/incremental_solver.cpp b/src/domains/incremental_solver.cpp
index 063ca9983..09ba49a73 100644
--- a/src/domains/incremental_solver.cpp
+++ b/src/domains/incremental_solver.cpp
@@ -16,7 +16,6 @@ Author: Peter Schrammel
 #include <set>
 
 #include <solvers/flattening/bv_pointers.h>
-#include <util/i2string.h>
 
 #include "incremental_solver.h"
 
@@ -35,7 +34,7 @@ void incremental_solvert::new_context()
     solver->convert(
       symbol_exprt(
         "goto_symex::\\act$"+
-        i2string(activation_literal_counter++), bool_typet()));
+        std::to_string(activation_literal_counter++), bool_typet()));
 
 #ifdef DEBUG_OUTPUT
     debug() << "new context: " << activation_literal<< eom;
diff --git a/src/domains/lexlinrank_domain.cpp b/src/domains/lexlinrank_domain.cpp
index 36cc53d9a..257012efc 100644
--- a/src/domains/lexlinrank_domain.cpp
+++ b/src/domains/lexlinrank_domain.cpp
@@ -14,7 +14,6 @@ Author: Peter Schrammel
 #endif
 
 #include <util/find_symbols.h>
-#include <util/i2string.h>
 #include <util/simplify_expr.h>
 #include <langapi/languages.h>
 #include <goto-symex/adjust_float_expressions.h>
@@ -372,7 +371,7 @@ exprt lexlinrank_domaint::get_row_symb_constraint(
 
     symb_values[elm].c[0]=symbol_exprt(
       SYMB_COEFF_VAR+std::string("c!")+
-      i2string(row)+"$"+i2string(elm)+"$0",
+      std::to_string(row)+"$"+std::to_string(elm)+"$0",
       signedbv_typet(COEFF_C_SIZE));  // coefficients are signed integers
 
 #ifdef DIFFERENCE_ENCODING
@@ -388,7 +387,7 @@ exprt lexlinrank_domaint::get_row_symb_constraint(
     {
       symb_values[elm].c[i]=symbol_exprt(
         SYMB_COEFF_VAR+std::string("c!")+
-        i2string(row)+"$"+i2string(elm)+"$"+i2string(i),
+        std::to_string(row)+"$"+std::to_string(elm)+"$"+std::to_string(i),
         signedbv_typet(COEFF_C_SIZE));
 #ifdef DIFFERENCE_ENCODING
       sum=plus_exprt(
diff --git a/src/domains/linrank_domain.cpp b/src/domains/linrank_domain.cpp
index 4441421ce..e072c6d98 100644
--- a/src/domains/linrank_domain.cpp
+++ b/src/domains/linrank_domain.cpp
@@ -14,7 +14,6 @@ Author: Peter Schrammel
 #endif
 
 #include <util/find_symbols.h>
-#include <util/i2string.h>
 #include <util/simplify_expr.h>
 #include <langapi/languages.h>
 #include <util/cprover_prefix.h>
@@ -231,7 +230,7 @@ exprt linrank_domaint::get_row_symb_constraint(
   symb_values.c.resize(smt_model_values.size()/2);
   assert(!symb_values.c.empty());
   symb_values.c[0]=symbol_exprt(
-    SYMB_COEFF_VAR+std::string("c!")+i2string(row)+"$0",
+    SYMB_COEFF_VAR+std::string("c!")+std::to_string(row)+"$0",
     signedbv_typet(COEFF_C_SIZE));  // coefficients are signed integers
 
 #ifdef DIFFERENCE_ENCODING
@@ -245,7 +244,8 @@ exprt linrank_domaint::get_row_symb_constraint(
   for(unsigned i=1, vals_i=2; i<symb_values.c.size(); ++i, vals_i+=2)
   {
     symb_values.c[i]=symbol_exprt(
-      SYMB_COEFF_VAR+std::string("c!")+i2string(row)+"$"+i2string(i),
+      SYMB_COEFF_VAR+std::string("c!")+std::to_string(row)+"$"+
+      std::to_string(i),
       signedbv_typet(COEFF_C_SIZE));  // coefficients are signed integers
 #ifdef DIFFERENCE_ENCODING
     sum=plus_exprt(
diff --git a/src/domains/predabs_domain.cpp b/src/domains/predabs_domain.cpp
index 7a6fa189b..eb4fce38a 100644
--- a/src/domains/predabs_domain.cpp
+++ b/src/domains/predabs_domain.cpp
@@ -15,7 +15,6 @@ Author: Peter Schrammel
 
 #include <util/find_symbols.h>
 #include <util/prefix.h>
-#include <util/i2string.h>
 #include <util/simplify_expr.h>
 #include <langapi/languages.h>
 
diff --git a/src/domains/strategy_solver_binsearch2.cpp b/src/domains/strategy_solver_binsearch2.cpp
index 4c6fa4ee9..71038dd53 100644
--- a/src/domains/strategy_solver_binsearch2.cpp
+++ b/src/domains/strategy_solver_binsearch2.cpp
@@ -17,8 +17,6 @@ Author: Peter Schrammel
 
 #include <cassert>
 
-#include <util/i2string.h>
-
 #include "strategy_solver_binsearch2.h"
 #include "ssa/local_ssa.h"
 #include "util.h"
@@ -163,7 +161,7 @@ bool strategy_solver_binsearch2t::iterate(invariantt &_inv)
   assert(sum.type()==lower.type());
 
   symbol_exprt sum_bound(
-    SUM_BOUND_VAR+i2string(sum_bound_counter++),
+    SUM_BOUND_VAR+std::to_string(sum_bound_counter++),
     sum.type());
   solver << equal_exprt(sum_bound, sum);
 
diff --git a/src/domains/strategy_solver_binsearch3.cpp b/src/domains/strategy_solver_binsearch3.cpp
index 24d1716ea..c909d0433 100644
--- a/src/domains/strategy_solver_binsearch3.cpp
+++ b/src/domains/strategy_solver_binsearch3.cpp
@@ -15,8 +15,6 @@ Author: Peter Schrammel
 
 #include <cassert>
 
-#include <util/i2string.h>
-
 #include "strategy_solver_binsearch3.h"
 #include "util.h"
 
@@ -164,7 +162,7 @@ bool strategy_solver_binsearch3t::iterate(invariantt &_inv)
   assert(sum.type()==lower.type());
 
   symbol_exprt sum_bound(
-    SUM_BOUND_VAR+i2string(sum_bound_counter++),
+    SUM_BOUND_VAR+std::to_string(sum_bound_counter++),
     sum.type());
   solver << equal_exprt(sum_bound, sum);
 
diff --git a/src/domains/tpolyhedra_domain.cpp b/src/domains/tpolyhedra_domain.cpp
index aa3f8b43e..c5fb71271 100644
--- a/src/domains/tpolyhedra_domain.cpp
+++ b/src/domains/tpolyhedra_domain.cpp
@@ -15,7 +15,6 @@ Author: Peter Schrammel
 #endif
 
 #include <util/find_symbols.h>
-#include <util/i2string.h>
 #include <util/simplify_expr.h>
 
 #include "tpolyhedra_domain.h"
@@ -186,7 +185,7 @@ symbol_exprt tpolyhedra_domaint::get_row_symb_value(const rowt &row)
   assert(row<templ.size());
   auto &row_expr=dynamic_cast<template_row_exprt &>(*templ[row].expr);
   return symbol_exprt(
-    SYMB_BOUND_VAR+i2string(domain_number)+"$"+i2string(row),
+    SYMB_BOUND_VAR+std::to_string(domain_number)+"$"+std::to_string(row),
     row_expr.type());
 }
 
@@ -358,7 +357,7 @@ void tpolyhedra_domaint::rename_for_row(exprt &expr, const rowt &row)
     const std::string &old_id=expr.get_string(ID_identifier);
     if(old_id.find(SYMB_BOUND_VAR)==std::string::npos)
     {
-      irep_idt id=old_id+"_"+i2string(row);
+      irep_idt id=old_id+"_"+std::to_string(row);
       expr.set(ID_identifier, id);
     }
   }
diff --git a/src/solver/summarizer_fw_contexts.cpp b/src/solver/summarizer_fw_contexts.cpp
index 74f225a9d..2b2c4d1cf 100644
--- a/src/solver/summarizer_fw_contexts.cpp
+++ b/src/solver/summarizer_fw_contexts.cpp
@@ -19,7 +19,6 @@ Author: Peter Schrammel
 
 #include <util/xml.h>
 #include <util/xml_expr.h>
-#include <util/i2string.h>
 
 #include "summarizer_fw_contexts.h"
 #include "summary_db.h"
@@ -86,7 +85,7 @@ void summarizer_fw_contextst::inline_summaries(
           xmlt xml_cc("calling-context");
           xml_cc.set_attribute("function", id2string(fname));
           xml_cc.set_attribute(
-            "goto_location", i2string(n_it->location->location_number));
+            "goto_location", std::to_string(n_it->location->location_number));
 
           // location
           const source_locationt &source_location=
diff --git a/src/ssa/dynobj_instance_analysis.cpp b/src/ssa/dynobj_instance_analysis.cpp
index 73efcb772..b240dc1d3 100644
--- a/src/ssa/dynobj_instance_analysis.cpp
+++ b/src/ssa/dynobj_instance_analysis.cpp
@@ -206,7 +206,7 @@ bool dynobj_instance_domaint::merge(
   ai_domain_baset::locationt from,
   ai_domain_baset::locationt to)
 {
-  bool result=false;
+  bool result=has_values.is_false() && !other.has_values.is_false();
   for(auto &obj : other.must_alias_relations)
   {
     if(must_alias_relations.find(obj.first)==must_alias_relations.end())
diff --git a/src/ssa/dynobj_instance_analysis.h b/src/ssa/dynobj_instance_analysis.h
index b381b0652..ff20ab620 100644
--- a/src/ssa/dynobj_instance_analysis.h
+++ b/src/ssa/dynobj_instance_analysis.h
@@ -25,6 +25,7 @@ Description: In some cases, multiple instances must be used so that the
 #include <analyses/ai.h>
 #include <util/union_find.h>
 #include <util/options.h>
+#include <util/threeval.h>
 #include "ssa_object.h"
 #include "ssa_value_set.h"
 
@@ -159,6 +160,28 @@ class dynobj_instance_domaint:public ai_domain_baset
     locationt from,
     locationt to);
 
+  void make_bottom() override
+  {
+    must_alias_relations.clear();
+    live_pointers.clear();
+    has_values=tvt(false);
+  }
+
+  void make_top() override
+  {
+    must_alias_relations.clear();
+    live_pointers.clear();
+    has_values=tvt(true);
+  }
+
+  void make_entry() override
+  {
+    make_top();
+  }
+
+protected:
+  tvt has_values;
+
 private:
   void rhs_concretisation(
     const exprt &guard,
diff --git a/src/ssa/local_ssa.cpp b/src/ssa/local_ssa.cpp
index ad6299fb6..3a75f746f 100644
--- a/src/ssa/local_ssa.cpp
+++ b/src/ssa/local_ssa.cpp
@@ -16,7 +16,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <langapi/language_util.h>
 #endif
 
-#include <util/i2string.h>
 #include <util/prefix.h>
 #include <util/expr_util.h>
 #include <util/decision_procedure.h>
@@ -308,7 +307,7 @@ void local_SSAt::build_phi_nodes(locationt loc)
 exprt local_SSAt::dereference(const exprt &src, locationt loc) const
 {
   const ssa_value_domaint &ssa_value_domain=ssa_value_ai[loc];
-  const std::string nondet_prefix="deref#"+i2string(loc->location_number);
+  const std::string nondet_prefix="deref#"+std::to_string(loc->location_number);
   return ::dereference(
     src, ssa_value_domain, nondet_prefix, ns,
     options.get_bool_option("competition-mode"));
@@ -384,7 +383,8 @@ void local_SSAt::build_function_call(locationt loc)
       exprt deref_lhs=dereference(lhs, loc);
 
       // generate a symbol for rhs
-      irep_idt identifier="ssa::return_value"+i2string(loc->location_number);
+      irep_idt identifier="ssa::return_value"+
+        std::to_string(loc->location_number);
       symbol_exprt rhs(identifier, code_function_call.lhs().type());
 
       assign_rec(deref_lhs, rhs, true_exprt(), loc);
@@ -441,8 +441,8 @@ void local_SSAt::build_function_call(locationt loc)
     for(exprt &a : f.arguments())
     {
       const std::string arg_name=
-        id2string(fname)+"#arg"+i2string(i)+"#"+
-          i2string(loc->location_number);
+        id2string(fname)+"#arg"+std::to_string(i)+"#"+
+          std::to_string(loc->location_number);
       symbol_exprt arg(arg_name, a.type());
       n_it->equalities.push_back(equal_exprt(a, arg));
       a=arg;
@@ -902,8 +902,8 @@ void local_SSAt::replace_side_effects_rec(
       assert(false);
 /*      counter++;
         std::string tmp_suffix=
-        i2string(loc->location_number)+
-        "."+i2string(counter)+suffix;
+        std::to_string(loc->location_number)+
+        "."+std::to_string(counter)+suffix;
         expr=malloc_ssa(side_effect_expr, tmp_suffix, ns);*/
     }
     else
@@ -928,7 +928,7 @@ symbol_exprt local_SSAt::name(
       kind==LOOP_BACK?"lb":
       kind==LOOP_SELECT?"ls":
       kind==OBJECT_SELECT?"os":"")+
-    i2string(cnt)+
+    std::to_string(cnt)+
     (kind==LOOP_SELECT?std::string(""):suffix);
 
 #ifdef DEBUG
@@ -981,8 +981,8 @@ exprt local_SSAt::nondet_symbol(
   exprt s(ID_nondet_symbol, type);
   const irep_idt identifier=
     prefix+
-    i2string(loc->location_number)+
-    "."+i2string(counter)+suffix;
+    std::to_string(loc->location_number)+
+    "."+std::to_string(counter)+suffix;
   s.set(ID_identifier, identifier);
   return s;
 }
diff --git a/src/ssa/malloc_ssa.cpp b/src/ssa/malloc_ssa.cpp
index de353dea2..12f590c52 100644
--- a/src/ssa/malloc_ssa.cpp
+++ b/src/ssa/malloc_ssa.cpp
@@ -14,7 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/arith_tools.h>
 #include <util/expr_util.h>
 #include <util/symbol.h>
-#include <util/i2string.h>
 #include <util/pointer_offset_size.h>
 
 #include <ansi-c/c_types.h>
@@ -70,7 +69,7 @@ exprt create_dynamic_object(
     address_of_object.type()=pointer_typet(value_symbol.type.subtype());
     index_exprt index_expr(value_symbol.type.subtype());
     index_expr.array()=value_symbol.symbol_expr();
-    index_expr.index()=gen_zero(index_type());
+    index_expr.index()=from_integer(0, index_type());
     address_of_object.op0()=index_expr;
   }
   else
@@ -252,7 +251,7 @@ static bool replace_malloc_rec(
 
     expr=malloc_ssa(
       to_side_effect_expr(expr),
-      "$"+i2string(loc_number)+suffix,
+      "$"+std::to_string(loc_number)+suffix,
       symbol_table,
       is_concrete,
       alloc_concrete);
diff --git a/src/ssa/may_alias_analysis.cpp b/src/ssa/may_alias_analysis.cpp
index c7f182a8a..6d8f87082 100644
--- a/src/ssa/may_alias_analysis.cpp
+++ b/src/ssa/may_alias_analysis.cpp
@@ -35,7 +35,7 @@ bool may_alias_domaint::merge(
   ai_domain_baset::locationt from,
   ai_domain_baset::locationt to)
 {
-  bool changed=false;
+  bool changed=has_values.is_false() && !other.has_values.is_false();
 
   // do union
   for(aliasest::const_iterator it=other.aliases.begin();
diff --git a/src/ssa/may_alias_analysis.h b/src/ssa/may_alias_analysis.h
index c1e4adf90..dc2efb3ce 100644
--- a/src/ssa/may_alias_analysis.h
+++ b/src/ssa/may_alias_analysis.h
@@ -14,6 +14,7 @@ Author: Viktor Malik, imalik@fit.vutbr.cz
 
 #include <analyses/ai.h>
 #include <util/union_find.h>
+#include <util/threeval.h>
 #include "ssa_value_set.h"
 
 class may_alias_domaint:public ai_domain_baset
@@ -24,13 +25,31 @@ class may_alias_domaint:public ai_domain_baset
     locationt to,
     ai_baset &ai,
     const namespacet &ns) override;
-
   bool merge(const may_alias_domaint &other, locationt from, locationt to);
 
+  void make_bottom() override
+  {
+    aliases.clear();
+    has_values=tvt(false);
+  }
+
+  void make_top() override
+  {
+    aliases.clear();
+    has_values=tvt(true);
+  }
+
+  void make_entry() override
+  {
+    make_top();
+  }
+
   typedef union_find<irep_idt> aliasest;
   aliasest aliases;
 
 protected:
+  tvt has_values;
+
   void assign_lhs_aliases(
     const exprt &lhs,
     const std::set<irep_idt> &rhs_alias_set);
diff --git a/src/ssa/ssa_dereference.cpp b/src/ssa/ssa_dereference.cpp
index 9bb80bbd4..86a0f7e2b 100644
--- a/src/ssa/ssa_dereference.cpp
+++ b/src/ssa/ssa_dereference.cpp
@@ -134,12 +134,12 @@ bool ssa_may_alias(
   // If one is an array and the other not, consider the elements
   if(t1.id()==ID_array && t2.id()!=ID_array)
     if(ssa_may_alias(
-         index_exprt(e1, gen_zero(index_type()), t1.subtype()), e2, ns))
+         index_exprt(e1, from_integer(0, index_type()), t1.subtype()), e2, ns))
       return true;
 
   if(t2.id()==ID_array && t2.id()!=ID_array)
     if(ssa_may_alias(
-         e1, index_exprt(e2, gen_zero(index_type()), t2.subtype()), ns))
+         e1, index_exprt(e2, from_integer(0, index_type()), t2.subtype()), ns))
       return true;
 
   // Pointers only alias with other pointers,
diff --git a/src/ssa/ssa_domain.cpp b/src/ssa/ssa_domain.cpp
index 42de2f01b..5162cc3a5 100644
--- a/src/ssa/ssa_domain.cpp
+++ b/src/ssa/ssa_domain.cpp
@@ -126,7 +126,7 @@ bool ssa_domaint::merge(
   locationt from,
   locationt to)
 {
-  bool result=false;
+  bool result=has_values.is_false() && !b.has_values.is_false();
 
   // should traverse both maps simultaneously
   for(def_mapt::const_iterator
diff --git a/src/ssa/ssa_domain.h b/src/ssa/ssa_domain.h
index b3a4d8d4f..aa1f74ef1 100644
--- a/src/ssa/ssa_domain.h
+++ b/src/ssa/ssa_domain.h
@@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #define CPROVER_2LS_SSA_SSA_DOMAIN_H
 
 #include <analyses/ai.h>
+#include <util/threeval.h>
 
 #include "assignments.h"
 
@@ -90,8 +91,28 @@ class ssa_domaint:public ai_domain_baset
     locationt from,
     locationt to);
 
+  void make_bottom() override
+  {
+    phi_nodes.clear();
+    def_map.clear();
+    has_values=tvt(false);
+  }
+  void make_top() override
+  {
+    phi_nodes.clear();
+    def_map.clear();
+    has_values=tvt(true);
+  }
+  void make_entry() override
+  {
+    has_values=tvt(true);
+  }
+
+protected:
+  tvt has_values;
+
 private:
-  static std::map<dstring, ssa_domaint::def_entryt>::const_iterator
+  static std::map<dstringt, ssa_domaint::def_entryt>::const_iterator
   get_object_allocation_def(
     const irep_idt &id,
     const def_mapt &def_map);
diff --git a/src/ssa/ssa_inliner.cpp b/src/ssa/ssa_inliner.cpp
index 3ca76aab3..375530e81 100644
--- a/src/ssa/ssa_inliner.cpp
+++ b/src/ssa/ssa_inliner.cpp
@@ -11,7 +11,6 @@ Author: Peter Schrammel
 
 #include <algorithm>
 
-#include <util/i2string.h>
 #include <util/replace_expr.h>
 
 #include "ssa_inliner.h"
@@ -736,7 +735,7 @@ void ssa_inlinert::rename(exprt &expr)
   if(expr.id()==ID_symbol)
   {
     symbol_exprt &sexpr=to_symbol_expr(expr);
-    irep_idt id=id2string(sexpr.get_identifier())+"@"+i2string(counter);
+    irep_idt id=id2string(sexpr.get_identifier())+"@"+std::to_string(counter);
     sexpr.set_identifier(id);
   }
   else if(expr.id()==ID_address_of)
@@ -751,7 +750,7 @@ void ssa_inlinert::rename(exprt &expr)
       else
         id=id2string(obj_id)+"'addr";
 
-      id=id2string(id)+"@"+i2string(counter);
+      id=id2string(id)+"@"+std::to_string(counter);
     }
     symbol_exprt addr_symbol(id, expr.type());
     expr=addr_symbol;
@@ -811,7 +810,9 @@ void ssa_inlinert::rename_to_caller(
 #endif
       replace_map[*it]=
         symbol_exprt(
-          id2string(it->get_identifier())+"@"+i2string(++counter), it->type());
+          id2string(
+            it->get_identifier())+"@"+std::to_string(++counter),
+            it->type());
     }
   }
 
diff --git a/src/ssa/ssa_unwinder.cpp b/src/ssa/ssa_unwinder.cpp
index 8fa42c69b..bc20805ff 100644
--- a/src/ssa/ssa_unwinder.cpp
+++ b/src/ssa/ssa_unwinder.cpp
@@ -13,7 +13,6 @@ Author: Peter Schrammel, Saurabh Joshi
 #define COMPETITION
 
 #include <util/prefix.h>
-#include <util/i2string.h>
 
 #include "ssa_unwinder.h"
 
@@ -229,7 +228,7 @@ void ssa_local_unwindert::unwind(unsigned k)
 
   current_enabling_expr=
     symbol_exprt(
-      "unwind::"+id2string(fname)+"::enable"+i2string(k),
+      "unwind::"+id2string(fname)+"::enable"+std::to_string(k),
       bool_typet());
   SSA.enabling_exprs.push_back(current_enabling_expr);
 
@@ -620,12 +619,12 @@ void ssa_local_unwindert::unwinder_rename(
   unsigned unwinding=pre ? SSA.current_unwinding : 0;
   if(pos==pos1)
   {
-    suffix="%"+i2string(unwinding);
+    suffix="%"+std::to_string(unwinding);
   }
   else
   {
     suffix=id.substr(pos, pos1-pos);
-    suffix+="%"+i2string(unwinding);
+    suffix+="%"+std::to_string(unwinding);
   }
 
   var.set_identifier(id2string(var.get_identifier())+suffix);
diff --git a/src/ssa/ssa_value_set.cpp b/src/ssa/ssa_value_set.cpp
index 2a3d59096..6dd4a73fe 100644
--- a/src/ssa/ssa_value_set.cpp
+++ b/src/ssa/ssa_value_set.cpp
@@ -29,6 +29,8 @@ void ssa_value_domaint::transform(
   ai_baset &ai,
   const namespacet &ns)
 {
+  if(has_values.is_false())
+    return;
   competition_mode=static_cast<ssa_value_ait &>(ai).options
     .get_bool_option("competition-mode");
   if(from->is_assign())
@@ -527,7 +529,8 @@ bool ssa_value_domaint::merge(
 {
   value_mapt::iterator v_it=value_map.begin();
   const value_mapt &new_value_map=other.value_map;
-  bool result=false;
+  bool result=has_values.is_false() && !other.has_values.is_false();
+  has_values=tvt::unknown();
 
   for(value_mapt::const_iterator
         it=new_value_map.begin();
diff --git a/src/ssa/ssa_value_set.h b/src/ssa/ssa_value_set.h
index 7b4a13908..eb3cf26fb 100644
--- a/src/ssa/ssa_value_set.h
+++ b/src/ssa/ssa_value_set.h
@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <analyses/ai.h>
 #include <util/options.h>
+#include <util/threeval.h>
 
 #include "ssa_object.h"
 
@@ -27,6 +28,23 @@ class ssa_value_domaint:public ai_domain_baset
     const namespacet &) const;
   bool merge(const ssa_value_domaint &, locationt, locationt);
 
+  void make_bottom() override
+  {
+    value_map.clear();
+    has_values=tvt(false);
+  }
+
+  void make_top() override
+  {
+    value_map.clear();
+    has_values=tvt(true);
+  }
+
+  void make_entry() override
+  {
+    make_top();
+  }
+
   struct valuest
   {
   public:
@@ -78,6 +96,8 @@ class ssa_value_domaint:public ai_domain_baset
   }
 
 protected:
+  tvt has_values;
+
   void assign_lhs_rec(
     const exprt &lhs,
     const exprt &rhs,
diff --git a/src/ssa/unwindable_local_ssa.cpp b/src/ssa/unwindable_local_ssa.cpp
index 78b1ef588..44762c0e9 100644
--- a/src/ssa/unwindable_local_ssa.cpp
+++ b/src/ssa/unwindable_local_ssa.cpp
@@ -13,7 +13,6 @@ Author: Peter Schrammel, Saurabh Joshi
 
 #include <limits>
 
-#include <util/i2string.h>
 #include <util/find_symbols.h>
 #include <util/rename_symbol.h>
 #include <util/string2int.h>
@@ -185,8 +184,8 @@ exprt unwindable_local_SSAt::nondet_symbol(
   exprt s(ID_nondet_symbol, type);
   const irep_idt identifier=
     prefix+
-    i2string(loc->location_number)+
-    "."+i2string(counter)+unwind_suffix+suffix;
+    std::to_string(loc->location_number)+
+    "."+std::to_string(counter)+unwind_suffix+suffix;
   s.set(ID_identifier, identifier);
 
 #if 0