diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
index e2f8584b9e4..7330a2dcbbc 100644
--- a/src/cbmc/bmc.cpp
+++ b/src/cbmc/bmc.cpp
@@ -153,9 +153,14 @@ bmct::run_decision_procedure(prop_convt &prop_conv)
 
 void bmct::report_success()
 {
-  result() << bold << "VERIFICATION SUCCESSFUL" << reset << eom;
+  report_success(*this, ui_message_handler);
+}
 
-  switch(ui_message_handler.get_ui())
+void bmct::report_success(messaget &log, ui_message_handlert &handler)
+{
+  log.result() << log.bold << "VERIFICATION SUCCESSFUL" << log.reset << log.eom;
+
+  switch(handler.get_ui())
   {
   case ui_message_handlert::uit::PLAIN:
     break;
@@ -164,7 +169,7 @@ void bmct::report_success()
     {
       xmlt xml("cprover-status");
       xml.data="SUCCESS";
-      result() << xml;
+      log.result() << xml;
     }
     break;
 
@@ -172,7 +177,7 @@ void bmct::report_success()
     {
       json_objectt json_result;
       json_result["cProverStatus"]=json_stringt("success");
-      result() << json_result;
+      log.result() << json_result;
     }
     break;
   }
@@ -180,9 +185,14 @@ void bmct::report_success()
 
 void bmct::report_failure()
 {
-  result() << bold << "VERIFICATION FAILED" << reset << eom;
+  report_failure(*this, ui_message_handler);
+}
 
-  switch(ui_message_handler.get_ui())
+void bmct::report_failure(messaget &log, ui_message_handlert &handler)
+{
+  log.result() << log.bold << "VERIFICATION FAILED" << log.reset << log.eom;
+
+  switch(handler.get_ui())
   {
   case ui_message_handlert::uit::PLAIN:
     break;
@@ -191,7 +201,7 @@ void bmct::report_failure()
     {
       xmlt xml("cprover-status");
       xml.data="FAILURE";
-      result() << xml;
+      log.result() << xml;
     }
     break;
 
@@ -199,7 +209,7 @@ void bmct::report_failure()
     {
       json_objectt json_result;
       json_result["cProverStatus"]=json_stringt("failure");
-      result() << json_result;
+      log.result() << json_result;
     }
     break;
   }
@@ -260,9 +270,6 @@ safety_checkert::resultt bmct::execute(
     const goto_functionst &goto_functions =
       goto_model.get_goto_functions();
 
-    if(symex.should_pause_symex)
-      return safety_checkert::resultt::PAUSED;
-
     // This provides the driver program the opportunity to do things like a
     // symbol-table or goto-functions dump instead of actually running the
     // checker, like show-vcc except driver-program specific.
@@ -272,9 +279,14 @@ safety_checkert::resultt bmct::execute(
     if(driver_callback_after_symex && driver_callback_after_symex())
       return safety_checkert::resultt::SAFE; // to indicate non-error
 
-    // add a partial ordering, if required
     if(equation.has_threads())
     {
+      // When doing path exploration in a concurrent setting, we should avoid
+      // model-checking the program until we reach the end of a path.
+      if(symex.should_pause_symex)
+        return safety_checkert::resultt::PAUSED;
+
+      // add a partial ordering, if required
       memory_model->set_message_handler(get_message_handler());
       (*memory_model)(equation);
     }
@@ -318,6 +330,8 @@ safety_checkert::resultt bmct::execute(
       !options.get_bool_option("program-only") &&
       symex.get_remaining_vccs() == 0)
     {
+      if(options.is_set("paths"))
+        return safety_checkert::resultt::PAUSED;
       report_success();
       output_graphml(resultt::SAFE);
       return safety_checkert::resultt::SAFE;
@@ -329,7 +343,10 @@ safety_checkert::resultt bmct::execute(
       return safety_checkert::resultt::SAFE;
     }
 
-    return decide(goto_functions, prop_conv);
+    if(!options.is_set("paths") || symex.path_segment_vccs > 0)
+      return decide(goto_functions, prop_conv);
+
+    return safety_checkert::resultt::PAUSED;
   }
 
   catch(const std::string &error_str)
@@ -396,6 +413,10 @@ void bmct::slice()
   statistics() << "Generated " << symex.get_total_vccs() << " VCC(s), "
                << symex.get_remaining_vccs()
                << " remaining after simplification" << eom;
+
+  if(options.is_set("paths"))
+    statistics() << "Generated " << symex.path_segment_vccs
+                 << " new VCC(s) along current path segment" << eom;
 }
 
 safety_checkert::resultt bmct::run(
@@ -484,8 +505,8 @@ int bmct::do_language_agnostic_bmc(
   std::function<void(bmct &, const symbol_tablet &)> driver_configure_bmc,
   std::function<bool(void)> callback_after_symex)
 {
-  safety_checkert::resultt final_result = safety_checkert::resultt::UNKNOWN;
-  safety_checkert::resultt tmp_result = safety_checkert::resultt::UNKNOWN;
+  safety_checkert::resultt final_result = safety_checkert::resultt::SAFE;
+  safety_checkert::resultt tmp_result = safety_checkert::resultt::SAFE;
   const symbol_tablet &symbol_table = model.get_symbol_table();
   messaget message(ui);
   std::unique_ptr<path_storaget> worklist;
@@ -544,11 +565,6 @@ int bmct::do_language_agnostic_bmc(
 
     while(!worklist->empty())
     {
-      if(tmp_result != safety_checkert::resultt::PAUSED)
-        message.status() << "___________________________\n"
-                         << "Starting new path (" << worklist->size()
-                         << " to go)\n"
-                         << message.eom;
       cbmc_solverst solvers(
         opts,
         symbol_table,
@@ -603,13 +619,15 @@ int bmct::do_language_agnostic_bmc(
   switch(final_result)
   {
   case safety_checkert::resultt::SAFE:
+    if(opts.is_set("paths"))
+      report_success(message, ui);
     return CPROVER_EXIT_VERIFICATION_SAFE;
   case safety_checkert::resultt::UNSAFE:
+    if(opts.is_set("paths"))
+      report_failure(message, ui);
     return CPROVER_EXIT_VERIFICATION_UNSAFE;
   case safety_checkert::resultt::ERROR:
     return CPROVER_EXIT_INTERNAL_ERROR;
-  case safety_checkert::resultt::UNKNOWN:
-    return CPROVER_EXIT_INTERNAL_ERROR;
   case safety_checkert::resultt::PAUSED:
     UNREACHABLE;
   }
diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h
index 261b77c96a3..6ff7f937c2a 100644
--- a/src/cbmc/bmc.h
+++ b/src/cbmc/bmc.h
@@ -208,6 +208,9 @@ class bmct:public safety_checkert
   virtual void report_success();
   virtual void report_failure();
 
+  static void report_success(messaget &, ui_message_handlert &);
+  static void report_failure(messaget &, ui_message_handlert &);
+
   virtual void error_trace();
   void output_graphml(resultt result);
 
diff --git a/src/goto-programs/safety_checker.h b/src/goto-programs/safety_checker.h
index b2aee4fab3e..21d2529b410 100644
--- a/src/goto-programs/safety_checker.h
+++ b/src/goto-programs/safety_checker.h
@@ -42,10 +42,6 @@ class safety_checkert:public messaget
     /// doing path exploration; the symex state has been saved, and symex should
     /// be resumed by the caller.
     PAUSED,
-    /// We haven't yet assigned a safety check result to this object. A value of
-    /// UNKNOWN can be used to initialize a resultt object, and that object may
-    /// then safely be used with the |= and &= operators.
-    UNKNOWN
   };
 
   // check whether all assertions in goto_functions are safe
@@ -76,9 +72,6 @@ operator&=(safety_checkert::resultt &a, safety_checkert::resultt const &b)
     b != safety_checkert::resultt::PAUSED);
   switch(a)
   {
-  case safety_checkert::resultt::UNKNOWN:
-    a = b;
-    return a;
   case safety_checkert::resultt::ERROR:
     return a;
   case safety_checkert::resultt::SAFE:
@@ -107,9 +100,6 @@ operator|=(safety_checkert::resultt &a, safety_checkert::resultt const &b)
     b != safety_checkert::resultt::PAUSED);
   switch(a)
   {
-  case safety_checkert::resultt::UNKNOWN:
-    a = b;
-    return a;
   case safety_checkert::resultt::SAFE:
     return a;
   case safety_checkert::resultt::ERROR:
diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
index 667f85039ef..90594da545b 100644
--- a/src/goto-symex/goto_symex.h
+++ b/src/goto-symex/goto_symex.h
@@ -70,6 +70,7 @@ class goto_symext
       log(mh),
       guard_identifier("goto_symex::\\guard"),
       path_storage(path_storage),
+      path_segment_vccs(0),
       _total_vccs(std::numeric_limits<unsigned>::max()),
       _remaining_vccs(std::numeric_limits<unsigned>::max())
   {
@@ -464,6 +465,18 @@ class goto_symext
 
   path_storaget &path_storage;
 
+public:
+  /// \brief Number of VCCs generated during the run of this goto_symext object
+  ///
+  /// This member is always initialized to `0` upon construction of this object.
+  /// It therefore differs from goto_symex_statet::total_vccs, which persists
+  /// across the creation of several goto_symext objects. When CBMC is run in
+  /// path-exploration mode, the meaning of this member is "the number of VCCs
+  /// generated between the last branch point and the current instruction,"
+  /// while goto_symex_statet::total_vccs records the total number of VCCs
+  /// generated along the entire path from the beginning of the program.
+  std::size_t path_segment_vccs;
+
 protected:
   /// @{\name Statistics
   ///
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
index fb213414477..e0d7b39790e 100644
--- a/src/goto-symex/symex_main.cpp
+++ b/src/goto-symex/symex_main.cpp
@@ -52,6 +52,7 @@ void goto_symext::vcc(
   statet &state)
 {
   state.total_vccs++;
+  path_segment_vccs++;
 
   exprt expr=vcc_expr;
 
diff --git a/unit/path_strategies.cpp b/unit/path_strategies.cpp
index d4b07f67ed4..17b8ef244b7 100644
--- a/unit/path_strategies.cpp
+++ b/unit/path_strategies.cpp
@@ -81,7 +81,6 @@ SCENARIO("path strategies")
       opts_callback,
       c,
       {symex_eventt::resume(symex_eventt::enumt::JUMP, 7),
-       symex_eventt::result(symex_eventt::enumt::SUCCESS),
        symex_eventt::resume(symex_eventt::enumt::NEXT, 5),
        symex_eventt::result(symex_eventt::enumt::SUCCESS)});
     check_with_strategy(
@@ -89,7 +88,6 @@ SCENARIO("path strategies")
       opts_callback,
       c,
       {symex_eventt::resume(symex_eventt::enumt::NEXT, 5),
-       symex_eventt::result(symex_eventt::enumt::SUCCESS),
        symex_eventt::resume(symex_eventt::enumt::JUMP, 7),
        symex_eventt::result(symex_eventt::enumt::SUCCESS)});
   }
@@ -125,14 +123,11 @@ SCENARIO("path strategies")
       {// Outer else, inner else
        symex_eventt::resume(symex_eventt::enumt::JUMP, 13),
        symex_eventt::resume(symex_eventt::enumt::JUMP, 16),
-       symex_eventt::result(symex_eventt::enumt::SUCCESS),
        // Outer else, inner if
        symex_eventt::resume(symex_eventt::enumt::NEXT, 14),
-       symex_eventt::result(symex_eventt::enumt::SUCCESS),
        // Outer if, inner else
        symex_eventt::resume(symex_eventt::enumt::NEXT, 6),
        symex_eventt::resume(symex_eventt::enumt::JUMP, 9),
-       symex_eventt::result(symex_eventt::enumt::SUCCESS),
        // Outer if, inner if
        symex_eventt::resume(symex_eventt::enumt::NEXT, 7),
        symex_eventt::result(symex_eventt::enumt::SUCCESS)});
@@ -147,13 +142,9 @@ SCENARIO("path strategies")
        symex_eventt::resume(symex_eventt::enumt::JUMP, 13),
        // Expand inner if of the outer if
        symex_eventt::resume(symex_eventt::enumt::NEXT, 7),
-       // No more branch points, so complete the path
-       symex_eventt::result(symex_eventt::enumt::SUCCESS),
-       // Continue BFSing
+       // No more branch points, so complete the path. Then continue BFSing
        symex_eventt::resume(symex_eventt::enumt::JUMP, 9),
-       symex_eventt::result(symex_eventt::enumt::SUCCESS),
        symex_eventt::resume(symex_eventt::enumt::NEXT, 14),
-       symex_eventt::result(symex_eventt::enumt::SUCCESS),
        symex_eventt::resume(symex_eventt::enumt::JUMP, 16),
        symex_eventt::result(symex_eventt::enumt::SUCCESS)});
   }
@@ -199,6 +190,9 @@ SCENARIO("path strategies")
         // infeasible.
         symex_eventt::resume(symex_eventt::enumt::NEXT, 7),
         symex_eventt::result(symex_eventt::enumt::SUCCESS),
+
+        // Overall we fail.
+        symex_eventt::result(symex_eventt::enumt::FAILURE),
       });
 
     check_with_strategy(
@@ -224,6 +218,9 @@ SCENARIO("path strategies")
         // executing the loop once, decrementing x to 0; assert(x) should fail.
         symex_eventt::resume(symex_eventt::enumt::JUMP, 9),
         symex_eventt::result(symex_eventt::enumt::FAILURE),
+
+        // Overall we fail.
+        symex_eventt::result(symex_eventt::enumt::FAILURE),
       });
   }
 
@@ -253,6 +250,8 @@ SCENARIO("path strategies")
         {symex_eventt::resume(symex_eventt::enumt::JUMP, 7),
          symex_eventt::result(symex_eventt::enumt::FAILURE),
          symex_eventt::resume(symex_eventt::enumt::NEXT, 5),
+         symex_eventt::result(symex_eventt::enumt::FAILURE),
+         // Overall result
          symex_eventt::result(symex_eventt::enumt::FAILURE)});
     }
     GIVEN("stopping on failure")
@@ -262,6 +261,8 @@ SCENARIO("path strategies")
         halt_callback,
         c,
         {symex_eventt::resume(symex_eventt::enumt::JUMP, 7),
+         symex_eventt::result(symex_eventt::enumt::FAILURE),
+         // Overall result
          symex_eventt::result(symex_eventt::enumt::FAILURE)});
     }
   }
@@ -272,12 +273,14 @@ SCENARIO("path strategies")
 
 void symex_eventt::validate_result(
   listt &events,
-  const safety_checkert::resultt result)
+  const safety_checkert::resultt result,
+  std::size_t &counter)
 {
   INFO(
     "Expecting result to be '"
     << (result == safety_checkert::resultt::SAFE ? "success" : "failure")
-    << "'");
+    << "' (item at index [" << counter << "] in expected results list");
+  ++counter;
 
   REQUIRE(result != safety_checkert::resultt::ERROR);
 
@@ -297,7 +300,8 @@ void symex_eventt::validate_result(
 
 void symex_eventt::validate_resume(
   listt &events,
-  const goto_symex_statet &state)
+  const goto_symex_statet &state,
+  std::size_t &counter)
 {
   REQUIRE(!events.empty());
 
@@ -305,17 +309,24 @@ void symex_eventt::validate_resume(
 
   if(state.has_saved_jump_target)
   {
-    INFO("Expecting resume to be 'jump' to line " << dst);
+    INFO(
+      "Expecting resume to be 'jump' to line "
+      << dst << " (item at index [" << counter
+      << "] in expected resumes list)");
     REQUIRE(events.front().first == symex_eventt::enumt::JUMP);
   }
   else if(state.has_saved_next_instruction)
   {
-    INFO("Expecting resume to be 'next' to line " << dst);
+    INFO(
+      "Expecting resume to be 'next' to line "
+      << dst << " (item at index [" << counter
+      << "] in expected resumes list)");
     REQUIRE(events.front().first == symex_eventt::enumt::NEXT);
   }
   else
     REQUIRE(false);
 
+  ++counter;
   REQUIRE(events.front().second == dst);
 
   events.pop_front();
@@ -370,12 +381,20 @@ void _check_with_strategy(
   prop_convt &pc = cbmc_solver->prop_conv();
   std::function<bool(void)> callback = []() { return false; };
 
+  safety_checkert::resultt overall_result = safety_checkert::resultt::SAFE;
+  std::size_t expected_results_cnt = 0;
+
   bmct bmc(opts, gm.get_symbol_table(), mh, pc, *worklist, callback);
-  safety_checkert::resultt result = bmc.run(gm);
-  symex_eventt::validate_result(events, result);
+  safety_checkert::resultt tmp_result = bmc.run(gm);
+
+  if(tmp_result != safety_checkert::resultt::PAUSED)
+  {
+    symex_eventt::validate_result(events, tmp_result, expected_results_cnt);
+    overall_result &= tmp_result;
+  }
 
   if(
-    result == safety_checkert::resultt::UNSAFE &&
+    overall_result == safety_checkert::resultt::UNSAFE &&
     opts.get_bool_option("stop-on-fail") && opts.is_set("paths"))
   {
     worklist->clear();
@@ -388,7 +407,7 @@ void _check_with_strategy(
     prop_convt &pc = cbmc_solver->prop_conv();
     path_storaget::patht &resume = worklist->peek();
 
-    symex_eventt::validate_resume(events, resume.state);
+    symex_eventt::validate_resume(events, resume.state, expected_results_cnt);
 
     path_explorert pe(
       opts,
@@ -399,17 +418,25 @@ void _check_with_strategy(
       resume.state,
       *worklist,
       callback);
-    result = pe.run(gm);
+    tmp_result = pe.run(gm);
 
-    symex_eventt::validate_result(events, result);
+    if(tmp_result != safety_checkert::resultt::PAUSED)
+    {
+      symex_eventt::validate_result(events, tmp_result, expected_results_cnt);
+      overall_result &= tmp_result;
+    }
     worklist->pop();
 
     if(
-      result == safety_checkert::resultt::UNSAFE &&
+      overall_result == safety_checkert::resultt::UNSAFE &&
       opts.get_bool_option("stop-on-fail"))
     {
       worklist->clear();
     }
   }
+
+  symex_eventt::validate_result(events, overall_result, expected_results_cnt);
+
+  INFO("The expected results list contains " << events.size() << " items");
   REQUIRE(events.empty());
 }
diff --git a/unit/path_strategies.h b/unit/path_strategies.h
index cc0096095e1..c9537896194 100644
--- a/unit/path_strategies.h
+++ b/unit/path_strategies.h
@@ -36,10 +36,13 @@ struct symex_eventt
     return pairt(kind, -1);
   }
 
-  static void
-  validate_result(listt &events, const safety_checkert::resultt result);
+  static void validate_result(
+    listt &events,
+    const safety_checkert::resultt result,
+    std::size_t &);
 
-  static void validate_resume(listt &events, const goto_symex_statet &state);
+  static void
+  validate_resume(listt &events, const goto_symex_statet &state, std::size_t &);
 };
 
 void _check_with_strategy(