diff --git a/src/goto-diff/change_impact.cpp b/src/goto-diff/change_impact.cpp
index 67bcc2535b0..32ce14e28fc 100644
--- a/src/goto-diff/change_impact.cpp
+++ b/src/goto-diff/change_impact.cpp
@@ -315,8 +315,7 @@ change_impactt::change_impactt(
 
 void change_impactt::change_impact(const irep_idt &function)
 {
-  unified_difft::goto_program_difft diff;
-  unified_diff.get_diff(function, diff);
+  unified_difft::goto_program_difft diff = unified_diff.get_diff(function);
 
   if(diff.empty())
     return;
diff --git a/src/goto-diff/unified_diff.cpp b/src/goto-diff/unified_diff.cpp
index 75924bfca5d..aefcdc4c91c 100644
--- a/src/goto-diff/unified_diff.cpp
+++ b/src/goto-diff/unified_diff.cpp
@@ -17,85 +17,87 @@ Date: April 2016
 
 #include <goto-programs/goto_model.h>
 
-unified_difft::unified_difft(const goto_modelt &model_old,
-                             const goto_modelt &model_new):
-  old_goto_functions(model_old.goto_functions),
-  ns_old(model_old.symbol_table),
-  new_goto_functions(model_new.goto_functions),
-  ns_new(model_new.symbol_table)
+unified_difft::unified_difft(
+  const goto_modelt &model_old,
+  const goto_modelt &model_new)
+  : old_goto_functions(model_old.goto_functions),
+    ns_old(model_old.symbol_table),
+    new_goto_functions(model_new.goto_functions),
+    ns_new(model_new.symbol_table)
 {
 }
 
-void unified_difft::get_diff(
-  const irep_idt &function,
-  goto_program_difft &dest) const
+unified_difft::goto_program_difft
+unified_difft::get_diff(const irep_idt &function) const
 {
-  dest.clear();
+  differences_mapt::const_iterator entry = differences_map_.find(function);
+  if(entry == differences_map_.end())
+    return {};
 
-  differences_mapt::const_iterator entry=
-    differences_map.find(function);
-  if(entry==differences_map.end())
-    return;
-
-  goto_functionst::function_mapt::const_iterator old_fit=
+  goto_functionst::function_mapt::const_iterator old_fit =
     old_goto_functions.function_map.find(function);
-  goto_functionst::function_mapt::const_iterator new_fit=
+  goto_functionst::function_mapt::const_iterator new_fit =
     new_goto_functions.function_map.find(function);
 
   goto_programt empty;
 
-  const goto_programt &old_goto_program=
-    old_fit==old_goto_functions.function_map.end() ?
-    empty :
-    old_fit->second.body;
-  const goto_programt &new_goto_program=
-    new_fit==new_goto_functions.function_map.end() ?
-    empty :
-    new_fit->second.body;
-
-  get_diff(
-    old_goto_program,
-    new_goto_program,
-    entry->second,
-    dest);
+  const goto_programt &old_goto_program =
+    old_fit == old_goto_functions.function_map.end() ? empty
+                                                     : old_fit->second.body;
+  const goto_programt &new_goto_program =
+    new_fit == new_goto_functions.function_map.end() ? empty
+                                                     : new_fit->second.body;
+
+  return get_diff(old_goto_program, new_goto_program, entry->second);
 }
 
-void unified_difft::get_diff(
+unified_difft::goto_program_difft unified_difft::get_diff(
   const goto_programt &old_goto_program,
   const goto_programt &new_goto_program,
-  const differencest &differences,
-  goto_program_difft &dest) const
+  const differencest &differences) const
 {
-  goto_programt::instructionst::const_iterator old_it=
+  goto_programt::instructionst::const_iterator old_it =
     old_goto_program.instructions.begin();
-  goto_programt::instructionst::const_iterator new_it=
+  goto_programt::instructionst::const_iterator new_it =
     new_goto_program.instructions.begin();
 
-  for(differencest::const_reverse_iterator rit=differences.rbegin();
-      rit!=differences.rend();
+  goto_program_difft dest;
+
+  for(differencest::const_reverse_iterator rit = differences.rbegin();
+      rit != differences.rend();
       ++rit)
   {
     switch(*rit)
     {
-      case differencet::SAME:
-        dest.push_back(std::make_pair(new_it, differencet::SAME));
-        assert(old_it!=old_goto_program.instructions.end());
-        ++old_it;
-        assert(new_it!=new_goto_program.instructions.end());
-        ++new_it;
-        break;
-      case differencet::DELETED:
-        dest.push_back(std::make_pair(old_it, differencet::DELETED));
-        assert(old_it!=old_goto_program.instructions.end());
-        ++old_it;
-        break;
-      case differencet::NEW:
-        dest.push_back(std::make_pair(new_it, differencet::NEW));
-        assert(new_it!=new_goto_program.instructions.end());
-        ++new_it;
-        break;
+    case differencet::SAME:
+      dest.push_back(std::make_pair(new_it, differencet::SAME));
+      INVARIANT(
+        old_it != old_goto_program.instructions.end(),
+        "old iterator reached the final goto instruction");
+      ++old_it;
+      INVARIANT(
+        new_it != new_goto_program.instructions.end(),
+        "new iterator reached the final goto instruction");
+      ++new_it;
+      break;
+    case differencet::DELETED:
+      dest.push_back(std::make_pair(old_it, differencet::DELETED));
+      INVARIANT(
+        old_it != old_goto_program.instructions.end(),
+        "old iterator reached the final goto instruction");
+      ++old_it;
+      break;
+    case differencet::NEW:
+      dest.push_back(std::make_pair(new_it, differencet::NEW));
+      INVARIANT(
+        new_it != new_goto_program.instructions.end(),
+        "new iterator reached the final goto instruction");
+      ++new_it;
+      break;
     }
   }
+
+  return dest;
 }
 
 void unified_difft::output_diff(
@@ -105,19 +107,15 @@ void unified_difft::output_diff(
   const differencest &differences,
   std::ostream &os) const
 {
-  goto_program_difft diff;
-  get_diff(
-    old_goto_program,
-    new_goto_program,
-    differences,
-    diff);
-
-  bool has_diff=false;
+  goto_program_difft diff =
+    get_diff(old_goto_program, new_goto_program, differences);
+
+  bool has_diff = false;
   for(const auto &d : diff)
   {
-    if(d.second!=differencet::SAME)
+    if(d.second != differencet::SAME)
     {
-      has_diff=true;
+      has_diff = true;
       break;
     }
   }
@@ -130,18 +128,18 @@ void unified_difft::output_diff(
   {
     switch(d.second)
     {
-      case differencet::SAME:
-        os << ' ';
-        new_goto_program.output_instruction(ns_new, identifier, os, *d.first);
-        break;
-      case differencet::DELETED:
-        os << '-';
-        old_goto_program.output_instruction(ns_old, identifier, os, *d.first);
-        break;
-      case differencet::NEW:
-        os << '+';
-        new_goto_program.output_instruction(ns_new, identifier, os, *d.first);
-        break;
+    case differencet::SAME:
+      os << ' ';
+      new_goto_program.output_instruction(ns_new, identifier, os, *d.first);
+      break;
+    case differencet::DELETED:
+      os << '-';
+      old_goto_program.output_instruction(ns_old, identifier, os, *d.first);
+      break;
+    case differencet::NEW:
+      os << '+';
+      new_goto_program.output_instruction(ns_new, identifier, os, *d.first);
+      break;
     }
   }
 }
@@ -152,21 +150,20 @@ void unified_difft::lcss(
   const goto_programt &new_goto_program,
   differencest &differences) const
 {
-  std::size_t old_count=old_goto_program.instructions.size();
-  std::size_t new_count=new_goto_program.instructions.size();
+  std::size_t old_count = old_goto_program.instructions.size();
+  std::size_t new_count = new_goto_program.instructions.size();
 
-  differences.reserve(old_count+new_count);
+  differences.reserve(old_count + new_count);
 
   // skip common prefix
-  goto_programt::instructionst::const_iterator old_it=
+  goto_programt::instructionst::const_iterator old_it =
     old_goto_program.instructions.begin();
-  goto_programt::instructionst::const_iterator new_it=
+  goto_programt::instructionst::const_iterator new_it =
     new_goto_program.instructions.begin();
 
-  for( ;
-       old_it!=old_goto_program.instructions.end() &&
-       new_it!=new_goto_program.instructions.end();
-       ++old_it, ++new_it)
+  for(; old_it != old_goto_program.instructions.end() &&
+        new_it != new_goto_program.instructions.end();
+      ++old_it, ++new_it)
   {
     if(!instructions_equal(*old_it, *new_it))
       break;
@@ -178,12 +175,12 @@ void unified_difft::lcss(
   // differ
 
   // skip common suffix
-  goto_programt::instructionst::const_iterator old_rit=
+  goto_programt::instructionst::const_iterator old_rit =
     old_goto_program.instructions.end();
-  goto_programt::instructionst::const_iterator new_rit=
+  goto_programt::instructionst::const_iterator new_rit =
     new_goto_program.instructions.end();
 
-  while(old_rit!=old_it && new_rit!=new_it)
+  while(old_rit != old_it && new_rit != new_it)
   {
     --old_rit;
     --new_rit;
@@ -202,38 +199,37 @@ void unified_difft::lcss(
   // old_rit, new_rit are now iterators to the first instructions of
   // the common tail
 
-  if(old_count==0 && new_count==0)
+  if(old_count == 0 && new_count == 0)
     return;
 
   // apply longest common subsequence (LCSS)
-  typedef std::vector<std::vector<std::size_t> > lcss_matrixt;
+  typedef std::vector<std::vector<std::size_t>> lcss_matrixt;
   lcss_matrixt lcss_matrix(
-    old_count+1,
-    std::vector<size_t>(new_count+1, 0));
+    old_count + 1, std::vector<size_t>(new_count + 1, 0));
 
   // fill the matrix
-  std::size_t i=1, j=1;
-  for(goto_programt::instructionst::const_iterator old_it2=old_it;
-      old_it2!=old_rit;
+  std::size_t i = 1, j = 1;
+  for(goto_programt::instructionst::const_iterator old_it2 = old_it;
+      old_it2 != old_rit;
       ++old_it2)
   {
-    j=1;
-    for(goto_programt::instructionst::const_iterator new_it2=new_it;
-        new_it2!=new_rit;
+    j = 1;
+    for(goto_programt::instructionst::const_iterator new_it2 = new_it;
+        new_it2 != new_rit;
         ++new_it2)
     {
       if(instructions_equal(*old_it2, *new_it2))
-        lcss_matrix[i][j]+=lcss_matrix[i-1][j-1]+1;
+        lcss_matrix[i][j] += lcss_matrix[i - 1][j - 1] + 1;
       else
-        lcss_matrix[i][j]=
-          std::max(lcss_matrix[i][j-1], lcss_matrix[i-1][j]);
+        lcss_matrix[i][j] =
+          std::max(lcss_matrix[i][j - 1], lcss_matrix[i - 1][j]);
 
       ++j;
     }
     ++i;
   }
 
-  #if 0
+#if 0
   std::cerr << "old_count=" << old_count << '\n';
   std::cerr << "new_count=" << new_count << '\n';
   for(i=0; i<=old_count; ++i)
@@ -247,26 +243,26 @@ void unified_difft::lcss(
     }
     std::cerr << '\n';
   }
-  #endif
+#endif
 
   // backtracking
   // note that the order in case of multiple possible matches of
   // the if-clauses is important to provide a convenient ordering
   // of - and + lines (- goes before +)
-  i=old_count;
-  j=new_count;
+  i = old_count;
+  j = new_count;
   --old_rit;
   --new_rit;
 
-  while(i>0 || j>0)
+  while(i > 0 || j > 0)
   {
-    if(i==0)
+    if(i == 0)
     {
       differences.push_back(differencet::NEW);
       --j;
       --new_rit;
     }
-    else if(j==0)
+    else if(j == 0)
     {
       differences.push_back(differencet::DELETED);
       --i;
@@ -280,7 +276,7 @@ void unified_difft::lcss(
       --j;
       --new_rit;
     }
-    else if(lcss_matrix[i][j-1]<lcss_matrix[i][j])
+    else if(lcss_matrix[i][j - 1] < lcss_matrix[i][j])
     {
       differences.push_back(differencet::DELETED);
       --i;
@@ -295,7 +291,7 @@ void unified_difft::lcss(
   }
 
   // add common prefix (if any)
-  for( ; old_it!=old_goto_program.instructions.begin(); --old_it)
+  for(; old_it != old_goto_program.instructions.begin(); --old_it)
     differences.push_back(differencet::SAME);
 }
 
@@ -304,20 +300,19 @@ void unified_difft::unified_diff(
   const goto_programt &old_goto_program,
   const goto_programt &new_goto_program)
 {
-  differencest &differences=differences_map[identifier];
+  differencest &differences = differences_map_[identifier];
   differences.clear();
 
-  if(old_goto_program.instructions.empty() ||
-     new_goto_program.instructions.empty())
+  if(
+    old_goto_program.instructions.empty() ||
+    new_goto_program.instructions.empty())
   {
     if(new_goto_program.instructions.empty())
       differences.resize(
-        old_goto_program.instructions.size(),
-        differencet::DELETED);
+        old_goto_program.instructions.size(), differencet::DELETED);
     else
       differences.resize(
-        new_goto_program.instructions.size(),
-        differencet::NEW);
+        new_goto_program.instructions.size(), differencet::NEW);
   }
   else
     lcss(identifier, old_goto_program, new_goto_program, differences);
@@ -325,9 +320,8 @@ void unified_difft::unified_diff(
 
 bool unified_difft::operator()()
 {
-  typedef std::map<irep_idt,
-                   goto_functionst::function_mapt::const_iterator>
-                     function_mapt;
+  typedef std::map<irep_idt, goto_functionst::function_mapt::const_iterator>
+    function_mapt;
 
   function_mapt old_funcs, new_funcs;
 
@@ -338,61 +332,67 @@ bool unified_difft::operator()()
 
   goto_programt empty;
 
-  function_mapt::const_iterator ito=old_funcs.begin();
-  for(function_mapt::const_iterator itn=new_funcs.begin();
-      itn!=new_funcs.end();
+  function_mapt::const_iterator ito = old_funcs.begin();
+  for(function_mapt::const_iterator itn = new_funcs.begin();
+      itn != new_funcs.end();
       ++itn)
   {
-    for( ;
-        ito!=old_funcs.end() && ito->first<itn->first;
-        ++ito)
+    for(; ito != old_funcs.end() && ito->first < itn->first; ++ito)
       unified_diff(ito->first, ito->second->second.body, empty);
 
-    if(ito==old_funcs.end() || itn->first<ito->first)
+    if(ito == old_funcs.end() || itn->first < ito->first)
       unified_diff(itn->first, empty, itn->second->second.body);
     else
     {
-      assert(ito->first==itn->first);
+      INVARIANT(
+        ito->first == itn->first, "old and new function names do not match");
       unified_diff(
-        itn->first,
-        ito->second->second.body,
-        itn->second->second.body);
+        itn->first, ito->second->second.body, itn->second->second.body);
       ++ito;
     }
   }
-  for( ; ito!=old_funcs.end(); ++ito)
+  for(; ito != old_funcs.end(); ++ito)
     unified_diff(ito->first, ito->second->second.body, empty);
 
-  return !differences_map.empty();
+  return !differences_map_.empty();
 }
 
 void unified_difft::output(std::ostream &os) const
 {
   goto_programt empty;
 
-  for(const std::pair<irep_idt, differencest> &p : differences_map)
+  for(const std::pair<irep_idt, differencest> &p : differences_map_)
   {
-    const irep_idt &function=p.first;
+    const irep_idt &function = p.first;
 
-    goto_functionst::function_mapt::const_iterator old_fit=
+    goto_functionst::function_mapt::const_iterator old_fit =
       old_goto_functions.function_map.find(function);
-    goto_functionst::function_mapt::const_iterator new_fit=
+    goto_functionst::function_mapt::const_iterator new_fit =
       new_goto_functions.function_map.find(function);
 
-    const goto_programt &old_goto_program=
-      old_fit==old_goto_functions.function_map.end() ?
-      empty :
-      old_fit->second.body;
-    const goto_programt &new_goto_program=
-      new_fit==new_goto_functions.function_map.end() ?
-      empty :
-      new_fit->second.body;
-
-    output_diff(
-      function,
-      old_goto_program,
-      new_goto_program,
-      p.second,
-      os);
+    const goto_programt &old_goto_program =
+      old_fit == old_goto_functions.function_map.end() ? empty
+                                                       : old_fit->second.body;
+    const goto_programt &new_goto_program =
+      new_fit == new_goto_functions.function_map.end() ? empty
+                                                       : new_fit->second.body;
+
+    output_diff(function, old_goto_program, new_goto_program, p.second, os);
   }
 }
+
+bool unified_difft::instructions_equal(
+  const goto_programt::instructiont &ins1,
+  const goto_programt::instructiont &ins2)
+{
+  return ins1.code == ins2.code && ins1.function == ins2.function &&
+         ins1.type == ins2.type && ins1.guard == ins2.guard &&
+         ins1.targets.size() == ins2.targets.size() &&
+         (ins1.targets.empty() ||
+          instructions_equal(*ins1.get_target(), *ins2.get_target()));
+}
+
+const unified_difft::differences_mapt &unified_difft::differences_map() const
+{
+  return differences_map_;
+}
diff --git a/src/goto-diff/unified_diff.h b/src/goto-diff/unified_diff.h
index 2ba9f09ae1c..e8a6e227e46 100644
--- a/src/goto-diff/unified_diff.h
+++ b/src/goto-diff/unified_diff.h
@@ -30,9 +30,7 @@ class goto_programt;
 class unified_difft
 {
 public:
-  unified_difft(
-    const goto_modelt &model_old,
-    const goto_modelt &model_new);
+  unified_difft(const goto_modelt &model_old, const goto_modelt &model_new);
 
   bool operator()();
 
@@ -45,15 +43,11 @@ class unified_difft
     NEW
   };
 
-  typedef std::list<std::pair<goto_programt::const_targett,
-                              differencet> >
+  typedef std::list<std::pair<goto_programt::const_targett, differencet>>
     goto_program_difft;
 
-  void get_diff(
-    const irep_idt &function,
-    goto_program_difft &dest) const;
+  goto_program_difft get_diff(const irep_idt &function) const;
 
-protected:
   const goto_functionst &old_goto_functions;
   const namespacet ns_old;
   const goto_functionst &new_goto_functions;
@@ -62,8 +56,6 @@ class unified_difft
   typedef std::vector<differencet> differencest;
   typedef std::map<irep_idt, differencest> differences_mapt;
 
-  differences_mapt differences_map;
-
   void unified_diff(
     const irep_idt &identifier,
     const goto_programt &old_goto_program,
@@ -75,11 +67,10 @@ class unified_difft
     const goto_programt &new_goto_program,
     differencest &differences) const;
 
-  void get_diff(
+  goto_program_difft get_diff(
     const goto_programt &old_goto_program,
     const goto_programt &new_goto_program,
-    const differencest &differences,
-    goto_program_difft &dest) const;
+    const differencest &differences) const;
 
   void output_diff(
     const irep_idt &identifier,
@@ -88,23 +79,14 @@ class unified_difft
     const differencest &differences,
     std::ostream &os) const;
 
-  bool instructions_equal(
+  static bool instructions_equal(
     const goto_programt::instructiont &ins1,
-    const goto_programt::instructiont &ins2,
-    bool recurse=true) const
-  {
-    return
-      ins1.code==ins2.code &&
-      ins1.function==ins2.function &&
-      ins1.type==ins2.type &&
-      ins1.guard==ins2.guard &&
-      ins1.targets.size()==ins2.targets.size() &&
-      (ins1.targets.empty() ||
-       instructions_equal(
-         *ins1.get_target(),
-         *ins2.get_target(),
-         false));
-  }
+    const goto_programt::instructiont &ins2);
+
+  const differences_mapt &differences_map() const;
+
+private:
+  differences_mapt differences_map_;
 };
 
 #endif // CPROVER_GOTO_DIFF_UNIFIED_DIFF_H