diff --git a/lib/cbmc b/lib/cbmc
index 37c42b669..18fef2504 160000
--- a/lib/cbmc
+++ b/lib/cbmc
@@ -1 +1 @@
-Subproject commit 37c42b669d5b7db5da7acb2c7b4fa3791ff661a9
+Subproject commit 18fef25049bc2ddbc426000e892f974eab14934e
diff --git a/regression/memsafety/built_from_end_false/test.desc b/regression/memsafety/built_from_end_false/test.desc
index e100b955f..db3c4b8ba 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.15\] dereference failure: deallocated dynamic object in \*p: FAILURE
+\[main.pointer_dereference.17\] dereference failure: deallocated dynamic object in \*\(\(List\)\(char \*\)\(\(char \*\)p \+ \(signed long int\)8ul\)\): FAILURE
diff --git a/regression/memsafety/simple_false/test.desc b/regression/memsafety/simple_false/test.desc
index f091cf7f8..ca06506c2 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.33\] dereference failure: deallocated dynamic object in \*p: FAILURE
+\[main.pointer_dereference.38\] dereference failure: deallocated dynamic object in \*\(\(List\)\(char \*\)\(\(char \*\)p \+ \(signed long int\)8ul\)\): FAILURE
diff --git a/src/2ls/2ls_parse_options.cpp b/src/2ls/2ls_parse_options.cpp
index a61a9ea19..09ffda976 100644
--- a/src/2ls/2ls_parse_options.cpp
+++ b/src/2ls/2ls_parse_options.cpp
@@ -39,6 +39,7 @@ Author: Daniel Kroening, Peter Schrammel
 #include <goto-programs/remove_skip.h>
 #include <goto-programs/show_symbol_table.h>
 #include <goto-programs/initialize_goto_model.h>
+#include <goto-programs/show_goto_functions.h>
 
 #include <analyses/goto_check.h>
 
@@ -899,11 +900,11 @@ bool twols_parse_optionst::get_goto_program(
 
   try
   {
-    goto_model=initialize_goto_model(cmdline, ui_message_handler);
+    goto_model=initialize_goto_model(cmdline.args, ui_message_handler, options);
 
     if(cmdline.isset("show-symbol-table"))
     {
-      show_symbol_table(goto_model, ui_message_handler.get_ui());
+      show_symbol_table(goto_model.symbol_table, ui_message_handler);
       return true;
     }
 
@@ -1140,8 +1141,11 @@ bool twols_parse_optionst::process_goto_program(
     // show it?
     if(cmdline.isset("show-goto-functions"))
     {
-      const namespacet ns(goto_model.symbol_table);
-      goto_model.goto_functions.output(ns, std::cout);
+      show_goto_functions(
+        goto_model,
+        get_message_handler(),
+        ui_message_handler.get_ui(),
+        false);
       return true;
     }
   }
@@ -1282,7 +1286,7 @@ void twols_parse_optionst::show_counterexample(
   {
   case ui_message_handlert::uit::PLAIN:
     std::cout << std::endl << "Counterexample:" << std::endl;
-    show_goto_trace(std::cout, ns, error_trace);
+    show_goto_trace(result(), ns, error_trace);
     break;
 
   case ui_message_handlert::uit::XML_UI:
diff --git a/src/2ls/horn_encoding.cpp b/src/2ls/horn_encoding.cpp
index 8045d8e81..058d8ed73 100644
--- a/src/2ls/horn_encoding.cpp
+++ b/src/2ls/horn_encoding.cpp
@@ -65,7 +65,7 @@ void horn_encodingt::translate(
          ";\n";
 
   // compute SSA
-  local_SSAt local_SSA(f_it->second, symbol_table, options, "");
+  local_SSAt local_SSA(f_it->first, f_it->second, symbol_table, options, "");
 
   const goto_programt &body=f_it->second.body;
 
diff --git a/src/2ls/preprocessing_util.cpp b/src/2ls/preprocessing_util.cpp
index 969b50b72..a4c53df75 100644
--- a/src/2ls/preprocessing_util.cpp
+++ b/src/2ls/preprocessing_util.cpp
@@ -59,7 +59,7 @@ void twols_parse_optionst::propagate_constants(goto_modelt &goto_model)
   namespacet ns(goto_model.symbol_table);
   Forall_goto_functions(f_it, goto_model.goto_functions)
   {
-    constant_propagator_ait(f_it->second, ns);
+    constant_propagator_ait(f_it->first, f_it->second, ns);
   }
 }
 
@@ -627,9 +627,9 @@ std::map<symbol_exprt, size_t> twols_parse_optionst::split_dynamic_objects(
     if(!f_it->second.body_available())
       continue;
     namespacet ns(goto_model.symbol_table);
-    ssa_value_ait value_analysis(f_it->second, ns, options);
+    ssa_value_ait value_analysis(f_it->first, f_it->second, ns, options);
     dynobj_instance_analysist do_inst(
-      f_it->second, ns, options, value_analysis);
+      f_it->first, f_it->second, ns, options, value_analysis);
 
     compute_dynobj_instances(
       f_it->second.body, do_inst, dynobj_instances, ns);
diff --git a/src/2ls/show.cpp b/src/2ls/show.cpp
index ea90a8805..959e62e0d 100644
--- a/src/2ls/show.cpp
+++ b/src/2ls/show.cpp
@@ -29,13 +29,14 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "show.h"
 
 void show_assignments(
+  const irep_idt &function_identifier,
   const goto_functionst::goto_functiont &goto_function,
   const namespacet &ns,
   const optionst &options,
   std::ostream &out)
 {
   ssa_objectst ssa_objects(goto_function, ns);
-  ssa_value_ait ssa_value_ai(goto_function, ns, options);
+  ssa_value_ait ssa_value_ai(function_identifier, goto_function, ns, options);
   assignmentst assignments(
     goto_function.body,
     ns,
@@ -61,7 +62,7 @@ void show_assignments(
     if(f_it==goto_model.goto_functions.function_map.end())
       out << "function " << function << " not found\n";
     else
-      show_assignments(f_it->second, ns, options, out);
+      show_assignments(f_it->first, f_it->second, ns, options, out);
   }
   else
   {
@@ -69,7 +70,7 @@ void show_assignments(
     {
       out << ">>>> Function " << f_it->first << "\n";
 
-      show_assignments(f_it->second, ns, options, out);
+      show_assignments(f_it->first, f_it->second, ns, options, out);
 
       out << "\n";
     }
@@ -77,13 +78,14 @@ void show_assignments(
 }
 
 void show_defs(
+  const irep_idt &function_identifier,
   const goto_functionst::goto_functiont &goto_function,
   const namespacet &ns,
   const optionst &options,
   std::ostream &out)
 {
   ssa_objectst ssa_objects(goto_function, ns);
-  ssa_value_ait ssa_value_ai(goto_function, ns, options);
+  ssa_value_ait ssa_value_ai(function_identifier, goto_function, ns, options);
   assignmentst assignments(
     goto_function.body,
     ns,
@@ -91,7 +93,7 @@ void show_defs(
     ssa_objects,
     ssa_value_ai);
   ssa_ait ssa_analysis(assignments);
-  ssa_analysis(goto_function, ns);
+  ssa_analysis(function_identifier, goto_function, ns);
   ssa_analysis.output(ns, goto_function.body, out);
 }
 
@@ -111,7 +113,7 @@ void show_defs(
     if(f_it==goto_model.goto_functions.function_map.end())
       out << "function " << function << " not found\n";
     else
-      show_defs(f_it->second, ns, options, out);
+      show_defs(f_it->first, f_it->second, ns, options, out);
   }
   else
   {
@@ -119,7 +121,7 @@ void show_defs(
     {
       out << ">>>> Function " << f_it->first << "\n";
 
-      show_defs(f_it->second, ns, options, out);
+      show_defs(f_it->first, f_it->second, ns, options, out);
 
       out << "\n";
     }
@@ -166,6 +168,7 @@ void show_guards(
 }
 
 void show_ssa(
+  const irep_idt &function_identifier,
   const goto_functionst::goto_functiont &goto_function,
   bool simplify,
   const symbol_tablet &symbol_table,
@@ -175,7 +178,11 @@ void show_ssa(
   if(!goto_function.body_available())
     return;
 
-  unwindable_local_SSAt local_SSA(goto_function, symbol_table, options);
+  unwindable_local_SSAt local_SSA(
+    function_identifier,
+    goto_function,
+    symbol_table,
+    options);
   if(simplify)
     ::simplify(local_SSA, local_SSA.ns);
   local_SSA.output_verbose(out);
@@ -197,7 +204,13 @@ void show_ssa(
     if(f_it==goto_model.goto_functions.function_map.end())
       out << "function " << function << " not found\n";
     else
-      show_ssa(f_it->second, simplify, goto_model.symbol_table, options, out);
+      show_ssa(
+        f_it->first,
+        f_it->second,
+        simplify,
+        goto_model.symbol_table,
+        options,
+        out);
   }
   else
   {
@@ -210,7 +223,13 @@ void show_ssa(
 
       out << ">>>> Function " << f_it->first << "\n";
 
-      show_ssa(f_it->second, simplify, goto_model.symbol_table, options, out);
+      show_ssa(
+        f_it->first,
+        f_it->second,
+        simplify,
+        goto_model.symbol_table,
+        options,
+        out);
 
       out << "\n";
     }
@@ -383,13 +402,14 @@ void show_ssa_symbols(
 }
 
 void show_value_set(
+  const irep_idt &function_identifier,
   const goto_functionst::goto_functiont &goto_function,
   const namespacet &ns,
   const optionst &options,
   std::ostream &out)
 {
   ssa_objectst ssa_objects(goto_function, ns);
-  ssa_value_ait ssa_value_ai(goto_function, ns, options);
+  ssa_value_ait ssa_value_ai(function_identifier, goto_function, ns, options);
   ssa_value_ai.output(ns, goto_function, out);
 }
 
@@ -409,7 +429,7 @@ void show_value_sets(
     if(f_it==goto_model.goto_functions.function_map.end())
       out << "function " << function << " not found\n";
     else
-      show_value_set(f_it->second, ns, options, out);
+      show_value_set(f_it->first, f_it->second, ns, options, out);
   }
   else
   {
@@ -417,7 +437,7 @@ void show_value_sets(
     {
       out << ">>>> Function " << f_it->first << "\n";
 
-      show_value_set(f_it->second, ns, options, out);
+      show_value_set(f_it->first, f_it->second, ns, options, out);
 
       out << "\n";
     }
diff --git a/src/2ls/summary_checker_base.cpp b/src/2ls/summary_checker_base.cpp
index 5d88b19c3..42ae807e5 100644
--- a/src/2ls/summary_checker_base.cpp
+++ b/src/2ls/summary_checker_base.cpp
@@ -16,6 +16,7 @@ Author: Peter Schrammel
 #include <langapi/language_util.h>
 #include <util/prefix.h>
 #include <goto-programs/write_goto_binary.h>
+#include <goto-programs/show_goto_functions.h>
 
 #include <solvers/sat/satcheck.h>
 #include <solvers/flattening/bv_pointers.h>
@@ -501,7 +502,11 @@ void summary_checker_baset::instrument_and_output(
   instrument_gotot instrument_goto(options, ssa_db, summary_db);
   instrument_goto(goto_model);
   if(verbosity==10)
-    goto_model.output(std::cout);
+    show_goto_functions(
+      goto_model,
+      get_message_handler(),
+      ui_message_handlert::uit::PLAIN,
+      false);
   std::string filename=options.get_option("instrument-output");
   status() << "Writing instrumented goto-binary " << filename << eom;
   write_goto_binary(
diff --git a/src/2ls/version.h b/src/2ls/version.h
index 991ed7c0b..987421874 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.4"
+#define TWOLS_VERSION "0.9.5"
 
 #endif
diff --git a/src/ssa/dynobj_instance_analysis.cpp b/src/ssa/dynobj_instance_analysis.cpp
index 1bb858799..c1bf1976a 100644
--- a/src/ssa/dynobj_instance_analysis.cpp
+++ b/src/ssa/dynobj_instance_analysis.cpp
@@ -119,7 +119,9 @@ void dynobj_instance_domaint::rhs_concretisation(
 }
 
 void dynobj_instance_domaint::transform(
+  const irep_idt &function_from,
   ai_domain_baset::locationt from,
+  const irep_idt &function_to,
   ai_domain_baset::locationt to,
   ai_baset &ai,
   const namespacet &ns)
diff --git a/src/ssa/dynobj_instance_analysis.h b/src/ssa/dynobj_instance_analysis.h
index 929b8dc27..c47017228 100644
--- a/src/ssa/dynobj_instance_analysis.h
+++ b/src/ssa/dynobj_instance_analysis.h
@@ -151,7 +151,9 @@ class dynobj_instance_domaint:public ai_domain_baset
   std::map<symbol_exprt, std::set<exprt>> live_pointers;
 
   void transform(
+    const irep_idt &,
     locationt from,
+    const irep_idt &,
     locationt to,
     ai_baset &ai,
     const namespacet &ns) override;
@@ -208,6 +210,7 @@ class dynobj_instance_analysist:public ait<dynobj_instance_domaint>
 {
 public:
   dynobj_instance_analysist(
+    const irep_idt &function_identifier,
     const goto_functionst::goto_functiont &goto_function,
     const namespacet &ns,
     const optionst &_options,
@@ -215,7 +218,7 @@ class dynobj_instance_analysist:public ait<dynobj_instance_domaint>
     options(_options),
     value_analysis(_value_ai)
   {
-    operator()(goto_function, ns);
+    operator()(function_identifier, goto_function, ns);
   }
 
 protected:
diff --git a/src/ssa/local_ssa.cpp b/src/ssa/local_ssa.cpp
index 0fbfa6e0e..4ee061c81 100644
--- a/src/ssa/local_ssa.cpp
+++ b/src/ssa/local_ssa.cpp
@@ -30,7 +30,7 @@ Author: Daniel Kroening, kroening@kroening.com
 void local_SSAt::build_SSA()
 {
   // perform SSA data-flow analysis
-  ssa_analysis(goto_function, ns);
+  ssa_analysis(function_identifier, goto_function, ns);
 
   forall_goto_program_instructions(i_it, goto_function.body)
   {
@@ -414,10 +414,10 @@ void local_SSAt::build_function_call(locationt loc)
     }
 
     // turn function call into expression
-    function_application_exprt f;
-    f.function()=to_symbol_expr(code_function_call.function());
-    f.type()=code_function_call.lhs().type();
-    f.arguments()=code_function_call.arguments();
+    function_application_exprt f(
+      to_symbol_expr(code_function_call.function()),
+      code_function_call.arguments(),
+      code_function_call.lhs().type());
 
     // access to "new" value in template declarations
     if(code_function_call.function().id()==ID_symbol &&
diff --git a/src/ssa/local_ssa.h b/src/ssa/local_ssa.h
index 850aee994..05381ec0e 100644
--- a/src/ssa/local_ssa.h
+++ b/src/ssa/local_ssa.h
@@ -37,21 +37,23 @@ class local_SSAt
   typedef goto_programt::const_targett locationt;
 
   inline local_SSAt(
+    const irep_idt &_function_identifier,
     const goto_functiont &_goto_function,
     const symbol_tablet &_symbol_table,
     const optionst &_options,
     const std::string &_suffix=""):
     ns(_symbol_table), goto_function(_goto_function), options(_options),
     ssa_objects(_goto_function, ns),
-    ssa_value_ai(_goto_function, ns, options),
+    ssa_value_ai(_function_identifier, _goto_function, ns, options),
     assignments(
       _goto_function.body,
       ns,
       options,
       ssa_objects,
       ssa_value_ai),
-    alias_analysis(_goto_function, ns),
+    alias_analysis(_function_identifier, _goto_function, ns),
     guard_map(_goto_function.body),
+    function_identifier(_function_identifier),
     ssa_analysis(assignments),
     suffix(_suffix)
   {
@@ -242,6 +244,7 @@ class local_SSAt
 // protected:
   guard_mapt guard_map;
 
+  const irep_idt &function_identifier;
   ssa_ait ssa_analysis;
   std::string suffix; // an extra suffix
 
diff --git a/src/ssa/malloc_ssa.cpp b/src/ssa/malloc_ssa.cpp
index 15d41943a..37ba76584 100644
--- a/src/ssa/malloc_ssa.cpp
+++ b/src/ssa/malloc_ssa.cpp
@@ -163,23 +163,26 @@ exprt malloc_ssa(
       if(tmp_type.is_not_nil())
       {
         // Did the size get multiplied?
-        mp_integer elem_size=pointer_offset_size(tmp_type, ns);
-        mp_integer alloc_size;
-        if(elem_size<0 || to_integer(size, alloc_size))
+        if(auto maybe_elem_size=pointer_offset_size(tmp_type, ns))
         {
-        }
-        else
-        {
-          if(alloc_size==elem_size)
-            object_type=tmp_type;
+          mp_integer alloc_size;
+          mp_integer elem_size=*maybe_elem_size;
+          if(elem_size<0 || to_integer(size, alloc_size))
+          {
+          }
           else
           {
-            mp_integer elements=alloc_size/elem_size;
+            if(alloc_size==elem_size)
+              object_type=tmp_type;
+            else
+            {
+              mp_integer elements=alloc_size/elem_size;
 
-            if(elements*elem_size==alloc_size)
-              object_type=array_typet(
-                tmp_type,
-                from_integer(elements, size.type()));
+              if(elements*elem_size==alloc_size)
+                object_type=array_typet(
+                  tmp_type,
+                  from_integer(elements, size.type()));
+            }
           }
         }
       }
@@ -326,7 +329,10 @@ bool replace_malloc(
             namespacet ns(goto_model.symbol_table);
             goto_functionst::goto_functiont function_copy;
             function_copy.copy_from(f_it->second);
-            constant_propagator_ait const_propagator(function_copy, ns);
+            constant_propagator_ait const_propagator(
+              f_it->first,
+              function_copy,
+              ns);
             forall_goto_program_instructions(copy_i_it, function_copy.body)
             {
               if(copy_i_it->location_number==i_it->location_number)
diff --git a/src/ssa/may_alias_analysis.cpp b/src/ssa/may_alias_analysis.cpp
index 6d8f87082..ab9d43cec 100644
--- a/src/ssa/may_alias_analysis.cpp
+++ b/src/ssa/may_alias_analysis.cpp
@@ -12,7 +12,9 @@ Author: Viktor Malik, imalik@fit.vutbr.cz
 #include "may_alias_analysis.h"
 
 void may_alias_domaint::transform(
+  const irep_idt &from_function,
   ai_domain_baset::locationt from,
+  const irep_idt &to_function,
   ai_domain_baset::locationt to,
   ai_baset &ai,
   const namespacet &ns)
diff --git a/src/ssa/may_alias_analysis.h b/src/ssa/may_alias_analysis.h
index 832d58390..4d14f13e9 100644
--- a/src/ssa/may_alias_analysis.h
+++ b/src/ssa/may_alias_analysis.h
@@ -21,7 +21,9 @@ class may_alias_domaint:public ai_domain_baset
 {
 public:
   void transform(
+    const irep_idt &,
     locationt from,
+    const irep_idt &,
     locationt to,
     ai_baset &ai,
     const namespacet &ns) override;
@@ -73,10 +75,11 @@ class may_alias_analysist:public ait<may_alias_domaint>
 {
 public:
   may_alias_analysist(
+    const irep_idt &function_identifier,
     const goto_functionst::goto_functiont &goto_function,
     const namespacet &ns)
   {
-    operator()(goto_function, ns);
+    operator()(function_identifier, goto_function, ns);
   }
 };
 
diff --git a/src/ssa/ssa_build_goto_trace.cpp b/src/ssa/ssa_build_goto_trace.cpp
index d8161104a..c8500e624 100644
--- a/src/ssa/ssa_build_goto_trace.cpp
+++ b/src/ssa/ssa_build_goto_trace.cpp
@@ -208,16 +208,16 @@ bool ssa_build_goto_tracet::record_step(
     if(!can_convert_ssa_expr(lhs_simplified))
       break;
 
-    step.lhs_object=ssa_exprt(lhs_simplified);
-    step.lhs_object_value=rhs_simplified;
+    step.full_lhs=ssa_exprt(lhs_simplified);
+    step.full_lhs_value=rhs_simplified;
 
     // skip unresolved lhs
-    if(step.lhs_object.is_nil())
+    if(step.full_lhs.is_nil())
       break;
 
     // skip strings (for SV-COMP)
-    if(step.lhs_object.type().id()==ID_pointer &&
-       to_pointer_type(step.lhs_object.type()).subtype().id()==ID_signedbv)
+    if(step.full_lhs.type().id()==ID_pointer &&
+       to_pointer_type(step.full_lhs.type()).subtype().id()==ID_signedbv)
       break;
 
     // skip undetermined rhs
diff --git a/src/ssa/ssa_db.h b/src/ssa/ssa_db.h
index f64d61e4d..603e70fc8 100644
--- a/src/ssa/ssa_db.h
+++ b/src/ssa/ssa_db.h
@@ -70,7 +70,11 @@ class ssa_dbt
     const symbol_tablet &symbol_table)
   {
     store[function_name]=
-      new unwindable_local_SSAt(goto_function, symbol_table, options);
+      new unwindable_local_SSAt(
+        function_name,
+        goto_function,
+        symbol_table,
+        options);
   }
 
 protected:
diff --git a/src/ssa/ssa_dereference.cpp b/src/ssa/ssa_dereference.cpp
index 343460633..c63a4b06b 100644
--- a/src/ssa/ssa_dereference.cpp
+++ b/src/ssa/ssa_dereference.cpp
@@ -195,17 +195,22 @@ exprt ssa_alias_guard(
 
   // in some cases, we can use plain address equality,
   // as we assume well-aligned-ness
-  mp_integer size1=pointer_offset_size(e1.type(), ns);
-  mp_integer size2=pointer_offset_size(e2.type(), ns);
+  auto maybe_size1=pointer_offset_size(e1.type(), ns);
+  auto maybe_size2=pointer_offset_size(e2.type(), ns);
 
-  if(size1>=size2)
+  if(maybe_size1 && maybe_size2)
   {
-    exprt lhs=a1;
-    exprt rhs=a2;
-    if(ns.follow(rhs.type())!=ns.follow(lhs.type()))
-      rhs=typecast_exprt(rhs, lhs.type());
+    mp_integer size1=*maybe_size1;
+    mp_integer size2=*maybe_size2;
+    if(size1>=size2)
+    {
+      exprt lhs=a1;
+      exprt rhs=a2;
+      if(ns.follow(rhs.type())!=ns.follow(lhs.type()))
+        rhs=typecast_exprt(rhs, lhs.type());
 
-    return equal_exprt(lhs, rhs);
+      return equal_exprt(lhs, rhs);
+    }
   }
 
   return same_object(a1, a2);
@@ -235,15 +240,17 @@ exprt ssa_alias_value(
   {
     // this assumes well-alignedness
 
-    mp_integer element_size=pointer_offset_size(e2_type.subtype(), ns);
-
-    if(element_size==1)
-      return index_exprt(e2, offset1, e1.type());
-    else if(element_size>1)
+    if(auto maybe_element_size=pointer_offset_size(e2_type.subtype(), ns))
     {
-      exprt index=
-        div_exprt(offset1, from_integer(element_size, offset1.type()));
-      return index_exprt(e2, index, e1.type());
+      mp_integer element_size=*maybe_element_size;
+      if(element_size==1)
+        return index_exprt(e2, offset1, e1.type());
+      else if(element_size>1)
+      {
+        exprt index=
+          div_exprt(offset1, from_integer(element_size, offset1.type()));
+        return index_exprt(e2, index, e1.type());
+      }
     }
   }
 
diff --git a/src/ssa/ssa_domain.cpp b/src/ssa/ssa_domain.cpp
index 5162cc3a5..0130a6280 100644
--- a/src/ssa/ssa_domain.cpp
+++ b/src/ssa/ssa_domain.cpp
@@ -52,7 +52,9 @@ void ssa_domaint::output(
 }
 
 void ssa_domaint::transform(
+  const irep_idt &from_function,
   locationt from,
+  const irep_idt &to_function,
   locationt to,
   ai_baset &ai,
   const namespacet &ns)
diff --git a/src/ssa/ssa_domain.h b/src/ssa/ssa_domain.h
index 27cbab031..9950c7668 100644
--- a/src/ssa/ssa_domain.h
+++ b/src/ssa/ssa_domain.h
@@ -76,7 +76,9 @@ class ssa_domaint:public ai_domain_baset
   phi_nodest phi_nodes;
 
   virtual void transform(
+    const irep_idt &,
     locationt from,
+    const irep_idt &,
     locationt to,
     ai_baset &ai,
     const namespacet &ns);
diff --git a/src/ssa/ssa_value_set.cpp b/src/ssa/ssa_value_set.cpp
index 6dd4a73fe..9f078a9bb 100644
--- a/src/ssa/ssa_value_set.cpp
+++ b/src/ssa/ssa_value_set.cpp
@@ -24,7 +24,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "ssa_pointed_objects.h"
 
 void ssa_value_domaint::transform(
+  const irep_idt &function_from,
   locationt from,
+  const irep_idt &function_to,
   locationt to,
   ai_baset &ai,
   const namespacet &ns)
@@ -301,13 +303,18 @@ void ssa_value_domaint::assign_rhs_rec(
     {
       if(it->type().id()==ID_pointer)
       {
-        mp_integer pointer_offset=pointer_offset_size(it->type().subtype(), ns);
-        if(pointer_offset<1)
-          pointer_offset=1;
-        unsigned a=merge_alignment(integer2ulong(pointer_offset), alignment);
-        assign_rhs_rec(dest, *it, ns, true, a);
+        if(auto maybe_pointer_offset=pointer_offset_size(
+          it->type().subtype(),
+          ns))
+        {
+          mp_integer pointer_offset=*maybe_pointer_offset;
+          if(pointer_offset<1)
+            pointer_offset=1;
+          unsigned a=merge_alignment(integer2ulong(pointer_offset), alignment);
+          assign_rhs_rec(dest, *it, ns, true, a);
 
-        pointer=true;
+          pointer=true;
+        }
       }
       else if(it->type().id()==ID_unsignedbv || it->type().id()==ID_signedbv)
       {
@@ -323,16 +330,20 @@ void ssa_value_domaint::assign_rhs_rec(
     assert(rhs.operands().size()==2);
     if(rhs.type().id()==ID_pointer)
     {
-      mp_integer pointer_offset=pointer_offset_size(rhs.type().subtype(), ns);
-      if(pointer_offset<1)
-        pointer_offset=1;
-      unsigned a=merge_alignment(integer2ulong(pointer_offset), alignment);
-      assign_rhs_rec(dest, rhs.op0(), ns, true, a);
-
-      if(competition_mode)
-        assert(
-          !(rhs.op1().type().id()==ID_unsignedbv ||
-            rhs.op1().type().id()==ID_signedbv));
+      if(auto maybe_pointer_offset=
+        pointer_offset_size(rhs.type().subtype(), ns))
+      {
+        mp_integer pointer_offset=*maybe_pointer_offset;
+        if(pointer_offset<1)
+          pointer_offset=1;
+        unsigned a=merge_alignment(integer2ulong(pointer_offset), alignment);
+        assign_rhs_rec(dest, rhs.op0(), ns, true, a);
+
+        if(competition_mode)
+          assert(
+            !(rhs.op1().type().id()==ID_unsignedbv ||
+              rhs.op1().type().id()==ID_signedbv));
+      }
     }
   }
   else if(rhs.id()==ID_dereference)
@@ -397,10 +408,13 @@ void ssa_value_domaint::assign_rhs_rec_address_of(
     if(!to_index_expr(rhs).index().is_zero())
     {
       offset=true;
-      mp_integer pointer_offset=pointer_offset_size(rhs.type(), ns);
-      if(pointer_offset<1)
-        pointer_offset=1;
-      a=merge_alignment(a, integer2ulong(pointer_offset));
+      if(auto maybe_pointer_offset=pointer_offset_size(rhs.type(), ns))
+      {
+        mp_integer pointer_offset=*maybe_pointer_offset;
+        if(pointer_offset<1)
+          pointer_offset=1;
+        a=merge_alignment(a, integer2ulong(pointer_offset));
+      }
     }
 
     assign_rhs_rec_address_of(dest, to_index_expr(rhs).array(), ns, offset, a);
diff --git a/src/ssa/ssa_value_set.h b/src/ssa/ssa_value_set.h
index 056530c12..5ed06e4a5 100644
--- a/src/ssa/ssa_value_set.h
+++ b/src/ssa/ssa_value_set.h
@@ -21,11 +21,17 @@ Author: Daniel Kroening, kroening@kroening.com
 class ssa_value_domaint:public ai_domain_baset
 {
 public:
-  virtual void transform(locationt, locationt, ai_baset &, const namespacet &);
-  virtual void output(
+  void transform(
+    const irep_idt &,
+    locationt,
+    const irep_idt &,
+    locationt,
+    ai_baset &,
+    const namespacet &) override;
+  void output(
     std::ostream &,
     const ai_baset &,
-    const namespacet &) const;
+    const namespacet &) const override;
   bool merge(const ssa_value_domaint &, locationt, locationt);
 
   void make_bottom() override
@@ -147,13 +153,14 @@ class ssa_value_ait:public ait<ssa_value_domaint>
 {
 public:
   ssa_value_ait(
+    const irep_idt &function_identifier,
     const goto_functionst::goto_functiont &goto_function,
     const namespacet &ns_,
     const optionst &_options):
     ns(ns_),
     options(_options)
   {
-    operator()(goto_function, ns_);
+    operator()(function_identifier, goto_function, ns_);
   }
 
 protected:
diff --git a/src/ssa/unwindable_local_ssa.h b/src/ssa/unwindable_local_ssa.h
index 62c4df5cb..cf41b4242 100644
--- a/src/ssa/unwindable_local_ssa.h
+++ b/src/ssa/unwindable_local_ssa.h
@@ -20,11 +20,17 @@ class unwindable_local_SSAt:public local_SSAt
 {
 public:
   unwindable_local_SSAt(
+    const irep_idt &function_identifier,
     const goto_functiont &_goto_function,
     const symbol_tablet &_symbol_table,
     const optionst &_options,
     const std::string &_suffix=""):
-    local_SSAt(_goto_function, _symbol_table, _options, _suffix),
+    local_SSAt(
+      function_identifier,
+      _goto_function,
+      _symbol_table,
+      _options,
+      _suffix),
     current_unwinding(-1)
   {
     compute_loop_hierarchy();