diff --git a/src/cbmc/symex_bmc.cpp b/src/cbmc/symex_bmc.cpp
index 1dd1e8dceb9..a6dfa3bcb3a 100644
--- a/src/cbmc/symex_bmc.cpp
+++ b/src/cbmc/symex_bmc.cpp
@@ -63,11 +63,52 @@ void symex_bmct::symex_step(
     last_source_location=source_location;
   }
 
-  if(record_coverage &&
-     !state.guard.is_false())
-    symex_coverage.covered(state.source.pc);
+  const goto_programt::const_targett cur_pc=state.source.pc;
 
   goto_symext::symex_step(goto_functions, state);
+
+  if(record_coverage &&
+     // is the instruction being executed
+     !state.guard.is_false() &&
+     // avoid an invalid iterator in state.source.pc
+     (!cur_pc->is_end_function() ||
+      cur_pc->function!=ID__start) &&
+     // ignore transition to next instruction when goto points elsewhere
+     (!cur_pc->is_goto() ||
+      cur_pc->get_target()==state.source.pc ||
+      !cur_pc->guard.is_true()))
+    symex_coverage.covered(cur_pc, state.source.pc);
+}
+
+/*******************************************************************\
+
+Function: symex_bmct::merge_goto
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void symex_bmct::merge_goto(
+  const statet::goto_statet &goto_state,
+  statet &state)
+{
+  const goto_programt::const_targett prev_pc=goto_state.source.pc;
+  const guardt prev_guard=goto_state.guard;
+
+  goto_symext::merge_goto(goto_state, state);
+
+  assert(prev_pc->is_goto());
+  if(record_coverage &&
+     // could the branch possibly be taken?
+     !prev_guard.is_false() &&
+     !state.guard.is_false() &&
+     // branches only, no single-successor goto
+     !prev_pc->guard.is_true())
+    symex_coverage.covered(prev_pc, state.source.pc);
 }
 
 /*******************************************************************\
diff --git a/src/cbmc/symex_bmc.h b/src/cbmc/symex_bmc.h
index 10f4b821e88..8b2df348f3b 100644
--- a/src/cbmc/symex_bmc.h
+++ b/src/cbmc/symex_bmc.h
@@ -83,6 +83,10 @@ class symex_bmct:
     const goto_functionst &goto_functions,
     statet &state);
 
+  virtual void merge_goto(
+    const statet::goto_statet &goto_state,
+    statet &state);
+
   // for loop unwinding
   virtual bool get_unwind(
     const symex_targett::sourcet &source,
diff --git a/src/cbmc/symex_coverage.cpp b/src/cbmc/symex_coverage.cpp
index 69af02e9e9e..e984aa13a73 100644
--- a/src/cbmc/symex_coverage.cpp
+++ b/src/cbmc/symex_coverage.cpp
@@ -19,6 +19,7 @@ Date: March 2016
 #include <util/prefix.h>
 
 #include <goto-programs/goto_functions.h>
+#include <goto-programs/remove_returns.h>
 
 #include "symex_coverage.h"
 
@@ -57,26 +58,37 @@ class goto_program_coverage_recordt:public coverage_recordt
 protected:
   irep_idt file_name;
 
-  struct line_coverage_recordt
+  struct coverage_conditiont
   {
-    line_coverage_recordt():
-      hits(0), is_branch(false), branch_covered(false)
+    coverage_conditiont():
+      false_taken(false), true_taken(false)
+    {
+    }
+
+    bool false_taken;
+    bool true_taken;
+  };
+
+  struct coverage_linet
+  {
+    coverage_linet():
+      hits(0)
     {
     }
 
     unsigned hits;
-    bool is_branch;
-    bool branch_covered;
+    std::map<goto_programt::const_targett, coverage_conditiont>
+      conditions;
   };
 
-  typedef std::map<unsigned, line_coverage_recordt>
-    line_coverage_mapt;
+  typedef std::map<unsigned, coverage_linet>
+    coverage_lines_mapt;
 
-  void compute_line_coverage(
+  void compute_coverage_lines(
     const goto_programt &goto_program,
     const irep_idt &file_name,
     const symex_coveraget::coveraget &coverage,
-    line_coverage_mapt &dest);
+    coverage_lines_mapt &dest);
 };
 
 /*******************************************************************\
@@ -91,17 +103,26 @@ Function: rate
 
 \*******************************************************************/
 
-static std::string rate(std::size_t covered, std::size_t total)
+static std::string rate(
+  std::size_t covered,
+  std::size_t total,
+  bool per_cent=false)
 {
+  std::ostringstream oss;
+
 #if 1
-  if(total==0)
-    return "1.0";
+  float fraction;
 
-  std::ostringstream oss;
+  if(total==0)
+    fraction=1.0;
+  else
+    fraction=static_cast<float>(covered)/static_cast<float>(total);
 
-  oss << static_cast<float>(covered)/static_cast<float>(total);
+  if(per_cent)
+    oss << fraction*100.0 << '%';
+  else
+    oss << fraction;
 #else
-  std::ostringstream oss;
   oss << covered << " of " << total;
 #endif
 
@@ -137,12 +158,12 @@ goto_program_coverage_recordt::goto_program_coverage_recordt(
   assert(!file_name.empty());
 
   // compute the maximum coverage of individual source-code lines
-  line_coverage_mapt line_coverage_map;
-  compute_line_coverage(
+  coverage_lines_mapt coverage_lines_map;
+  compute_coverage_lines(
     gf_it->second.body,
     file_name,
     coverage,
-    line_coverage_map);
+    coverage_lines_map);
 
   // <method name="foo" signature="int(int)" line-rate="1.0" branch-rate="1.0">
   //   <lines>
@@ -157,8 +178,14 @@ goto_program_coverage_recordt::goto_program_coverage_recordt(
   //   </lines>
   // </method>
   xml.set_attribute("name", id2string(gf_it->first));
+
+  code_typet sig_type=
+    original_return_type(ns.get_symbol_table(), gf_it->first);
+  if(sig_type.is_nil())
+    sig_type=gf_it->second.type;
   xml.set_attribute("signature",
-                    from_type(ns, gf_it->first, gf_it->second.type));
+                    from_type(ns, gf_it->first, sig_type));
+
   xml.set_attribute("line-rate",
                     rate(lines_covered, lines_total));
   xml.set_attribute("branch-rate",
@@ -166,28 +193,43 @@ goto_program_coverage_recordt::goto_program_coverage_recordt(
 
   xmlt &lines=xml.new_element("lines");
 
-  for(line_coverage_mapt::const_iterator
-      it=line_coverage_map.begin();
-      it!=line_coverage_map.end();
-      ++it)
+  for(const auto &cov_line : coverage_lines_map)
   {
     xmlt &line=lines.new_element("line");
 
-    line.set_attribute("number", std::to_string(it->first));
-    line.set_attribute("hits", std::to_string(it->second.hits));
-    if(!it->second.is_branch)
+    line.set_attribute("number", std::to_string(cov_line.first));
+    line.set_attribute("hits", std::to_string(cov_line.second.hits));
+    if(cov_line.second.conditions.empty())
       line.set_attribute("branch", "false");
     else
     {
-      // TODO: conditions
       line.set_attribute("branch", "true");
+
+      xmlt &conditions=line.new_element("conditions");
+
+      std::size_t number=0, total_taken=0;
+      for(const auto &c : cov_line.second.conditions)
+      {
+        // <condition number="0" type="jump" coverage="50%"/>
+        xmlt &condition=conditions.new_element("condition");
+        condition.set_attribute("number", std::to_string(number++));
+        condition.set_attribute("type", "jump");
+        unsigned taken=c.second.false_taken+c.second.true_taken;
+        total_taken+=taken;
+        condition.set_attribute("coverage", rate(taken, 2, true));
+      }
+
+      std::ostringstream oss;
+      oss << rate(total_taken, number*2, true)
+          << " (" << total_taken << '/' << number*2 << ')';
+      line.set_attribute("condition-coverage", oss.str());
     }
   }
 }
 
 /*******************************************************************\
 
-Function: goto_program_coverage_recordt::compute_line_coverage
+Function: goto_program_coverage_recordt::compute_coverage_lines
 
   Inputs:
 
@@ -197,58 +239,83 @@ Function: goto_program_coverage_recordt::compute_line_coverage
 
 \*******************************************************************/
 
-void goto_program_coverage_recordt::compute_line_coverage(
+void goto_program_coverage_recordt::compute_coverage_lines(
     const goto_programt &goto_program,
     const irep_idt &file_name,
     const symex_coveraget::coveraget &coverage,
-    line_coverage_mapt &dest)
+    coverage_lines_mapt &dest)
 {
   forall_goto_program_instructions(it, goto_program)
   {
     if(it->source_location.is_nil() ||
-       it->source_location.get_file()!=file_name)
+       it->source_location.get_file()!=file_name ||
+       it->is_dead() ||
+       it->is_end_function())
       continue;
 
     const bool is_branch=it->is_goto() && !it->guard.is_constant();
 
     unsigned l=
       safe_string2unsigned(id2string(it->source_location.get_line()));
-    std::pair<line_coverage_mapt::iterator, bool> entry=
-      dest.insert(std::make_pair(l, line_coverage_recordt()));
+    std::pair<coverage_lines_mapt::iterator, bool> entry=
+      dest.insert(std::make_pair(l, coverage_linet()));
 
     if(entry.second)
-    {
       ++lines_total;
-      if(is_branch)
-        ++branches_total;
-    }
 
     // mark as branch if any instruction in this source code line is
     // a branching instruction
-    if(is_branch &&
-       !entry.first->second.is_branch)
+    if(is_branch)
     {
-      ++branches_total;
-      entry.first->second.is_branch=true;
+      branches_total+=2;
+      if(!entry.first->second.conditions.insert(
+          {it, coverage_conditiont()}).second)
+        assert(false);
     }
 
     symex_coveraget::coveraget::const_iterator c_entry=
       coverage.find(it);
-    if(c_entry!=coverage.end() &&
-       c_entry->second.num_executions>0)
+    if(c_entry!=coverage.end())
     {
-      // maximum over all instructions in this source code line
-      if(c_entry->second.num_executions>entry.first->second.hits)
+      if(!(c_entry->second.size()==1 || is_branch))
       {
-        if(entry.first->second.hits==0)
-          ++lines_covered;
-        entry.first->second.hits=c_entry->second.num_executions;
+        std::cerr << it->location_number << std::endl;
+        for(const auto &cov : c_entry->second)
+          std::cerr << cov.second.succ->location_number << std::endl;
       }
+      assert(c_entry->second.size()==1 || is_branch);
 
-      if(is_branch && !entry.first->second.branch_covered)
+      for(const auto &cov : c_entry->second)
       {
-        ++branches_covered;
-        entry.first->second.branch_covered=true;
+        assert(cov.second.num_executions>0);
+
+        if(entry.first->second.hits==0)
+          ++lines_covered;
+
+        entry.first->second.hits+=cov.second.num_executions;
+
+        if(is_branch)
+        {
+          auto cond_entry=entry.first->second.conditions.find(it);
+          assert(cond_entry!=entry.first->second.conditions.end());
+
+          if(it->get_target()==cov.second.succ)
+          {
+            if(!cond_entry->second.false_taken)
+            {
+              cond_entry->second.false_taken=true;
+              ++branches_covered;
+            }
+          }
+          else
+          {
+            if(!cond_entry->second.true_taken)
+            {
+              cond_entry->second.true_taken=true;
+              ++branches_covered;
+            }
+          }
+        }
       }
     }
   }
diff --git a/src/cbmc/symex_coverage.h b/src/cbmc/symex_coverage.h
index 0e71b430630..c173bc65ad7 100644
--- a/src/cbmc/symex_coverage.h
+++ b/src/cbmc/symex_coverage.h
@@ -29,11 +29,12 @@ class symex_coveraget
   {
   }
 
-  void covered(goto_programt::const_targett location)
+  void covered(
+    goto_programt::const_targett from,
+    goto_programt::const_targett to)
   {
-    std::pair<coveraget::iterator, bool> entry=
-      coverage.insert(std::make_pair(location,
-                                     coverage_infot(location, 1)));
+    std::pair<coverage_innert::iterator, bool> entry=
+      coverage[from].insert({to, coverage_infot(from, to, 1)});
 
     if(!entry.second)
       ++(entry.first->second.num_executions);
@@ -49,17 +50,22 @@ class symex_coveraget
   struct coverage_infot
   {
     coverage_infot(
-      goto_programt::const_targett _location,
+      goto_programt::const_targett _from,
+      goto_programt::const_targett _to,
       unsigned _num_executions):
-      location(_location), num_executions(_num_executions)
+      location(_from), num_executions(_num_executions),
+      succ(_to)
     {
     }
 
     goto_programt::const_targett location;
     unsigned num_executions;
+    goto_programt::const_targett succ;
   };
 
   typedef std::map<goto_programt::const_targett, coverage_infot>
+    coverage_innert;
+  typedef std::map<goto_programt::const_targett, coverage_innert>
     coveraget;
   coveraget coverage;
 
diff --git a/src/goto-programs/remove_returns.cpp b/src/goto-programs/remove_returns.cpp
index b3afbf967fc..9ca6554275c 100644
--- a/src/goto-programs/remove_returns.cpp
+++ b/src/goto-programs/remove_returns.cpp
@@ -269,6 +269,46 @@ void remove_returns(goto_modelt &goto_model)
 
 /*******************************************************************\
 
+Function: original_return_type
+
+Inputs:
+
+Outputs:
+
+Purpose:
+
+\*******************************************************************/
+
+code_typet original_return_type(
+  const symbol_tablet &symbol_table,
+  const irep_idt &function_id)
+{
+  code_typet type;
+  type.make_nil();
+
+  // do we have X#return_value?
+  std::string rv_name=id2string(function_id)+RETURN_VALUE_SUFFIX;
+
+  symbol_tablet::symbolst::const_iterator rv_it=
+    symbol_table.symbols.find(rv_name);
+
+  if(rv_it!=symbol_table.symbols.end())
+  {
+    // look up the function symbol
+    symbol_tablet::symbolst::const_iterator s_it=
+      symbol_table.symbols.find(function_id);
+
+    assert(s_it!=symbol_table.symbols.end());
+
+    type=to_code_type(s_it->second.type);
+    type.return_type()=rv_it->second.type;
+  }
+
+  return type;
+}
+
+/*******************************************************************\
+
 Function: remove_returnst::restore_returns
 
 Inputs:
@@ -301,7 +341,7 @@ bool remove_returnst::restore_returns(
   symbolt &function_symbol=s_it->second;
 
   // restore the return type
-  f_it->second.type.return_type()=rv_it->second.type;
+  f_it->second.type=original_return_type(symbol_table, function_id);
   function_symbol.type=f_it->second.type;
 
   // remove the return_value symbol from the symbol_table
diff --git a/src/goto-programs/remove_returns.h b/src/goto-programs/remove_returns.h
index 3f68d3e89e2..453d8a7be7f 100644
--- a/src/goto-programs/remove_returns.h
+++ b/src/goto-programs/remove_returns.h
@@ -26,4 +26,8 @@ void remove_returns(goto_modelt &);
 // reverse the above operations
 void restore_returns(symbol_tablet &, goto_functionst &);
 
+code_typet original_return_type(
+  const symbol_tablet &symbol_table,
+  const irep_idt &function_id);
+
 #endif // CPROVER_GOTO_PROGRAMS_REMOVE_RETURNS_H
diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
index de71fcc9d09..f8c2cda0bf9 100644
--- a/src/goto-symex/goto_symex.h
+++ b/src/goto-symex/goto_symex.h
@@ -175,6 +175,10 @@ class goto_symext
   // gotos
   void merge_gotos(statet &state);
 
+  virtual void merge_goto(
+    const statet::goto_statet &goto_state,
+    statet &state);
+
   void merge_value_sets(
     const statet::goto_statet &goto_state,
     statet &dest);
diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h
index 5439af37e05..292dec478c7 100644
--- a/src/goto-symex/goto_symex_state.h
+++ b/src/goto-symex/goto_symex_state.h
@@ -189,6 +189,7 @@ class goto_symex_statet
     level2t::current_namest level2_current_names;
     value_sett value_set;
     guardt guard;
+    symex_targett::sourcet source;
     propagationt propagation;
     unsigned atomic_section_id;
 
@@ -197,6 +198,7 @@ class goto_symex_statet
       level2_current_names(s.level2.current_names),
       value_set(s.value_set),
       guard(s.guard),
+      source(s.source),
       propagation(s.propagation),
       atomic_section_id(s.atomic_section_id)
     {
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
index b8e6f1a0a36..7590a111e15 100644
--- a/src/goto-symex/symex_goto.cpp
+++ b/src/goto-symex/symex_goto.cpp
@@ -121,8 +121,6 @@ void goto_symext::symex_goto(statet &state)
     state_pc=goto_target;
   }
 
-  state.source.pc=state_pc;
-
   // put into state-queue
   statet::goto_state_listt &goto_state_list=
     state.top().goto_state_map[new_state_pc];
@@ -130,6 +128,8 @@ void goto_symext::symex_goto(statet &state)
   goto_state_list.push_back(statet::goto_statet(state));
   statet::goto_statet &new_state=goto_state_list.back();
 
+  state.source.pc=state_pc;
+
   // adjust guards
   if(new_guard.is_true())
   {
@@ -244,27 +244,42 @@ void goto_symext::merge_gotos(statet &state)
       list_it=state_list.rbegin();
       list_it!=state_list.rend();
       list_it++)
-  {
-    statet::goto_statet &goto_state=*list_it;
+    merge_goto(*list_it, state);
 
-    // check atomic section
-    if(state.atomic_section_id!=goto_state.atomic_section_id)
-      throw "atomic sections differ across branches";
+  // clean up to save some memory
+  frame.goto_state_map.erase(state_map_it);
+}
 
-    // do SSA phi functions
-    phi_function(goto_state, state);
+/*******************************************************************\
 
-    merge_value_sets(goto_state, state);
+Function: goto_symext::merge_goto
 
-    // adjust guard
-    state.guard|=goto_state.guard;
+  Inputs:
 
-    // adjust depth
-    state.depth=std::min(state.depth, goto_state.depth);
-  }
+ Outputs:
 
-  // clean up to save some memory
-  frame.goto_state_map.erase(state_map_it);
+ Purpose:
+
+\*******************************************************************/
+
+void goto_symext::merge_goto(
+  const statet::goto_statet &goto_state,
+  statet &state)
+{
+  // check atomic section
+  if(state.atomic_section_id!=goto_state.atomic_section_id)
+    throw "atomic sections differ across branches";
+
+  // do SSA phi functions
+  phi_function(goto_state, state);
+
+  merge_value_sets(goto_state, state);
+
+  // adjust guard
+  state.guard|=goto_state.guard;
+
+  // adjust depth
+  state.depth=std::min(state.depth, goto_state.depth);
 }
 
 /*******************************************************************\