From a3f9591a5f9b57583ed62c18e6efa6ec85e9c9d6 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Thu, 7 Feb 2019 12:08:05 +0000
Subject: [PATCH 1/5] Remove obsolete variant of symex_with_state

This variant did not support lazy loading
and was only used by scratch_program,
which can as well use the more general variant.
---
 .../accelerate/scratch_program.cpp            |  7 ++++-
 src/goto-symex/goto_symex.h                   | 17 +++--------
 src/goto-symex/symex_main.cpp                 | 29 ++++++-------------
 3 files changed, 19 insertions(+), 34 deletions(-)

diff --git a/src/goto-instrument/accelerate/scratch_program.cpp b/src/goto-instrument/accelerate/scratch_program.cpp
index 069f0b4b6b9..6297922c260 100644
--- a/src/goto-instrument/accelerate/scratch_program.cpp
+++ b/src/goto-instrument/accelerate/scratch_program.cpp
@@ -35,7 +35,12 @@ bool scratch_programt::check_sat(bool do_slice)
   output(ns, "scratch", std::cout);
 #endif
 
-  symex.symex_with_state(symex_state, functions, symex_symbol_table);
+  symex.symex_with_state(
+    symex_state,
+    [this](const irep_idt &key) -> const goto_functionst::goto_functiont & {
+      return functions.function_map.at(key);
+    },
+    symex_symbol_table);
 
   if(do_slice)
   {
diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
index 962a7cad55f..8c2e0a894f1 100644
--- a/src/goto-symex/goto_symex.h
+++ b/src/goto-symex/goto_symex.h
@@ -15,7 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/options.h>
 #include <util/message.h>
 
-#include <goto-programs/goto_functions.h>
+#include <goto-programs/abstract_goto_model.h>
 
 #include "goto_symex_state.h"
 #include "path_storage.h"
@@ -97,6 +97,9 @@ class goto_symext
     std::function<const goto_functionst::goto_functiont &(const irep_idt &)>
     get_goto_functiont;
 
+  /// Return a function to get/load a goto function from the given goto model
+  static get_goto_functiont get_goto_function(abstract_goto_modelt &);
+
   /// \brief symex entire program starting from entry point
   ///
   /// The state that goto_symext maintains has a large memory footprint.
@@ -117,18 +120,6 @@ class goto_symext
     symex_target_equationt *saved_equation,
     symbol_tablet &new_symbol_table);
 
-  //// \brief symex entire program starting from entry point
-  ///
-  /// This method uses the `state` argument as the symbolic execution
-  /// state, which is useful for examining the state after this method
-  /// returns. The state that goto_symext maintains has a large memory
-  /// footprint, so if keeping the state around is not necessary,
-  /// clients should instead call goto_symext::symex_from_entry_point_of().
-  virtual void symex_with_state(
-    statet &,
-    const goto_functionst &,
-    symbol_tablet &);
-
   //// \brief symex entire program starting from entry point
   ///
   /// This method uses the `state` argument as the symbolic execution
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
index 16a3d4b331b..1f987a6aceb 100644
--- a/src/goto-symex/symex_main.cpp
+++ b/src/goto-symex/symex_main.cpp
@@ -229,26 +229,6 @@ void goto_symext::symex_threaded_step(
   }
 }
 
-static goto_symext::get_goto_functiont get_function_from_goto_functions(
-  const goto_functionst &goto_functions)
-{
-  return [&goto_functions](
-           const irep_idt &key) -> const goto_functionst::goto_functiont & {
-    return goto_functions.function_map.at(key);
-  };
-}
-
-void goto_symext::symex_with_state(
-  statet &state,
-  const goto_functionst &goto_functions,
-  symbol_tablet &new_symbol_table)
-{
-  symex_with_state(
-    state,
-    get_function_from_goto_functions(goto_functions),
-    new_symbol_table);
-}
-
 void goto_symext::symex_with_state(
   statet &state,
   const get_goto_functiont &get_goto_function,
@@ -354,6 +334,15 @@ void goto_symext::symex_from_entry_point_of(
     state, get_goto_function, new_symbol_table);
 }
 
+goto_symext::get_goto_functiont
+goto_symext::get_goto_function(abstract_goto_modelt &goto_model)
+{
+  return [&goto_model](
+           const irep_idt &id) -> const goto_functionst::goto_functiont & {
+    return goto_model.get_goto_function(id);
+  };
+}
+
 /// do just one step
 void goto_symext::symex_step(
   const get_goto_functiont &get_goto_function,

From 8592f2836576f43fadea42e58f547534aaf494a1 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Wed, 6 Feb 2019 20:57:44 +0000
Subject: [PATCH 2/5] Put initial state into path_storage

Allows us to perform the actual pathwise symex work
in a uniform way.
Required making path_storaget::push accept a single state.
---
 src/goto-symex/goto_symex.h     | 13 +++++++++++++
 src/goto-symex/path_storage.cpp | 14 ++++----------
 src/goto-symex/path_storage.h   | 16 ++++------------
 src/goto-symex/symex_goto.cpp   |  3 ++-
 src/goto-symex/symex_main.cpp   | 30 +++++++++++++++++++++++++-----
 5 files changed, 48 insertions(+), 28 deletions(-)

diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
index 8c2e0a894f1..25fb0db0a83 100644
--- a/src/goto-symex/goto_symex.h
+++ b/src/goto-symex/goto_symex.h
@@ -110,6 +110,11 @@ class goto_symext
     const get_goto_functiont &get_goto_function,
     symbol_tablet &new_symbol_table);
 
+  /// Puts the initial state of the entry point function into the path storage
+  virtual void initialize_path_storage_from_entry_point_of(
+    const get_goto_functiont &get_goto_function,
+    symbol_tablet &new_symbol_table);
+
   /// Performs symbolic execution using a state and equation that have
   /// already been used to symex part of the program. The state is not
   /// re-initialized; instead, symbolic execution resumes from the program
@@ -159,6 +164,14 @@ class goto_symext
     goto_programt::const_targett pc,
     goto_programt::const_targett limit);
 
+  /// Initialize the symbolic execution and the given state with
+  /// the beginning of the entry point function.
+  /// \param get_goto_function: producer for GOTO functions
+  /// \param state: Symex state to initialize.
+  void initialize_entry_point_state(
+    const get_goto_functiont &get_goto_function,
+    statet &state);
+
   /// Invokes symex_step and verifies whether additional threads can be
   /// executed.
   /// \param state: Current GOTO symex step.
diff --git a/src/goto-symex/path_storage.cpp b/src/goto-symex/path_storage.cpp
index 39cfeaffd5c..244ecac3d48 100644
--- a/src/goto-symex/path_storage.cpp
+++ b/src/goto-symex/path_storage.cpp
@@ -29,12 +29,9 @@ path_storaget::patht &path_lifot::private_peek()
   return paths.back();
 }
 
-void path_lifot::push(
-  const path_storaget::patht &next_instruction,
-  const path_storaget::patht &jump_target)
+void path_lifot::push(const path_storaget::patht &path)
 {
-  paths.push_back(next_instruction);
-  paths.push_back(jump_target);
+  paths.push_back(path);
 }
 
 void path_lifot::private_pop()
@@ -62,12 +59,9 @@ path_storaget::patht &path_fifot::private_peek()
   return paths.front();
 }
 
-void path_fifot::push(
-  const path_storaget::patht &next_instruction,
-  const path_storaget::patht &jump_target)
+void path_fifot::push(const path_storaget::patht &path)
 {
-  paths.push_back(next_instruction);
-  paths.push_back(jump_target);
+  paths.push_back(path);
 }
 
 void path_fifot::private_pop()
diff --git a/src/goto-symex/path_storage.h b/src/goto-symex/path_storage.h
index b22c760ad02..dacf0498ac7 100644
--- a/src/goto-symex/path_storage.h
+++ b/src/goto-symex/path_storage.h
@@ -68,16 +68,8 @@ class path_storaget
   /// that check that the worklist is always empty when symex finishes.
   virtual void clear() = 0;
 
-  /// \brief Add paths to resume to the storage
-  ///
-  /// Symbolic execution is suspended when we reach a conditional goto
-  /// instruction with two successors. Thus, we always add a pair of paths to
-  /// the path storage.
-  ///
-  /// \param next_instruction: the instruction following the goto instruction
-  /// \param jump_target: the target instruction of the goto instruction
-  virtual void
-  push(const patht &next_instruction, const patht &jump_target) = 0;
+  /// \brief Add a path to resume to the storage
+  virtual void push(const patht &) = 0;
 
   /// \brief Remove the next path to resume from the storage
   void pop()
@@ -109,7 +101,7 @@ class path_storaget
 class path_lifot : public path_storaget
 {
 public:
-  void push(const patht &, const patht &) override;
+  void push(const patht &) override;
   std::size_t size() const override;
   void clear() override;
 
@@ -126,7 +118,7 @@ class path_lifot : public path_storaget
 class path_fifot : public path_storaget
 {
 public:
-  void push(const patht &, const patht &) override;
+  void push(const patht &) override;
   std::size_t size() const override;
   void clear() override;
 
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
index c32ca2e7496..e5977b63ecc 100644
--- a/src/goto-symex/symex_goto.cpp
+++ b/src/goto-symex/symex_goto.cpp
@@ -207,7 +207,8 @@ void goto_symext::symex_goto(statet &state)
     log.debug() << "Saving jump target '"
                 << jump_target.state.saved_target->source_location << "'"
                 << log.eom;
-    path_storage.push(next_instruction, jump_target);
+    path_storage.push(next_instruction);
+    path_storage.push(jump_target);
 
     // It is now up to the caller of symex to decide which path to continue
     // executing. Signal to the caller that states have been pushed (therefore
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
index 1f987a6aceb..24f2cbb45f5 100644
--- a/src/goto-symex/symex_main.cpp
+++ b/src/goto-symex/symex_main.cpp
@@ -305,9 +305,9 @@ void goto_symext::resume_symex_from_saved_state(
       new_symbol_table);
 }
 
-void goto_symext::symex_from_entry_point_of(
+void goto_symext::initialize_entry_point_state(
   const get_goto_functiont &get_goto_function,
-  symbol_tablet &new_symbol_table)
+  statet &state)
 {
   const goto_functionst::goto_functiont *start_function;
   try
@@ -319,8 +319,6 @@ void goto_symext::symex_from_entry_point_of(
     throw unsupported_operation_exceptiont("the program has no entry point");
   }
 
-  statet state;
-
   state.run_validation_checks = symex_config.run_validation_checks;
 
   initialize_entry_point(
@@ -328,12 +326,34 @@ void goto_symext::symex_from_entry_point_of(
     get_goto_function,
     goto_functionst::entry_point(),
     start_function->body.instructions.begin(),
-    prev(start_function->body.instructions.end()));
+    std::prev(start_function->body.instructions.end()));
+}
+
+void goto_symext::symex_from_entry_point_of(
+  const get_goto_functiont &get_goto_function,
+  symbol_tablet &new_symbol_table)
+{
+  statet state;
+  initialize_entry_point_state(get_goto_function, state);
 
   symex_with_state(
     state, get_goto_function, new_symbol_table);
 }
 
+void goto_symext::initialize_path_storage_from_entry_point_of(
+  const get_goto_functiont &get_goto_function,
+  symbol_tablet &new_symbol_table)
+{
+  statet state;
+  initialize_entry_point_state(get_goto_function, state);
+
+  path_storaget::patht entry_point_start(target, state);
+  entry_point_start.state.saved_target = state.source.pc;
+  entry_point_start.state.has_saved_next_instruction = true;
+
+  path_storage.push(entry_point_start);
+}
+
 goto_symext::get_goto_functiont
 goto_symext::get_goto_function(abstract_goto_modelt &goto_model)
 {

From 0cf4c464e7e6aca61841d8fefa7abe8b4c674d24 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Wed, 6 Feb 2019 21:57:01 +0000
Subject: [PATCH 3/5] Expose equation post-processing

Will allow us to remove perform_symex utilities later
---
 src/goto-checker/bmc_util.cpp |  2 +-
 src/goto-checker/bmc_util.h   | 11 +++++++++++
 2 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/src/goto-checker/bmc_util.cpp b/src/goto-checker/bmc_util.cpp
index 89f1d421b17..156fb7a915b 100644
--- a/src/goto-checker/bmc_util.cpp
+++ b/src/goto-checker/bmc_util.cpp
@@ -302,7 +302,7 @@ void output_coverage_report(
   }
 }
 
-static void postprocess_equation(
+void postprocess_equation(
   symex_bmct &symex,
   symex_target_equationt &equation,
   const optionst &options,
diff --git a/src/goto-checker/bmc_util.h b/src/goto-checker/bmc_util.h
index 271dc97888b..5d449810c2b 100644
--- a/src/goto-checker/bmc_util.h
+++ b/src/goto-checker/bmc_util.h
@@ -70,6 +70,17 @@ void slice(
   const optionst &,
   ui_message_handlert &);
 
+/// Post process the equation
+/// - add partial order constraints
+/// - slice
+/// - perform validation
+void postprocess_equation(
+  symex_bmct &symex,
+  symex_target_equationt &equation,
+  const optionst &options,
+  const namespacet &ns,
+  ui_message_handlert &ui_message_handler);
+
 /// Perform symbolic execution from the entry point
 void perform_symex(
   abstract_goto_modelt &,

From 2b1d9f4d37897ca549a7ec4b681c0e5e8a442842 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Wed, 6 Feb 2019 21:57:21 +0000
Subject: [PATCH 4/5] Simplify single-path symex checker

Instead of handling the first symex run differently:
Push initial state into the worklist,
then iterate symex until done.
---
 .../single_path_symex_checker.cpp             | 90 ++++++-------------
 src/goto-checker/single_path_symex_checker.h  |  3 +-
 .../single_path_symex_only_checker.cpp        | 39 ++++----
 3 files changed, 43 insertions(+), 89 deletions(-)

diff --git a/src/goto-checker/single_path_symex_checker.cpp b/src/goto-checker/single_path_symex_checker.cpp
index 63168332592..372c7fea75e 100644
--- a/src/goto-checker/single_path_symex_checker.cpp
+++ b/src/goto-checker/single_path_symex_checker.cpp
@@ -30,45 +30,6 @@ operator()(propertiest &properties)
 {
   resultt result(resultt::progresst::DONE);
 
-  // Unfortunately, the initial symex run is currently handled differently
-  // from the subsequent runs
-  if(!initial_symex_has_run)
-  {
-    initial_symex_has_run = true;
-    first_equation = symex_target_equationt();
-    symex_bmct symex(
-      ui_message_handler,
-      goto_model.get_symbol_table(),
-      first_equation.value(),
-      options,
-      *worklist);
-
-    setup_symex(symex);
-    perform_symex(
-      goto_model,
-      symex,
-      symex_symbol_table,
-      first_equation.value(),
-      options,
-      ns,
-      ui_message_handler);
-
-    output_coverage_report(
-      options.get_option("symex-coverage-report"),
-      goto_model,
-      symex,
-      ui_message_handler);
-
-    if(symex.get_remaining_vccs() > 0)
-    {
-      prepare(result, properties, first_equation.value());
-      decide(result, properties);
-
-      if(result.progress == resultt::progresst::FOUND_FAIL)
-        return result;
-    }
-  }
-
   // There might be more solutions from the previous equation.
   if(property_decider)
   {
@@ -77,24 +38,28 @@ operator()(propertiest &properties)
       return result;
   }
 
-  if(first_equation.has_value())
+  if(!worklist->empty())
   {
-    // We are in the second iteration. We don't need the equation
-    // from the first iteration anymore.
-    first_equation = {};
+    // We pop the item processed in the previous iteration.
+    worklist->pop();
   }
-  else
+
+  if(!symex_initialized)
   {
-    if(!worklist->empty())
-    {
-      // We are in iteration 3 or later; we pop the item processed
-      // in the previous iteration.
-      worklist->pop();
-    }
-    else
-    {
-      // We are already done.
-    }
+    symex_initialized = true;
+
+    // Put initial state into the work list
+    symex_target_equationt equation;
+    symex_bmct symex(
+      ui_message_handler,
+      goto_model.get_symbol_table(),
+      equation,
+      options,
+      *worklist);
+    setup_symex(symex);
+
+    symex.initialize_path_storage_from_entry_point_of(
+      goto_symext::get_goto_function(goto_model), symex_symbol_table);
   }
 
   while(!worklist->empty())
@@ -106,16 +71,15 @@ operator()(propertiest &properties)
       resume.equation,
       options,
       *worklist);
-
     setup_symex(symex);
-    perform_symex(
-      goto_model,
-      symex,
-      resume,
-      symex_symbol_table,
-      options,
-      ns,
-      ui_message_handler);
+
+    symex.resume_symex_from_saved_state(
+      goto_symext::get_goto_function(goto_model),
+      resume.state,
+      &resume.equation,
+      symex_symbol_table);
+    postprocess_equation(
+      symex, resume.equation, options, ns, ui_message_handler);
 
     output_coverage_report(
       options.get_option("symex-coverage-report"),
diff --git a/src/goto-checker/single_path_symex_checker.h b/src/goto-checker/single_path_symex_checker.h
index 205f09baf2b..c7c74359a70 100644
--- a/src/goto-checker/single_path_symex_checker.h
+++ b/src/goto-checker/single_path_symex_checker.h
@@ -43,8 +43,7 @@ class single_path_symex_checkert : public single_path_symex_only_checkert,
   virtual ~single_path_symex_checkert() = default;
 
 protected:
-  bool initial_symex_has_run = false;
-  optionalt<symex_target_equationt> first_equation; // for building traces
+  bool symex_initialized = false;
   std::unique_ptr<goto_symex_property_decidert> property_decider;
 
   void prepare(
diff --git a/src/goto-checker/single_path_symex_only_checker.cpp b/src/goto-checker/single_path_symex_only_checker.cpp
index 29c4dde9bf0..beed2920325 100644
--- a/src/goto-checker/single_path_symex_only_checker.cpp
+++ b/src/goto-checker/single_path_symex_only_checker.cpp
@@ -37,29 +37,19 @@ operator()(propertiest &properties)
 {
   resultt result(resultt::progresst::DONE);
 
-  // First run goto-symex from entry point to initialize worklist
   {
-    symex_target_equationt first_equation;
+    // Put initial state into the work list
+    symex_target_equationt equation;
     symex_bmct symex(
       ui_message_handler,
       goto_model.get_symbol_table(),
-      first_equation,
+      equation,
       options,
       *worklist);
-
     setup_symex(symex);
-    perform_symex(
-      goto_model,
-      symex,
-      symex_symbol_table,
-      first_equation,
-      options,
-      ns,
-      ui_message_handler);
 
-    equation_output(symex, first_equation);
-    update_properties_status_from_symex_target_equation(
-      properties, result.updated_properties, first_equation);
+    symex.initialize_path_storage_from_entry_point_of(
+      goto_symext::get_goto_function(goto_model), symex_symbol_table);
   }
 
   while(!worklist->empty())
@@ -71,17 +61,18 @@ operator()(propertiest &properties)
       resume.equation,
       options,
       *worklist);
-
     setup_symex(symex);
-    perform_symex(
-      goto_model,
-      symex,
-      resume,
-      symex_symbol_table,
-      options,
-      ns,
-      ui_message_handler);
+
+    symex.resume_symex_from_saved_state(
+      goto_symext::get_goto_function(goto_model),
+      resume.state,
+      &resume.equation,
+      symex_symbol_table);
+    postprocess_equation(
+      symex, resume.equation, options, ns, ui_message_handler);
+
     equation_output(symex, resume.equation);
+
     update_properties_status_from_symex_target_equation(
       properties, result.updated_properties, resume.equation);
 

From 5281fa654b9674517fa6b9aef67c4060de6a77d8 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Wed, 6 Feb 2019 21:58:49 +0000
Subject: [PATCH 5/5] Inline perform_symex utility functions

Only used once resp. obsolete.
---
 src/goto-checker/bmc_util.cpp                 | 41 -------------------
 src/goto-checker/bmc_util.h                   | 20 ---------
 src/goto-checker/multi_path_symex_checker.cpp | 11 ++---
 .../multi_path_symex_only_checker.cpp         | 11 ++---
 4 files changed, 6 insertions(+), 77 deletions(-)

diff --git a/src/goto-checker/bmc_util.cpp b/src/goto-checker/bmc_util.cpp
index 156fb7a915b..158dc54bfc1 100644
--- a/src/goto-checker/bmc_util.cpp
+++ b/src/goto-checker/bmc_util.cpp
@@ -329,44 +329,3 @@ void postprocess_equation(
     symex.validate(validation_modet::INVARIANT);
   }
 }
-
-void perform_symex(
-  abstract_goto_modelt &goto_model,
-  symex_bmct &symex,
-  symbol_tablet &symex_symbol_table,
-  symex_target_equationt &equation,
-  const optionst &options,
-  const namespacet &ns,
-  ui_message_handlert &ui_message_handler)
-{
-  auto get_goto_function =
-    [&goto_model](
-      const irep_idt &id) -> const goto_functionst::goto_functiont & {
-    return goto_model.get_goto_function(id);
-  };
-
-  symex.symex_from_entry_point_of(get_goto_function, symex_symbol_table);
-
-  postprocess_equation(symex, equation, options, ns, ui_message_handler);
-}
-
-void perform_symex(
-  abstract_goto_modelt &goto_model,
-  symex_bmct &symex,
-  path_storaget::patht &resume,
-  symbol_tablet &symex_symbol_table,
-  const optionst &options,
-  const namespacet &ns,
-  ui_message_handlert &ui_message_handler)
-{
-  auto get_goto_function =
-    [&goto_model](
-      const irep_idt &id) -> const goto_functionst::goto_functiont & {
-    return goto_model.get_goto_function(id);
-  };
-
-  symex.resume_symex_from_saved_state(
-    get_goto_function, resume.state, &resume.equation, symex_symbol_table);
-
-  postprocess_equation(symex, resume.equation, options, ns, ui_message_handler);
-}
diff --git a/src/goto-checker/bmc_util.h b/src/goto-checker/bmc_util.h
index 5d449810c2b..101730072bb 100644
--- a/src/goto-checker/bmc_util.h
+++ b/src/goto-checker/bmc_util.h
@@ -81,26 +81,6 @@ void postprocess_equation(
   const namespacet &ns,
   ui_message_handlert &ui_message_handler);
 
-/// Perform symbolic execution from the entry point
-void perform_symex(
-  abstract_goto_modelt &,
-  symex_bmct &,
-  symbol_tablet &,
-  symex_target_equationt &,
-  const optionst &,
-  const namespacet &,
-  ui_message_handlert &);
-
-/// Perform symbolic execution starting from \p resume.
-void perform_symex(
-  abstract_goto_modelt &,
-  symex_bmct &,
-  path_storaget::patht &resume,
-  symbol_tablet &,
-  const optionst &,
-  const namespacet &,
-  ui_message_handlert &);
-
 /// Output a coverage report as generated by \ref symex_coveraget
 /// if \p cov_out is non-empty.
 /// \param cov_out: file to write the report to; no report is generated
diff --git a/src/goto-checker/multi_path_symex_checker.cpp b/src/goto-checker/multi_path_symex_checker.cpp
index 838839da5b6..64872c2c827 100644
--- a/src/goto-checker/multi_path_symex_checker.cpp
+++ b/src/goto-checker/multi_path_symex_checker.cpp
@@ -41,14 +41,9 @@ operator()(propertiest &properties)
   // we haven't got an equation yet
   if(!equation_generated)
   {
-    perform_symex(
-      goto_model,
-      symex,
-      symex_symbol_table,
-      equation,
-      options,
-      ns,
-      ui_message_handler);
+    symex.symex_from_entry_point_of(
+      goto_symext::get_goto_function(goto_model), symex_symbol_table);
+    postprocess_equation(symex, equation, options, ns, ui_message_handler);
 
     output_coverage_report(
       options.get_option("symex-coverage-report"),
diff --git a/src/goto-checker/multi_path_symex_only_checker.cpp b/src/goto-checker/multi_path_symex_only_checker.cpp
index 4fbb22f2d8a..9ad65517557 100644
--- a/src/goto-checker/multi_path_symex_only_checker.cpp
+++ b/src/goto-checker/multi_path_symex_only_checker.cpp
@@ -39,14 +39,9 @@ multi_path_symex_only_checkert::multi_path_symex_only_checkert(
 incremental_goto_checkert::resultt multi_path_symex_only_checkert::
 operator()(propertiest &properties)
 {
-  perform_symex(
-    goto_model,
-    symex,
-    symex_symbol_table,
-    equation,
-    options,
-    ns,
-    ui_message_handler);
+  symex.symex_from_entry_point_of(
+    goto_symext::get_goto_function(goto_model), symex_symbol_table);
+  postprocess_equation(symex, equation, options, ns, ui_message_handler);
 
   output_coverage_report(
     options.get_option("symex-coverage-report"),