diff --git a/.gitignore b/.gitignore
index ea8be88725b..9693fb2faef 100644
--- a/.gitignore
+++ b/.gitignore
@@ -101,6 +101,7 @@ src/goto-cc/goto-cc.exe
 src/goto-cc/goto-cl.exe
 src/goto-instrument/goto-instrument
 src/goto-instrument/goto-instrument.exe
+src/jbmc/jbmc
 src/musketeer/musketeer
 src/musketeer/musketeer.exe
 src/symex/symex
diff --git a/scripts/cpplint.py b/scripts/cpplint.py
index 4b4aac788f8..bb08391f4d9 100755
--- a/scripts/cpplint.py
+++ b/scripts/cpplint.py
@@ -3625,8 +3625,8 @@ def CheckOperatorSpacing(filename, clean_lines, linenum, error):
 #          'Remove spaces around %s' % match.group(0))
 
 # check any inherited classes don't have a space between the type and the :
-  if Search(r'(struct|class)\s[\w_]*\s+:', line):
-    error(filename, linenum, 'readability/identifier_spacing', 4, 'There shouldn\'t be a space between class identifier and :')
+  if Search(r'(struct|class)\s[\w_]*:', line):
+    error(filename, linenum, 'readability/identifier_spacing', 4, 'There should be a space between class identifier and :')
 
   #check type definitions end with t
   # Look for class declarations and check the final character is a t
diff --git a/src/analyses/dirty.cpp b/src/analyses/dirty.cpp
index b40e057a975..66c40141db8 100644
--- a/src/analyses/dirty.cpp
+++ b/src/analyses/dirty.cpp
@@ -69,6 +69,7 @@ void dirtyt::find_dirty_address_of(const exprt &expr)
 
 void dirtyt::output(std::ostream &out) const
 {
+  die_if_uninitialized();
   for(const auto &d : dirty)
     out << d << '\n';
 }
diff --git a/src/analyses/dirty.h b/src/analyses/dirty.h
index 880d01cb3ee..a50b8dbcaad 100644
--- a/src/analyses/dirty.h
+++ b/src/analyses/dirty.h
@@ -17,49 +17,80 @@ Date: March 2013
 #include <unordered_set>
 
 #include <util/std_expr.h>
+#include <util/invariant.h>
 #include <goto-programs/goto_functions.h>
 
 class dirtyt
 {
+private:
+  void die_if_uninitialized() const
+  {
+    INVARIANT(
+      initialized,
+      "Uninitialized dirtyt. This dirtyt was constructed using the default "
+      "constructor and not subsequently initialized using "
+      "dirtyt::build().");
+  }
+
 public:
+  bool initialized;
   typedef std::unordered_set<irep_idt, irep_id_hash> id_sett;
   typedef goto_functionst::goto_functiont goto_functiont;
 
-  dirtyt()
+  /// \post dirtyt objects that are created through this constructor are not
+  /// safe to use. If you copied a dirtyt (for example, by adding an object
+  /// that owns a dirtyt to a container and then copying it back out), you will
+  /// need to re-initialize the dirtyt by calling dirtyt::build().
+  dirtyt() : initialized(false)
   {
   }
 
-  explicit dirtyt(const goto_functiont &goto_function)
+  explicit dirtyt(const goto_functiont &goto_function) : initialized(false)
   {
     build(goto_function);
+    initialized = true;
   }
 
-  explicit dirtyt(const goto_functionst &goto_functions)
+  explicit dirtyt(const goto_functionst &goto_functions) : initialized(false)
   {
-    forall_goto_functions(it, goto_functions)
-      build(it->second);
+    build(goto_functions);
+    // build(g_funs) responsible for setting initialized to true, since
+    // it is public and can be called independently
   }
 
   void output(std::ostream &out) const;
 
   bool operator()(const irep_idt &id) const
   {
+    die_if_uninitialized();
     return dirty.find(id)!=dirty.end();
   }
 
   bool operator()(const symbol_exprt &expr) const
   {
+    die_if_uninitialized();
     return operator()(expr.get_identifier());
   }
 
   const id_sett &get_dirty_ids() const
   {
+    die_if_uninitialized();
     return dirty;
   }
 
   void add_function(const goto_functiont &goto_function)
   {
     build(goto_function);
+    initialized = true;
+  }
+
+  void build(const goto_functionst &goto_functions)
+  {
+    // dirtyts should not be initialized twice
+    PRECONDITION(!initialized);
+    forall_goto_functions(it, goto_functions)
+      build(it->second);
+    initialized = true;
   }
 
 protected:
diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
index 9bc86d3eec6..66ff5cb90ce 100644
--- a/src/cbmc/bmc.cpp
+++ b/src/cbmc/bmc.cpp
@@ -12,13 +12,16 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "bmc.h"
 
 #include <chrono>
+#include <exception>
 #include <fstream>
 #include <iostream>
 #include <memory>
 
+#include <util/exit_codes.h>
 #include <util/string2int.h>
 #include <util/source_location.h>
 #include <util/string_utils.h>
+#include <util/memory_info.h>
 #include <util/message.h>
 #include <util/json.h>
 #include <util/cprover_prefix.h>
@@ -26,6 +29,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <langapi/mode.h>
 #include <langapi/language_util.h>
 
+#include <goto-programs/goto_model.h>
 #include <goto-programs/xml_goto_trace.h>
 #include <goto-programs/json_goto_trace.h>
 #include <goto-programs/graphml_witness.h>
@@ -37,6 +41,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-symex/memory_model_tso.h>
 #include <goto-symex/memory_model_pso.h>
 
+#include "cbmc_solvers.h"
 #include "counterexample_beautification.h"
 #include "fault_localization.h"
 
@@ -359,8 +364,7 @@ safety_checkert::resultt bmct::execute(const goto_functionst &goto_functions)
 {
   try
   {
-    // perform symbolic execution
-    symex.symex_from_entry_point_of(goto_functions);
+    perform_symbolic_execution(goto_functions);
 
     // add a partial ordering, if required
     if(equation.has_threads())
@@ -595,3 +599,118 @@ void bmct::setup_unwind()
   if(options.get_option("unwind")!="")
     symex.set_unwind_limit(options.get_unsigned_int_option("unwind"));
 }
+
+int bmct::do_language_agnostic_bmc(
+  const optionst &opts,
+  const goto_modelt &goto_model,
+  const ui_message_handlert::uit &ui,
+  messaget &message,
+  std::function<void(bmct &, const goto_modelt &)> frontend_configure_bmc)
+{
+  message_handlert &mh = message.get_message_handler();
+  safety_checkert::resultt result;
+  goto_symext::branch_worklistt worklist;
+  try
+  {
+    {
+      cbmc_solverst solvers(
+        opts, goto_model.symbol_table, message.get_message_handler());
+      solvers.set_ui(ui);
+      std::unique_ptr<cbmc_solverst::solvert> cbmc_solver;
+      cbmc_solver = solvers.get_solver();
+      prop_convt &pc = cbmc_solver->prop_conv();
+      bmct bmc(opts, goto_model.symbol_table, mh, pc, worklist);
+      bmc.set_ui(ui);
+      frontend_configure_bmc(bmc, goto_model);
+      result = bmc.run(goto_model.goto_functions);
+    }
+    INVARIANT(
+      opts.get_bool_option("paths") || worklist.empty(),
+      "the worklist should be empty after doing full-program "
+      "model checking, but the worklist contains " +
+        std::to_string(worklist.size()) + " unexplored branches.");
+
+    // When model checking, the bmc.run() above will already have explored
+    // the entire program, and result contains the verification result. The
+    // worklist (containing paths that have not yet been explored) is thus
+    // empty, and we don't enter this loop.
+    //
+    // When doing path exploration, there will be some saved paths left to
+    // explore in the worklist. We thus need to run the above code again,
+    // once for each saved path in the worklist, to continue symbolically
+    // execute the program. Note that the code in the loop is similar to
+    // the code above except that we construct a path_explorert rather than
+    // a bmct, which allows us to execute from a saved state rather than
+    // from the entry point. See the path_explorert documentation, and the
+    // difference between the implementations of perform_symbolic_exection()
+    // in bmct and path_explorert, for more information.
+
+    while(!worklist.empty())
+    {
+      message.status() << "___________________________\n"
+                       << "Starting new path (" << worklist.size()
+                       << " to go)\n"
+                       << message.eom;
+      cbmc_solverst solvers(
+        opts, goto_model.symbol_table, message.get_message_handler());
+      solvers.set_ui(ui);
+      std::unique_ptr<cbmc_solverst::solvert> cbmc_solver;
+      cbmc_solver = solvers.get_solver();
+      prop_convt &pc = cbmc_solver->prop_conv();
+      goto_symext::branch_pointt &resume = worklist.front();
+      path_explorert pe(
+        opts,
+        goto_model.symbol_table,
+        mh,
+        pc,
+        resume.equation,
+        resume.state,
+        worklist);
+      frontend_configure_bmc(pe, goto_model);
+      result &= pe.run(goto_model.goto_functions);
+      worklist.pop_front();
+    }
+  }
+  catch(const char *error_msg)
+  {
+    message.error() << error_msg << message.eom;
+    return CPROVER_EXIT_EXCEPTION;
+  }
+  catch(const std::string &error_msg)
+  {
+    message.error() << error_msg << message.eom;
+    return CPROVER_EXIT_EXCEPTION;
+  }
+  catch(...)
+  {
+    message.error() << "unable to get solver" << message.eom;
+    throw std::current_exception();
+  }
+
+  switch(result)
+  {
+  case safety_checkert::resultt::SAFE:
+    return CPROVER_EXIT_VERIFICATION_SAFE;
+  case safety_checkert::resultt::UNSAFE:
+    return CPROVER_EXIT_VERIFICATION_UNSAFE;
+  case safety_checkert::resultt::ERROR:
+    return CPROVER_EXIT_INTERNAL_ERROR;
+  }
+  UNREACHABLE;
+}
+
+void bmct::perform_symbolic_execution(const goto_functionst &goto_functions)
+{
+  symex.symex_from_entry_point_of(goto_functions, symex_symbol_table);
+  INVARIANT(
+    options.get_bool_option("paths") || branch_worklist.empty(),
+    "Branch points were saved even though we should have been "
+    "executing the entire program and merging paths");
+}
+
+void path_explorert::perform_symbolic_execution(
+  const goto_functionst &goto_functions)
+{
+  symex.resume_symex_from_saved_state(
+    goto_functions, saved_state, &equation, symex_symbol_table);
+}
diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h
index b3f9a7846e1..8357b609aed 100644
--- a/src/cbmc/bmc.h
+++ b/src/cbmc/bmc.h
@@ -15,9 +15,12 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <list>
 #include <map>
 
+#include <util/invariant.h>
 #include <util/options.h>
 #include <util/ui_message.h>
 
+#include <java_bytecode/java_enum_static_init_unwind_handler.h>
+
 #include <solvers/prop/prop.h>
 #include <solvers/prop/prop_conv.h>
 #include <solvers/sat/cnf.h>
@@ -28,24 +31,57 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/goto_trace.h>
 
 #include <goto-symex/symex_target_equation.h>
+#include <goto-programs/goto_model.h>
 #include <goto-programs/safety_checker.h>
 #include <goto-symex/memory_model.h>
 
 #include "symex_bmc.h"
 
+class cbmc_solverst;
+
+/// \brief Bounded model checking or path exploration for goto-programs
+///
+/// Higher-level architectural information on symbolic execution is
+/// documented in the \ref symex-overview
+/// "Symbolic execution module page".
 class bmct:public safety_checkert
 {
 public:
+  /// \brief Constructor for path exploration with freshly-initialized state
+  ///
+  /// This constructor should be used for symbolically executing a program
+  /// from the entry point with fresh state. There are two main behaviours
+  /// that can happen when constructing an instance of this class:
+  ///
+  /// - If the `--paths` flag in the `options` argument to this
+  ///   constructor is `false` (unset), an instance of this class will
+  ///   symbolically execute the entire program, performing path merging
+  ///   to build a formula corresponding to all executions of the program
+  ///   up to the unwinding limit. In this case, the `branch_worklist`
+  ///   member shall not be touched; this is enforced by the assertion in
+  ///   this class' implementation of bmct::perform_symbolic_execution().
+  ///
+  /// - If the `--paths` flag is `true`, this `bmct` object will explore a
+  ///   single path through the codebase without doing any path merging.
+  ///   If some paths were not taken, the state at those branch points
+  ///   will be appended to `branch_worklist`. After the single path that
+  ///   this `bmct` object executed has been model-checked, you can resume
+  ///   exploring further paths by popping an element from
+  ///   `branch_worklist` and using it to construct a path_explorert
+  ///   object.
   bmct(
     const optionst &_options,
-    const symbol_tablet &_symbol_table,
+    const symbol_tablet &outer_symbol_table,
     message_handlert &_message_handler,
-    prop_convt &_prop_conv)
+    prop_convt &_prop_conv,
+    goto_symext::branch_worklistt &_branch_worklist)
     : safety_checkert(ns, _message_handler),
       options(_options),
-      ns(_symbol_table, new_symbol_table),
-      equation(ns),
-      symex(_message_handler, ns, new_symbol_table, equation),
+      outer_symbol_table(outer_symbol_table),
+      ns(outer_symbol_table, symex_symbol_table),
+      equation(),
+      branch_worklist(_branch_worklist),
+      symex(_message_handler, outer_symbol_table, equation, branch_worklist),
       prop_conv(_prop_conv),
       ui(ui_message_handlert::uit::PLAIN)
   {
@@ -82,11 +118,67 @@ class bmct:public safety_checkert
     symex.add_recursion_unwind_handler(handler);
   }
 
+  /// \brief common BMC code, invoked from language-specific frontends
+  ///
+  /// Do bounded model-checking after all language-specific program
+  /// preprocessing has been completed by language-specific frontends.
+  /// Language-specific frontends may customize the \ref bmct objects
+  /// that are used for model-checking by supplying a function object to
+  /// the `frontend_configure_bmc` parameter of this function; the
+  /// function object will be called with every \ref bmct object that
+  /// is constructed by `do_language_agnostic_bmc`.
+  static int do_language_agnostic_bmc(
+    const optionst &opts,
+    const goto_modelt &goto_model,
+    const ui_message_handlert::uit &ui,
+    messaget &message,
+    std::function<void(bmct &, const goto_modelt &)> frontend_configure_bmc =
+      [](bmct &_bmc, const goto_modelt &) { // NOLINT (*)
+        // Empty default implementation
+      });
+
 protected:
+  /// \brief Constructor for path exploration from saved state
+  ///
+  /// This constructor exists as a delegate for the path_explorert class.
+  /// It differs from \ref bmct's public constructor in that it actually
+  /// does something with the branch_worklistt argument, and also takes a
+  /// symex_target_equationt. See the documentation for path_explorert for
+  /// details.
+  bmct(
+    const optionst &_options,
+    const symbol_tablet &outer_symbol_table,
+    message_handlert &_message_handler,
+    prop_convt &_prop_conv,
+    symex_target_equationt &_equation,
+    goto_symext::branch_worklistt &_branch_worklist)
+    : safety_checkert(ns, _message_handler),
+      options(_options),
+      outer_symbol_table(outer_symbol_table),
+      ns(outer_symbol_table),
+      equation(_equation),
+      branch_worklist(_branch_worklist),
+      symex(_message_handler, outer_symbol_table, equation, branch_worklist),
+      prop_conv(_prop_conv),
+      ui(ui_message_handlert::uit::PLAIN)
+  {
+    symex.constant_propagation = options.get_bool_option("propagation");
+    symex.record_coverage =
+      !options.get_option("symex-coverage-report").empty();
+    INVARIANT(
+      options.get_bool_option("paths"),
+      "Should only use saved equation & goto_state constructor "
+      "when doing path exploration");
+  }
+
   const optionst &options;
-  symbol_tablet new_symbol_table;
+  /// \brief symbol table for the goto-program that we will execute
+  const symbol_tablet &outer_symbol_table;
+  /// \brief symbol table generated during symbolic execution
+  symbol_tablet symex_symbol_table;
   namespacet ns;
   symex_target_equationt equation;
+  goto_symext::branch_worklistt &branch_worklist;
   symex_bmct symex;
   prop_convt &prop_conv;
   std::unique_ptr<memory_model_baset> memory_model;
@@ -144,6 +236,93 @@ class bmct:public safety_checkert
   template <template <class goalt> class covert>
   friend class bmc_goal_covert;
   friend class fault_localizationt;
+
+private:
+  /// \brief Class-specific symbolic execution
+  ///
+  /// This private virtual should be overridden by derived classes to
+  /// invoke the symbolic executor in a class-specific way. This
+  /// implementation invokes goto_symext::operator() to perform
+  /// full-program model-checking from the entry point of the program.
+  virtual void
+  perform_symbolic_execution(const goto_functionst &goto_functions);
+};
+
+/// \brief Symbolic execution from a saved branch point
+///
+/// Instances of this class execute a single program path from a saved
+/// branch point. The saved branch point is supplied to the constructor
+/// as a pair of goto_target_equationt (which holds the SSA steps
+/// executed so far), and a goto_symex_statet Note that the \ref bmct
+/// base class can also execute a single path (it will do so if the
+/// `--paths` flag is set in its `options` member), but will always
+/// begin symbolic execution from the beginning of the program with
+/// fresh state.
+class path_explorert : public bmct
+{
+public:
+  path_explorert(
+    const optionst &_options,
+    const symbol_tablet &outer_symbol_table,
+    message_handlert &_message_handler,
+    prop_convt &_prop_conv,
+    symex_target_equationt &saved_equation,
+    const goto_symex_statet &saved_state,
+    goto_symext::branch_worklistt &branch_worklist)
+    : bmct(
+        _options,
+        outer_symbol_table,
+        _message_handler,
+        _prop_conv,
+        saved_equation,
+        branch_worklist),
+      saved_state(saved_state)
+  {
+  }
+
+protected:
+  const goto_symex_statet &saved_state;
+
+private:
+  /// \brief Resume symbolic execution from saved branch point
+  ///
+  /// This overrides the base implementation to call the symbolic executor with
+  /// the saved symex_target_equationt, symbol_tablet, and goto_symex_statet
+  /// provided as arguments to the constructor of this class.
+  void
+  perform_symbolic_execution(const goto_functionst &goto_functions) override;
+
+#define OPT_BMC                                                                \
+  "(program-only)"                                                             \
+  "(show-loops)"                                                               \
+  "(show-vcc)"                                                                 \
+  "(slice-formula)"                                                            \
+  "(unwinding-assertions)"                                                     \
+  "(no-unwinding-assertions)"                                                  \
+  "(no-pretty-names)"                                                          \
+  "(partial-loops)"                                                            \
+  "(paths)"                                                                    \
+  "(depth):"                                                                   \
+  "(unwind):"                                                                  \
+  "(unwindset):"                                                               \
+  "(graphml-witness):"                                                         \
+  "(unwindset):"
+
+#define HELP_BMC                                                               \
+  " --paths                      explore paths one at a time\n"                \
+  " --program-only               only show program expression\n"               \
+  " --show-loops                 show the loops in the program\n"              \
+  " --depth nr                   limit search depth\n"                         \
+  " --unwind nr                  unwind nr times\n"                            \
+  " --unwindset L:B,...          unwind loop L with a bound of B\n"            \
+  "                              (use --show-loops to get the loop IDs)\n"     \
+  " --show-vcc                   show the verification conditions\n"           \
+  " --slice-formula              remove assignments unrelated to property\n"   \
+  " --unwinding-assertions       generate unwinding assertions\n"              \
+  " --partial-loops              permit paths with partial loops\n"            \
+  " --no-pretty-names            do not simplify identifiers\n"                \
+  " --graphml-witness filename   write the witness in GraphML format to "      \
+  "filename\n" // NOLINT(*)
 };
 
 #endif // CPROVER_CBMC_BMC_H
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 1048b322a0f..0a6d7bee2d2 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -19,7 +19,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/string2int.h>
 #include <util/config.h>
 #include <util/unicode.h>
-#include <util/memory_info.h>
 #include <util/invariant.h>
 #include <util/exit_codes.h>
 
@@ -63,8 +62,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <langapi/mode.h>
 
-#include "cbmc_solvers.h"
-#include "bmc.h"
 #include "version.h"
 #include "xml_interface.h"
 
@@ -110,6 +107,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     exit(CPROVER_EXIT_USAGE_ERROR);
   }
 
+  if(cmdline.isset("paths"))
+    options.set_option("paths", true);
+
   if(cmdline.isset("program-only"))
     options.set_option("program-only", true);
 
@@ -373,13 +373,13 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
       }
       else
       {
-        assert(options.get_bool_option("smt2"));
+        PRECONDITION(options.get_bool_option("smt2"));
         options.set_option("z3", true), solver_set=true;
       }
     }
   }
   // Either have solver and standard version set, or neither.
-  assert(version_set==solver_set);
+  PRECONDITION(version_set == solver_set);
 
   if(cmdline.isset("beautify"))
     options.set_option("beautify", true);
@@ -542,36 +542,8 @@ int cbmc_parse_optionst::doit()
   if(set_properties())
     return CPROVER_EXIT_SET_PROPERTIES_FAILED;
 
-  // get solver
-  cbmc_solverst cbmc_solvers(
-    options,
-    goto_model.symbol_table,
-    get_message_handler());
-  cbmc_solvers.set_ui(ui_message_handler.get_ui());
-
-  std::unique_ptr<cbmc_solverst::solvert> cbmc_solver;
-
-  try
-  {
-    cbmc_solver=cbmc_solvers.get_solver();
-  }
-
-  catch(const char *error_msg)
-  {
-    error() << error_msg << eom;
-    return CPROVER_EXIT_EXCEPTION;
-  }
-
-  prop_convt &prop_conv=cbmc_solver->prop_conv();
-
-  bmct bmc(
-    options,
-    goto_model.symbol_table,
-    get_message_handler(),
-    prop_conv);
-
-  // do actual BMC
-  return do_bmc(bmc);
+  return bmct::do_language_agnostic_bmc(
+    options, goto_model, ui_message_handler.get_ui(), *this);
 }
 
 bool cbmc_parse_optionst::set_properties()
@@ -871,35 +843,6 @@ bool cbmc_parse_optionst::process_goto_program(
   return false;
 }
 
-/// invoke main modules
-int cbmc_parse_optionst::do_bmc(bmct &bmc)
-{
-  bmc.set_ui(ui_message_handler.get_ui());
-
-  int result = CPROVER_EXIT_INTERNAL_ERROR;
-
-  // do actual BMC
-  switch(bmc.run(goto_model.goto_functions))
-  {
-    case safety_checkert::resultt::SAFE:
-      result = CPROVER_EXIT_VERIFICATION_SAFE;
-      break;
-    case safety_checkert::resultt::UNSAFE:
-      result = CPROVER_EXIT_VERIFICATION_UNSAFE;
-      break;
-    case safety_checkert::resultt::ERROR:
-      result = CPROVER_EXIT_INTERNAL_ERROR;
-      break;
-  }
-
-  // let's log some more statistics
-  debug() << "Memory consumption:" << messaget::endl;
-  memory_info(debug());
-  debug() << eom;
-
-  return result;
-}
-
 /// display command line help
 void cbmc_parse_optionst::help()
 {
@@ -989,18 +932,7 @@ void cbmc_parse_optionst::help()
     " --nondet-static              add nondeterministic initialization of variables with static lifetime\n"
     "\n"
     "BMC options:\n"
-    " --program-only               only show program expression\n"
-    " --show-loops                 show the loops in the program\n"
-    " --depth nr                   limit search depth\n"
-    " --unwind nr                  unwind nr times\n"
-    " --unwindset L:B,...          unwind loop L with a bound of B\n"
-    "                              (use --show-loops to get the loop IDs)\n"
-    " --show-vcc                   show the verification conditions\n"
-    " --slice-formula              remove assignments unrelated to property\n"
-    " --unwinding-assertions       generate unwinding assertions\n"
-    " --partial-loops              permit paths with partial loops\n"
-    " --no-pretty-names            do not simplify identifiers\n"
-    " --graphml-witness filename   write the witness in GraphML format to filename\n" // NOLINT(*)
+    HELP_BMC
     "\n"
     "Backend options:\n"
     " --object-bits n              number of bits used for object addresses\n"
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
index c5fe31e6b88..4d5cc8ed943 100644
--- a/src/cbmc/cbmc_parse_options.h
+++ b/src/cbmc/cbmc_parse_options.h
@@ -22,7 +22,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <goto-programs/goto_trace.h>
 
+#include "bmc.h"
 #include "xml_interface.h"
+#include "cbmc_solvers.h"
 
 class bmct;
 class goto_functionst;
@@ -30,21 +32,21 @@ class optionst;
 
 // clang-format off
 #define CBMC_OPTIONS \
-  "(program-only)(preprocess)(slice-by-trace):" \
+  OPT_BMC \
+  "(preprocess)(slice-by-trace):" \
   OPT_FUNCTIONS \
-  "(no-simplify)(unwind):(unwindset):(slice-formula)(full-slice)" \
+  "(no-simplify)(full-slice)" \
   "(debug-level):(no-propagation)(no-simplify-if)" \
   "(document-subgoals)(outfile):(test-preprocessor)" \
   "D:I:(c89)(c99)(c11)(cpp98)(cpp03)(cpp11)" \
   "(object-bits):" \
-  "(depth):(partial-loops)(no-unwinding-assertions)(unwinding-assertions)" \
   OPT_GOTO_CHECK \
   "(no-assertions)(no-assumptions)" \
   "(no-built-in-assertions)" \
   "(xml-ui)(xml-interface)(json-ui)" \
   "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(opensmt)(mathsat)" \
   "(no-sat-preprocessor)" \
-  "(no-pretty-names)(beautify)" \
+  "(beautify)" \
   "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\
   "(refine-strings)" \
   "(string-printable)" \
@@ -54,8 +56,7 @@ class optionst;
   "(little-endian)(big-endian)" \
   OPT_SHOW_GOTO_FUNCTIONS \
   OPT_SHOW_PROPERTIES \
-  "(show-loops)" \
-  "(show-symbol-table)(show-parse-tree)(show-vcc)" \
+  "(show-symbol-table)(show-parse-tree)" \
   "(drop-unused-functions)" \
   "(property):(stop-on-fail)(trace)" \
   "(error-label):(verbosity):(no-library)" \
@@ -69,7 +70,6 @@ class optionst;
   "(arrays-uf-always)(arrays-uf-never)" \
   "(string-abstraction)(no-arch)(arch):" \
   "(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
-  "(graphml-witness):" \
   "(localize-faults)(localize-faults-method):" \
   OPT_GOTO_TRACE \
   "(claim):(show-claims)(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
@@ -101,7 +101,6 @@ class cbmc_parse_optionst:
   int get_goto_program(const optionst &);
   bool process_goto_program(const optionst &);
   bool set_properties();
-  int do_bmc(bmct &);
 };
 
 #endif // CPROVER_CBMC_CBMC_PARSE_OPTIONS_H
diff --git a/src/cbmc/symex_bmc.cpp b/src/cbmc/symex_bmc.cpp
index 45615063cc9..1bbd5af77e0 100644
--- a/src/cbmc/symex_bmc.cpp
+++ b/src/cbmc/symex_bmc.cpp
@@ -11,6 +11,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "symex_bmc.h"
 
+#include <goto-symex/symex_target_equation.h>
+
 #include <limits>
 
 #include <util/source_location.h>
@@ -18,14 +20,14 @@ Author: Daniel Kroening, kroening@kroening.com
 
 symex_bmct::symex_bmct(
   message_handlert &mh,
-  const namespacet &_ns,
-  symbol_tablet &_new_symbol_table,
-  symex_targett &_target)
-  : goto_symext(mh, _ns, _new_symbol_table, _target),
+  const symbol_tablet &outer_symbol_table,
+  symex_target_equationt &_target,
+  goto_symext::branch_worklistt &branch_worklist)
+  : goto_symext(mh, outer_symbol_table, _target, branch_worklist),
     record_coverage(false),
     max_unwind(0),
     max_unwind_is_set(false),
-    symex_coverage(_ns)
+    symex_coverage(ns)
 {
 }
 
diff --git a/src/cbmc/symex_bmc.h b/src/cbmc/symex_bmc.h
index 02f9ba6a561..65cd85880c8 100644
--- a/src/cbmc/symex_bmc.h
+++ b/src/cbmc/symex_bmc.h
@@ -24,9 +24,9 @@ class symex_bmct: public goto_symext
 public:
   symex_bmct(
     message_handlert &mh,
-    const namespacet &_ns,
-    symbol_tablet &_new_symbol_table,
-    symex_targett &_target);
+    const symbol_tablet &outer_symbol_table,
+    symex_target_equationt &_target,
+    goto_symext::branch_worklistt &branch_worklist);
 
   // To show progress
   source_locationt last_source_location;
diff --git a/src/goto-instrument/accelerate/scratch_program.cpp b/src/goto-instrument/accelerate/scratch_program.cpp
index 2e2faea34b4..6774f255c05 100644
--- a/src/goto-instrument/accelerate/scratch_program.cpp
+++ b/src/goto-instrument/accelerate/scratch_program.cpp
@@ -39,7 +39,7 @@ bool scratch_programt::check_sat(bool do_slice)
   symex.constant_propagation=constant_propagation;
   goto_symex_statet::propagationt::valuest constants;
 
-  symex.symex_with_state(symex_state, functions, *this);
+  symex.symex_with_state(symex_state, functions, symex_symbol_table);
 
   if(do_slice)
   {
diff --git a/src/goto-instrument/accelerate/scratch_program.h b/src/goto-instrument/accelerate/scratch_program.h
index 86a0323d139..0bd76634bd0 100644
--- a/src/goto-instrument/accelerate/scratch_program.h
+++ b/src/goto-instrument/accelerate/scratch_program.h
@@ -38,9 +38,11 @@ class scratch_programt:public goto_programt
   scratch_programt(symbol_tablet &_symbol_table, message_handlert &mh)
     : constant_propagation(true),
       symbol_table(_symbol_table),
-      ns(symbol_table),
-      equation(ns),
-      symex(mh, ns, symbol_table, equation),
+      symex_symbol_table(),
+      ns(symbol_table, symex_symbol_table),
+      equation(),
+      branch_worklist(),
+      symex(mh, symbol_table, equation, branch_worklist),
       satcheck(util_make_unique<satcheckt>()),
       satchecker(ns, *satcheck),
       z3(ns, "accelerate", "", "", smt2_dect::solvert::Z3),
@@ -73,8 +75,10 @@ class scratch_programt:public goto_programt
   goto_symex_statet symex_state;
   goto_functionst functions;
   symbol_tablet &symbol_table;
-  const namespacet ns;
+  symbol_tablet symex_symbol_table;
+  namespacet ns;
   symex_target_equationt equation;
+  goto_symext::branch_worklistt branch_worklist;
   goto_symext symex;
 
   std::unique_ptr<propt> satcheck;
diff --git a/src/goto-programs/safety_checker.h b/src/goto-programs/safety_checker.h
index bb1492d6f53..599669f4cce 100644
--- a/src/goto-programs/safety_checker.h
+++ b/src/goto-programs/safety_checker.h
@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 // this is just an interface -- it won't actually do any checking!
 
+#include <util/invariant.h>
 #include <util/message.h>
 
 #include "goto_trace.h"
@@ -45,4 +46,39 @@ class safety_checkert:public messaget
   const namespacet &ns;
 };
 
+/// \brief The worst of two results
+inline safety_checkert::resultt &
+operator&=(safety_checkert::resultt &a, safety_checkert::resultt const &b)
+{
+  switch(a)
+  {
+  case safety_checkert::resultt::ERROR:
+    return a;
+  case safety_checkert::resultt::SAFE:
+    a = b;
+    return a;
+  case safety_checkert::resultt::UNSAFE:
+    a = b == safety_checkert::resultt::ERROR ? b : a;
+    return a;
+  }
+  UNREACHABLE;
+}
+
+/// \brief The best of two results
+inline safety_checkert::resultt &
+operator|=(safety_checkert::resultt &a, safety_checkert::resultt const &b)
+{
+  switch(a)
+  {
+  case safety_checkert::resultt::SAFE:
+    return a;
+  case safety_checkert::resultt::ERROR:
+    a = b;
+    return a;
+  case safety_checkert::resultt::UNSAFE:
+    a = b == safety_checkert::resultt::SAFE ? b : a;
+    return a;
+  }
+  UNREACHABLE;
+}
 #endif // CPROVER_GOTO_PROGRAMS_SAFETY_CHECKER_H
diff --git a/src/goto-symex/auto_objects.cpp b/src/goto-symex/auto_objects.cpp
index b41a3e01c74..f411130474c 100644
--- a/src/goto-symex/auto_objects.cpp
+++ b/src/goto-symex/auto_objects.cpp
@@ -16,7 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/symbol_table.h>
 #include <util/std_expr.h>
 
-exprt goto_symext::make_auto_object(const typet &type)
+exprt goto_symext::make_auto_object(const typet &type, statet &state)
 {
   dynamic_counter++;
 
@@ -29,7 +29,7 @@ exprt goto_symext::make_auto_object(const typet &type)
   symbol.type=type;
   symbol.mode=ID_C;
 
-  new_symbol_table.add(symbol);
+  state.symbol_table.add(symbol);
 
   return symbol_exprt(symbol.name, symbol.type);
 }
@@ -67,8 +67,7 @@ void goto_symext::initialize_auto_object(
       // could be NULL nondeterministically
 
       address_of_exprt address_of_expr(
-        make_auto_object(type.subtype()),
-        pointer_type);
+        make_auto_object(type.subtype(), state), pointer_type);
 
       if_exprt rhs(
         side_effect_expr_nondett(bool_typet()),
diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
index 385c10905cf..f27a1f1ffac 100644
--- a/src/goto-symex/goto_symex.h
+++ b/src/goto-symex/goto_symex.h
@@ -19,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/goto_functions.h>
 
 #include "goto_symex_state.h"
+#include "symex_target_equation.h"
 
 class typet;
 class code_typet;
@@ -34,28 +35,53 @@ class symbol_exprt;
 class member_exprt;
 class namespacet;
 class side_effect_exprt;
-class symex_targett;
 class typecast_exprt;
 
 /// \brief The main class for the forward symbolic simulator
+///
+/// Higher-level architectural information on symbolic execution is
+/// documented in the \ref symex-overview
+/// "Symbolic execution module page".
 class goto_symext
 {
 public:
+  typedef goto_symex_statet statet;
+
+  /// \brief Information saved at a conditional goto to resume execution
+  struct branch_pointt
+  {
+    symex_target_equationt equation;
+    statet state;
+
+    explicit branch_pointt(const symex_target_equationt &e, const statet &s)
+      : equation(e), state(s, &equation)
+    {
+    }
+
+    explicit branch_pointt(const branch_pointt &other)
+      : equation(other.equation), state(other.state, &equation)
+    {
+    }
+  };
+
+  typedef std::list<branch_pointt> branch_worklistt;
+
   goto_symext(
     message_handlert &mh,
-    const namespacet &_ns,
-    symbol_tablet &_new_symbol_table,
-    symex_targett &_target)
+    const symbol_tablet &outer_symbol_table,
+    symex_target_equationt &_target,
+    branch_worklistt &branch_worklist)
     : total_vccs(0),
       remaining_vccs(0),
       constant_propagation(true),
-      new_symbol_table(_new_symbol_table),
       language_mode(),
-      ns(_ns),
+      outer_symbol_table(outer_symbol_table),
+      ns(outer_symbol_table),
       target(_target),
       atomic_section_counter(0),
       log(mh),
-      guard_identifier("goto_symex::\\guard")
+      guard_identifier("goto_symex::\\guard"),
+      branch_worklist(branch_worklist)
   {
     options.set_option("simplify", true);
     options.set_option("assertions", true);
@@ -65,8 +91,6 @@ class goto_symext
   {
   }
 
-  typedef goto_symex_statet statet;
-
   typedef
     std::function<const goto_functionst::goto_functiont &(const irep_idt &)>
     get_goto_functiont;
@@ -78,7 +102,18 @@ class goto_symext
   /// has completed, so use it if you don't care about having the state
   /// around afterwards.
   virtual void symex_from_entry_point_of(
-    const goto_functionst &goto_functions);
+    const goto_functionst &goto_functions,
+    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
+  /// counter of the saved state.
+  virtual void resume_symex_from_saved_state(
+    const goto_functionst &goto_functions,
+    const statet &saved_state,
+    symex_target_equationt *const saved_equation,
+    symbol_tablet &new_symbol_table);
 
   /// \brief symex entire program starting from entry point
   ///
@@ -87,7 +122,8 @@ class goto_symext
   /// has completed, so use it if you don't care about having the state
   /// around afterwards.
   virtual void symex_from_entry_point_of(
-    const get_goto_functiont &get_goto_function);
+    const get_goto_functiont &get_goto_function,
+    symbol_tablet &new_symbol_table);
 
   //// \brief symex entire program starting from entry point
   ///
@@ -99,7 +135,7 @@ class goto_symext
   virtual void symex_with_state(
     statet &,
     const goto_functionst &,
-    const goto_programt &);
+    symbol_tablet &);
 
   //// \brief symex entire program starting from entry point
   ///
@@ -111,7 +147,7 @@ class goto_symext
   virtual void symex_with_state(
     statet &,
     const get_goto_functiont &,
-    const goto_programt &);
+    symbol_tablet &);
 
   /// Symexes from the first instruction and the given state, terminating as
   /// soon as the last instruction is reached.  This is useful to explicitly
@@ -162,7 +198,6 @@ class goto_symext
   void symex_threaded_step(
     statet &, const get_goto_functiont &);
 
-  /** execute just one step */
   virtual void symex_step(
     const get_goto_functiont &,
     statet &);
@@ -177,22 +212,35 @@ class goto_symext
   bool constant_propagation;
 
   optionst options;
-  symbol_tablet &new_symbol_table;
 
   /// language_mode: ID_java, ID_C or another language identifier
   /// if we know the source language in use, irep_idt() otherwise.
   irep_idt language_mode;
 
 protected:
-  const namespacet &ns;
-  symex_targett &target;
+  /// The symbol table associated with the goto-program that we're
+  /// executing. This symbol table will not additionally contain objects
+  /// that are dynamically created as part of symbolic execution; the
+  /// names of those object are stored in the symbol table passed as the
+  /// `new_symbol_table` argument to the `symex_*` methods.
+  const symbol_tablet &outer_symbol_table;
+
+  /// Initialized just before symbolic execution begins, to point to
+  /// both `outer_symbol_table` and the symbol table owned by the
+  /// `goto_symex_statet` object used during symbolic execution. That
+  /// symbol table must be owned by goto_symex_statet rather than passed
+  /// in, in case the state is saved and resumed. This namespacet is
+  /// used during symbolic execution to look up names from the original
+  /// goto-program, and the names of dynamically-created objects.
+  namespacet ns;
+  symex_target_equationt &target;
   unsigned atomic_section_counter;
 
   mutable messaget log;
 
   friend class symex_dereference_statet;
 
-  void new_name(symbolt &symbol);
+  void new_name(symbolt &symbol, statet &state);
 
   // this does the following:
   // a) rename non-det choices
@@ -206,7 +254,7 @@ class goto_symext
   void initialize_auto_object(const exprt &, statet &);
   void process_array_expr(exprt &);
   void process_array_expr_rec(exprt &, const typet &) const;
-  exprt make_auto_object(const typet &);
+  exprt make_auto_object(const typet &, statet &);
   virtual void dereference(exprt &, statet &, const bool write);
 
   void dereference_rec(
@@ -415,6 +463,8 @@ class goto_symext
   void read(exprt &);
   void replace_nondet(exprt &);
   void rewrite_quantifiers(exprt &, statet &);
+
+  branch_worklistt &branch_worklist;
 };
 
 #endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_H
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index f2db40c8b71..f1c1e325e46 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/src/goto-symex/goto_symex_state.cpp
@@ -12,21 +12,21 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "goto_symex_state.h"
 
 #include <cstdlib>
-#include <cassert>
 #include <iostream>
 
+#include <util/invariant.h>
 #include <util/base_exceptions.h>
 #include <util/std_expr.h>
 #include <util/prefix.h>
 
 #include <analyses/dirty.h>
 
-goto_symex_statet::goto_symex_statet():
-  depth(0),
-  symex_target(nullptr),
-  atomic_section_id(0),
-  record_events(true),
-  dirty(nullptr)
+goto_symex_statet::goto_symex_statet()
+  : depth(0),
+    symex_target(nullptr),
+    atomic_section_id(0),
+    record_events(true),
+    dirty()
 {
   threads.resize(1);
   new_frame();
@@ -326,7 +326,7 @@ void goto_symex_statet::assignment(
   assert_l1_renaming(lhs);
 
   #if 0
-  assert(l1_identifier != get_original_name(l1_identifier)
+  PRECONDITION(l1_identifier != get_original_name(l1_identifier)
       || l1_identifier=="goto_symex::\\guard"
       || ns.lookup(l1_identifier).is_shared()
       || has_prefix(id2string(l1_identifier), "symex::invalid_object")
@@ -493,9 +493,12 @@ void goto_symex_statet::rename(
   }
   else if(expr.id()==ID_address_of)
   {
-    assert(expr.operands().size()==1);
+    DATA_INVARIANT(
+      expr.operands().size() == 1, "address_of should have a single operand");
     rename_address(expr.op0(), ns, level);
-    assert(expr.type().id()==ID_pointer);
+    DATA_INVARIANT(
+      expr.type().id() == ID_pointer,
+      "type of address_of should be ID_pointer");
     expr.type().subtype()=expr.op0().type();
   }
   else
@@ -512,8 +515,11 @@ void goto_symex_statet::rename(
       expr.type()=to_with_expr(expr).old().type();
     else if(expr.id()==ID_if)
     {
-      assert(to_if_expr(expr).true_case().type()==
-             to_if_expr(expr).false_case().type());
+      DATA_INVARIANT(
+        to_if_expr(expr).true_case().type() ==
+          to_if_expr(expr).false_case().type(),
+        "true case of to_if_expr should be of same type "
+        "as false case");
       expr.type()=to_if_expr(expr).true_case().type();
     }
   }
@@ -529,11 +535,10 @@ bool goto_symex_statet::l2_thread_read_encoding(
     return false;
 
   // is it a shared object?
-  INVARIANT_STRUCTURED(dirty!=nullptr, nullptr_exceptiont, "dirty is null");
   const irep_idt &obj_identifier=expr.get_object_name();
-  if(obj_identifier=="goto_symex::\\guard" ||
-     (!ns.lookup(obj_identifier).is_shared() &&
-      !(*dirty)(obj_identifier)))
+  if(
+    obj_identifier == "goto_symex::\\guard" ||
+    (!ns.lookup(obj_identifier).is_shared() && !(dirty)(obj_identifier)))
     return false;
 
   ssa_exprt ssa_l1=expr;
@@ -674,11 +679,10 @@ bool goto_symex_statet::l2_thread_write_encoding(
     return false;
 
   // is it a shared object?
-  INVARIANT_STRUCTURED(dirty!=nullptr, nullptr_exceptiont, "dirty is null");
   const irep_idt &obj_identifier=expr.get_object_name();
-  if(obj_identifier=="goto_symex::\\guard" ||
-     (!ns.lookup(obj_identifier).is_shared() &&
-      !(*dirty)(obj_identifier)))
+  if(
+    obj_identifier == "goto_symex::\\guard" ||
+    (!ns.lookup(obj_identifier).is_shared() && !(dirty)(obj_identifier)))
     return false; // not shared
 
   // see whether we are within an atomic section
@@ -730,7 +734,7 @@ void goto_symex_statet::rename_address(
       index_exprt &index_expr=to_index_expr(expr);
 
       rename_address(index_expr.array(), ns, level);
-      assert(index_expr.array().type().id()==ID_array);
+      PRECONDITION(index_expr.array().type().id() == ID_array);
       expr.type()=index_expr.array().type().subtype();
 
       // the index is not an address
@@ -760,7 +764,7 @@ void goto_symex_statet::rename_address(
           to_struct_union_type(member_expr.struct_op().type());
         const struct_union_typet::componentt &comp=
           su_type.get_component(member_expr.get_component_name());
-        assert(comp.is_not_nil());
+        PRECONDITION(comp.is_not_nil());
         expr.type()=comp.type();
       }
       else
@@ -904,8 +908,8 @@ void goto_symex_statet::get_l1_name(exprt &expr) const
 
 void goto_symex_statet::switch_to_thread(unsigned t)
 {
-  assert(source.thread_nr<threads.size());
-  assert(t<threads.size());
+  PRECONDITION(source.thread_nr < threads.size());
+  PRECONDITION(t < threads.size());
 
   // save PC
   threads[source.thread_nr].pc=source.pc;
diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h
index bbbc9b64d92..fd8e80ed2fd 100644
--- a/src/goto-symex/goto_symex_state.h
+++ b/src/goto-symex/goto_symex_state.h
@@ -12,10 +12,12 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_GOTO_SYMEX_GOTO_SYMEX_STATE_H
 #define CPROVER_GOTO_SYMEX_GOTO_SYMEX_STATE_H
 
-#include <cassert>
 #include <memory>
 #include <unordered_set>
 
+#include <analyses/dirty.h>
+
+#include <util/invariant.h>
 #include <util/guard.h>
 #include <util/std_expr.h>
 #include <util/ssa_expr.h>
@@ -24,9 +26,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <pointer-analysis/value_set.h>
 #include <goto-programs/goto_functions.h>
 
-#include "symex_target.h"
-
-class incremental_dirtyt;
+#include "symex_target_equation.h"
 
 // central data structure: state
 class goto_symex_statet final
@@ -35,12 +35,26 @@ class goto_symex_statet final
   goto_symex_statet();
   ~goto_symex_statet();
 
-  // distance from entry
+  /// \brief Fake "copy constructor" that initializes the `symex_target` member
+  explicit goto_symex_statet(
+    const goto_symex_statet &other,
+    symex_target_equationt *const target)
+    : goto_symex_statet(other) // NOLINT
+  {
+    symex_target = target;
+  }
+
+  /// contains symbols that are minted during symbolic execution, such as
+  /// dynamically created objects etc. The names in this table are needed
+  /// for error traces even after symbolic execution has finished.
+  symbol_tablet symbol_table;
+
+  /// distance from entry
   unsigned depth;
 
   guardt guard;
   symex_targett::sourcet source;
-  symex_targett *symex_target;
+  symex_target_equationt *symex_target;
 
   // we have a two-level renaming
 
@@ -66,7 +80,7 @@ class goto_symex_statet final
 
     void increase_counter(const irep_idt &identifier)
     {
-      assert(current_names.find(identifier)!=current_names.end());
+      PRECONDITION(current_names.find(identifier) != current_names.end());
       ++current_names[identifier].second;
     }
 
@@ -113,7 +127,7 @@ class goto_symex_statet final
           current_names.insert(it, *ito);
         else if(it!=current_names.end())
         {
-          assert(it->first==ito->first);
+          PRECONDITION(it->first == ito->first);
           it->second=ito->second;
           ++it;
         }
@@ -227,6 +241,17 @@ class goto_symex_statet final
     }
   };
 
+  explicit goto_symex_statet(const goto_statet &s)
+    : depth(s.depth),
+      guard(s.guard),
+      source(s.source),
+      propagation(s.propagation),
+      value_set(s.value_set),
+      atomic_section_id(s.atomic_section_id)
+  {
+    level2.current_names = s.level2_current_names;
+  }
+
   // gotos
   typedef std::list<goto_statet> goto_state_listt;
   typedef std::map<goto_programt::const_targett, goto_state_listt>
@@ -282,25 +307,25 @@ class goto_symex_statet final
 
   call_stackt &call_stack()
   {
-    assert(source.thread_nr<threads.size());
+    PRECONDITION(source.thread_nr < threads.size());
     return threads[source.thread_nr].call_stack;
   }
 
   const call_stackt &call_stack() const
   {
-    assert(source.thread_nr<threads.size());
+    PRECONDITION(source.thread_nr < threads.size());
     return threads[source.thread_nr].call_stack;
   }
 
   framet &top()
   {
-    assert(!call_stack().empty());
+    PRECONDITION(!call_stack().empty());
     return call_stack().back();
   }
 
   const framet &top() const
   {
-    assert(!call_stack().empty());
+    PRECONDITION(!call_stack().empty());
     return call_stack().back();
   }
 
@@ -345,7 +370,24 @@ class goto_symex_statet final
 
   void switch_to_thread(unsigned t);
   bool record_events;
-  std::unique_ptr<incremental_dirtyt> dirty;
+  incremental_dirtyt dirty;
+
+  goto_programt::const_targett saved_target;
+  bool has_saved_target;
+  bool saved_target_is_backwards;
+
+private:
+  /// \brief Dangerous, do not use
+  ///
+  /// Copying a state S1 to S2 risks S2 pointing to a deallocated
+  /// symex_target_equationt if S1 (and the symex_target_equationt that its
+  /// `symex_target` member points to) go out of scope. If your class has a
+  /// goto_symex_statet member and needs a copy constructor, copy instances
+  /// of this class using the public two-argument copy constructor
+  /// constructor to ensure that the copy points to an allocated
+  /// symex_target_equationt. The two-argument copy constructor uses this
+  /// private copy constructor as a delegate.
+  goto_symex_statet(const goto_symex_statet &other) = default;
 };
 
 #endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_STATE_H
diff --git a/src/goto-symex/module.md b/src/goto-symex/module.md
index 6c8321ce33e..c062c1d8f3f 100644
--- a/src/goto-symex/module.md
+++ b/src/goto-symex/module.md
@@ -3,6 +3,10 @@
 
 \author Kareem Khazem
 
+\section symbolic-execution Symbolic Execution
+
+In the \ref goto-symex directory.
+
 **Key classes:**
 * goto_symex_statet
 * goto_symext
@@ -19,6 +23,115 @@ digraph G {
 }
 \enddot
 
+\subsection symex-overview Overview
+
+The \ref bmct class gets a reference to an \ref symex_target_equationt
+"equation" (initially, an empty list of \ref symex_target_equationt::SSA_stept
+"single-static assignment steps") and a goto-program from the frontend.
+The \ref bmct creates a goto_symext to symbolically execute the
+goto-program, thereby filling the equation, which can then be passed
+along to the SAT solver.
+
+The symbolic execution state is maintained by goto_symex_statet. This is
+a memory-heavy data structure, so goto_symext creates it on-demand and
+lets it go out-of-scope as soon as possible. However, the process of
+symbolic execution fills out an additional \ref symbol_tablet
+"symbol table" of dynamically-created objects; this symbol table is
+needed when solving the equation. This symbol table must thus be
+exported out of the state before it is torn down; this is done through
+the parameter "`new_symbol_table`" passed as a reference to the various
+functions in goto_symext.
+
+The main symbolic execution loop code is goto_symext::symex_step(). This
+function case-switches over the type of the instruction that we're
+currently executing, and calls various other functions appropriate to
+the instruction type, i.e. goto_symext::symex_function_call() if the
+current instruction is a function call, goto_symext::symex_goto() if the
+current instruction is a goto, etc.
+
+\subsection symex-path Path exploration
+
+By default, CBMC symbolically executes the entire program, building up
+an equation representing all instructions, which it then passes to the
+solver. Notably, it _merges_ paths that diverge due to a goto
+instruction, forming a constraint that represents having taken either of
+the two paths; the code for doing this is goto_symext::merge_goto().
+
+CBMC can operate in a different mode when the `--paths` flag is passed
+on the command line. This disables path merging; instead, CBMC executes
+a single path at a time, calling the solver with the equation
+representing that path, then continues to execute other paths.
+The 'other paths' that would have been taken when the program branches
+are saved onto a workqueue so that CBMC can continue to execute the
+current path, and then later retrieve saved paths from the workqueue.
+Implementation-wise, \ref bmct passes a worklist to goto_symext in
+bmct::do_language_agnostic_bmc(). If path exploration is enabled,
+goto_symext will fill up the worklist whenever it encounters a branch,
+instead of merging the paths on the branch.  After the initial symbolic
+execution (i.e. the first call to bmct::run() in
+bmct::do_language_agnostic_bmc()), \ref bmct continues popping the
+worklist and executing untaken paths until the worklist empties. Note
+that this means that the default model-checking behaviour is a special
+case of path exploration: when model-checking, the initial symbolic
+execution run does not add any paths to the workqueue but rather merges
+all the paths together, so the additional path-exploration loop is
+skipped over.
+
+\subsection ssa-renaming SSA renaming levels
+
+In goto-programs, variable names get a prefix to indicate their scope
+(like `main::1::%foo` or whatever). At symbolic execution level, variables
+also get a _suffix_ because we’re doing single-static assignment. There
+are three “levels” of renaming. At Level 2, variables are renamed every
+time they are encountered in a function. At Level 1, variables are
+renamed every time the functions that contain those variables are
+called. At Level 0, variables are renamed every time a new thread
+containing those variables are spawned. We can inspect the renamed
+variable names with the –show-vcc flag, which prints a string with the
+following format: `%%s!%%d@%%d#%%d`. The string field is the variable name,
+and the numbers after the !, @, and # are the L0, L1, and L2 suffixes
+respectively. The following examples illustrate Level 1 and 2 renaming:
+
+    $ cat l1.c
+    int main() {
+      int x=7;
+      x=8;
+      assert(0);
+    }
+    $ cbmc --show-vcc l1.c
+    ...
+    {-12} x!0@1#2 == 7
+    {-13} x!0@1#3 == 8
+
+That is, the L0 names for both xs are 0; the L1 names for both xs are 1;
+but each occurrence of x within main() gets a fresh L2 suffix (2 and 3,
+respectively).
+
+    $ cat l2.c
+    void foo(){
+      int x=7;
+      x=8;
+      x=9;
+    }
+    int main(){
+      foo();
+      foo();
+      assert(0);
+    }
+    $ cbmc --show-vcc l2.c
+    ...
+    {-12} x!0@1#2 == 7
+    {-13} x!0@1#3 == 8
+    {-14} x!0@1#4 == 9
+    {-15} x!0@2#2 == 7
+    {-16} x!0@2#3 == 8
+    {-17} x!0@2#4 == 9
+
+That is, every time we enter function foo, the L1 counter of x is
+incremented (from 1 to 2) and the L0 counter is reset (back to 2, after
+having been incremented up to 4). The L0 counter then increases every
+time we access x as we walk through the function.
+
 ---
 \section counter-example-production Counter Example Production
 
diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp
index cbf9f822d1c..65e6c9cd4f7 100644
--- a/src/goto-symex/symex_builtin_functions.cpp
+++ b/src/goto-symex/symex_builtin_functions.cpp
@@ -11,8 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "goto_symex.h"
 
-#include <cassert>
-
 #include <util/expr_util.h>
 #include <util/message.h>
 #include <util/arith_tools.h>
@@ -103,10 +101,10 @@ void goto_symext::symex_allocate(
           if(s.is_constant())
           {
             s=tmp_size.op1();
-            assert(c_sizeof_type_rec(tmp_size.op0())==tmp_type);
+            PRECONDITION(c_sizeof_type_rec(tmp_size.op0()) == tmp_type);
           }
           else
-            assert(c_sizeof_type_rec(tmp_size.op1())==tmp_type);
+            PRECONDITION(c_sizeof_type_rec(tmp_size.op1()) == tmp_type);
 
           object_type=array_typet(tmp_type, s);
         }
@@ -146,7 +144,7 @@ void goto_symext::symex_allocate(
       size_symbol.type=tmp_size.type();
       size_symbol.mode=ID_C;
 
-      new_symbol_table.add(size_symbol);
+      state.symbol_table.add(size_symbol);
 
       code_assignt assignment(size_symbol.symbol_expr(), size);
       size=assignment.lhs();
@@ -165,7 +163,7 @@ void goto_symext::symex_allocate(
   value_symbol.type.set("#dynamic", true);
   value_symbol.mode=ID_C;
 
-  new_symbol_table.add(value_symbol);
+  state.symbol_table.add(value_symbol);
 
   exprt zero_init=code.op1();
   state.rename(zero_init, ns); // to allow constant propagation
@@ -283,15 +281,15 @@ irep_idt get_string_argument_rec(const exprt &src)
 {
   if(src.id()==ID_typecast)
   {
-    assert(src.operands().size()==1);
+    PRECONDITION(src.operands().size() == 1);
     return get_string_argument_rec(src.op0());
   }
   else if(src.id()==ID_address_of)
   {
-    assert(src.operands().size()==1);
+    PRECONDITION(src.operands().size() == 1);
     if(src.op0().id()==ID_index)
     {
-      assert(src.op0().operands().size()==2);
+      PRECONDITION(src.op0().operands().size() == 2);
 
       if(src.op0().op0().id()==ID_string_constant &&
          src.op0().op1().is_zero())
@@ -440,7 +438,7 @@ void goto_symext::symex_cpp_new(
 
   symbol.type.set("#dynamic", true);
 
-  new_symbol_table.add(symbol);
+  state.symbol_table.add(symbol);
 
   // make symbol expression
 
diff --git a/src/goto-symex/symex_decl.cpp b/src/goto-symex/symex_decl.cpp
index 3dbdc1e554c..e243c46a9fe 100644
--- a/src/goto-symex/symex_decl.cpp
+++ b/src/goto-symex/symex_decl.cpp
@@ -98,9 +98,7 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
       symex_targett::assignment_typet::HIDDEN:
       symex_targett::assignment_typet::STATE);
 
-  assert(state.dirty);
-  if((*state.dirty)(ssa.get_object_name()) &&
-     state.atomic_section_id==0)
+  if(state.dirty(ssa.get_object_name()) && state.atomic_section_id == 0)
     target.shared_write(
       state.guard.as_expr(),
       ssa,
diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp
index 4fd3b0176a2..a7648a2e896 100644
--- a/src/goto-symex/symex_dereference.cpp
+++ b/src/goto-symex/symex_dereference.cpp
@@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "goto_symex.h"
 
+#include <util/invariant.h>
 #include <util/pointer_offset_size.h>
 #include <util/arith_tools.h>
 #include <util/base_type.h>
@@ -200,7 +201,7 @@ exprt goto_symext::address_arithmetic(
        expr.get_bool(ID_C_SSA_symbol))
     {
       offset=compute_pointer_offset(expr, ns);
-      assert(offset>=0);
+      PRECONDITION(offset >= 0);
     }
 
     if(offset>0)
@@ -249,11 +250,7 @@ void goto_symext::dereference_rec(
     symex_dereference_statet symex_dereference_state(*this, state);
 
     value_set_dereferencet dereference(
-      ns,
-      new_symbol_table,
-      options,
-      symex_dereference_state,
-      language_mode);
+      ns, state.symbol_table, options, symex_dereference_state, language_mode);
 
     // std::cout << "**** " << from_expr(ns, "", tmp1) << '\n';
     exprt tmp2=
@@ -351,7 +348,7 @@ void goto_symext::dereference(
   // in order to distinguish addresses of local variables
   // from different frames. Would be enough to rename
   // symbols whose address is taken.
-  assert(!state.call_stack().empty());
+  PRECONDITION(!state.call_stack().empty());
   state.rename(expr, ns, goto_symex_statet::L1);
 
   // start the recursion!
diff --git a/src/goto-symex/symex_dereference_state.cpp b/src/goto-symex/symex_dereference_state.cpp
index 9911ba51e7d..d0e00b0ce7d 100644
--- a/src/goto-symex/symex_dereference_state.cpp
+++ b/src/goto-symex/symex_dereference_state.cpp
@@ -47,7 +47,7 @@ bool symex_dereference_statet::has_failed_symbol(
       symbol_exprt sym_expr=sym.symbol_expr();
       state.rename(sym_expr, ns, goto_symex_statet::L1);
       sym.name=to_ssa_expr(sym_expr).get_identifier();
-      goto_symex.new_symbol_table.move(sym, sym_ptr);
+      state.symbol_table.move(sym, sym_ptr);
       symbol=sym_ptr;
       return true;
     }
@@ -68,7 +68,7 @@ bool symex_dereference_statet::has_failed_symbol(
       symbol_exprt sym_expr=sym.symbol_expr();
       state.rename(sym_expr, ns, goto_symex_statet::L1);
       sym.name=to_ssa_expr(sym_expr).get_identifier();
-      goto_symex.new_symbol_table.move(sym, sym_ptr);
+      state.symbol_table.move(sym, sym_ptr);
       symbol=sym_ptr;
       return true;
     }
diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp
index 15daefbee4a..37e173928c4 100644
--- a/src/goto-symex/symex_function_call.cpp
+++ b/src/goto-symex/symex_function_call.cpp
@@ -12,9 +12,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "goto_symex.h"
 
 #include <sstream>
-#include <cassert>
 
 #include <util/cprover_prefix.h>
+#include <util/invariant.h>
 #include <util/prefix.h>
 #include <util/arith_tools.h>
 #include <util/base_type.h>
@@ -158,7 +158,7 @@ void goto_symext::parameter_assignments(
       symbol.base_name="va_arg"+std::to_string(va_count);
       symbol.type=it1->type();
 
-      new_symbol_table.insert(std::move(symbol));
+      state.symbol_table.insert(std::move(symbol));
 
       symbol_exprt lhs=symbol_exprt(id, it1->type());
 
@@ -228,8 +228,7 @@ void goto_symext::symex_function_call_code(
   const goto_functionst::goto_functiont &goto_function =
     get_goto_function(identifier);
 
-  if(state.dirty)
-    state.dirty->populate_dirty_for_function(identifier, goto_function);
+  state.dirty.populate_dirty_for_function(identifier, goto_function);
 
   const bool stop_recursing=get_unwind_recursion(
     identifier,
@@ -330,7 +329,6 @@ void goto_symext::pop_frame(statet &state)
     state.level1.restore_from(frame.old_level1);
 
     // clear function-locals from L2 renaming
-    PRECONDITION(state.dirty);
     for(goto_symex_statet::renaming_levelt::current_namest::iterator
         c_it=state.level2.current_names.begin();
         c_it!=state.level2.current_names.end();
@@ -338,9 +336,10 @@ void goto_symext::pop_frame(statet &state)
     {
       const irep_idt l1_o_id=c_it->second.first.get_l1_object_identifier();
       // could use iteration over local_objects as l1_o_id is prefix
-      if(frame.local_objects.find(l1_o_id)==frame.local_objects.end() ||
-         (state.threads.size()>1 &&
-          (*state.dirty)(c_it->second.first.get_object_name())))
+      if(
+        frame.local_objects.find(l1_o_id) == frame.local_objects.end() ||
+        (state.threads.size() > 1 &&
+         state.dirty(c_it->second.first.get_object_name())))
       {
         ++c_it;
         continue;
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
index d4875f27228..e25add14741 100644
--- a/src/goto-symex/symex_goto.cpp
+++ b/src/goto-symex/symex_goto.cpp
@@ -11,9 +11,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "goto_symex.h"
 
-#include <cassert>
 #include <algorithm>
 
+#include <util/invariant.h>
 #include <util/std_expr.h>
 
 #include <analyses/dirty.h>
@@ -43,7 +43,8 @@ void goto_symext::symex_goto(statet &state)
 
   target.goto_instruction(state.guard.as_expr(), new_guard, state.source);
 
-  assert(!instruction.targets.empty());
+  DATA_INVARIANT(
+    !instruction.targets.empty(), "goto should have at least one target");
 
   // we only do deterministic gotos for now
   if(instruction.targets.size()!=1)
@@ -99,6 +100,27 @@ void goto_symext::symex_goto(statet &state)
     }
   }
 
+  exprt simpl_state_guard = state.guard.as_expr();
+  do_simplify(simpl_state_guard);
+
+  // No point executing both branches of an unconditional goto.
+  if(
+    new_guard.is_true() && // We have an unconditional goto, AND
+    // either there are no blocks between us and the target in the
+    // surrounding scope
+    (simpl_state_guard.is_true() ||
+     // or there is another block, but we're doing path exploration so
+     // we're going to skip over it for now and return to it later.
+     options.get_bool_option("paths")))
+  {
+    DATA_INVARIANT(
+      instruction.targets.size() > 0,
+      "Instruction is an unconditional goto with no target: " +
+        instruction.code.pretty());
+    symex_transition(state, instruction.get_target(), true);
+    return;
+  }
+
   goto_programt::const_targett new_state_pc, state_pc;
   symex_targett::sourcet original_source=state.source;
 
@@ -126,12 +148,56 @@ void goto_symext::symex_goto(statet &state)
     state_pc=goto_target;
   }
 
+  // Normally the next instruction to execute would be state_pc and we save
+  // new_state_pc for later. But if we're executing from a saved state, then
+  // new_state_pc should be the state that we saved from earlier, so let's
+  // execute that instead.
+  if(state.has_saved_target)
+  {
+    INVARIANT(
+      new_state_pc == state.saved_target,
+      "Tried to explore the other path of a branch, but the next "
+      "instruction along that path is not the same as the instruction "
+      "that we saved at the branch point. Saved instruction is " +
+        state.saved_target->code.pretty() +
+        "\nwe were intending "
+        "to explore " +
+        new_state_pc->code.pretty() +
+        "\nthe "
+        "instruction we think we saw on a previous path exploration is " +
+        state_pc->code.pretty());
+    goto_programt::const_targett tmp = new_state_pc;
+    new_state_pc = state_pc;
+    state_pc = tmp;
+    log.debug() << "Resuming from '" << state_pc->code.source_location() << "'"
+                << log.eom;
+  }
+  else if(options.get_bool_option("paths"))
+  {
+    // At this point, `state_pc` is the instruction we should execute
+    // immediately, and `new_state_pc` is the instruction that we should execute
+    // later (after we've finished exploring this branch). For path-based
+    // exploration, save `new_state_pc` to the saved state that we will resume
+    // executing from, so that goto_symex::symex_goto() knows that we've already
+    // explored the branch starting from `state_pc` when it is later called at
+    // this branch.
+    branch_pointt branch_point(target, state);
+    branch_point.state.saved_target = new_state_pc;
+    branch_point.state.has_saved_target = true;
+    // `forward` tells us where the branch we're _currently_ executing is
+    // pointing to; this needs to be inverted for the branch that we're saving,
+    // so let its truth value for `backwards` be the same as ours for `forward`.
+    branch_point.state.saved_target_is_backwards = forward;
+    branch_worklist.push_back(branch_point);
+    log.debug() << "Saving '" << new_state_pc->source_location << "'"
+                << log.eom;
+  }
+
   // put into state-queue
   statet::goto_state_listt &goto_state_list=
     state.top().goto_state_map[new_state_pc];
 
   goto_state_list.push_back(statet::goto_statet(state));
-  statet::goto_statet &new_state=goto_state_list.back();
 
   symex_transition(state, state_pc, !forward);
 
@@ -175,17 +241,31 @@ void goto_symext::symex_goto(statet &state)
       state.rename(guard_expr, ns);
     }
 
-    if(forward)
+    if(state.has_saved_target)
     {
-      new_state.guard.add(guard_expr);
-      guard_expr.make_not();
-      state.guard.add(guard_expr);
+      if(forward)
+        state.guard.add(guard_expr);
+      else
+      {
+        guard_expr.make_not();
+        state.guard.add(guard_expr);
+      }
     }
     else
     {
-      state.guard.add(guard_expr);
-      guard_expr.make_not();
-      new_state.guard.add(guard_expr);
+      statet::goto_statet &new_state = goto_state_list.back();
+      if(forward)
+      {
+        new_state.guard.add(guard_expr);
+        guard_expr.make_not();
+        state.guard.add(guard_expr);
+      }
+      else
+      {
+        state.guard.add(guard_expr);
+        guard_expr.make_not();
+        new_state.guard.add(guard_expr);
+      }
     }
   }
 }
@@ -306,9 +386,9 @@ void goto_symext::phi_function(
     const symbolt &symbol=ns.lookup(obj_identifier);
 
     // shared?
-    if(dest_state.atomic_section_id==0 &&
-       dest_state.threads.size()>=2 &&
-       (symbol.is_shared() || (*dest_state.dirty)(symbol.name)))
+    if(
+      dest_state.atomic_section_id == 0 && dest_state.threads.size() >= 2 &&
+      (symbol.is_shared() || (dest_state.dirty)(symbol.name)))
       continue; // no phi nodes for shared stuff
 
     // don't merge (thread-)locals across different threads, which
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
index 1f0baf6dbe2..77d906d0770 100644
--- a/src/goto-symex/symex_main.cpp
+++ b/src/goto-symex/symex_main.cpp
@@ -46,10 +46,10 @@ void goto_symext::symex_transition(
   state.source.pc=to;
 }
 
-void goto_symext::new_name(symbolt &symbol)
+void goto_symext::new_name(symbolt &symbol, statet &state)
 {
   get_new_name(symbol, ns);
-  new_symbol_table.add(symbol);
+  state.symbol_table.add(symbol);
 }
 
 void goto_symext::vcc(
@@ -136,11 +136,10 @@ void goto_symext::initialize_entry_point(
   state.top().end_of_function=limit;
   state.top().calling_location.pc=state.top().end_of_function;
   state.symex_target=&target;
-  state.dirty=util_make_unique<incremental_dirtyt>();
 
   INVARIANT(
     !pc->function.empty(), "all symexed instructions should have a function");
-  state.dirty->populate_dirty_for_function(
+  state.dirty.populate_dirty_for_function(
     pc->function, get_goto_function(pc->function));
 
   symex_transition(state, state.source.pc);
@@ -176,29 +175,65 @@ static goto_symext::get_goto_functiont get_function_from_goto_functions(
 void goto_symext::symex_with_state(
   statet &state,
   const goto_functionst &goto_functions,
-  const goto_programt &goto_program)
+  symbol_tablet &new_symbol_table)
 {
   symex_with_state(
-    state, get_function_from_goto_functions(goto_functions), goto_program);
+    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,
-  const goto_programt &goto_program)
+  symbol_tablet &new_symbol_table)
 {
-  PRECONDITION(!goto_program.instructions.empty());
-  initialize_entry_point(
-    state,
-    get_goto_function,
-    goto_program.instructions.begin(),
-    prev(goto_program.instructions.end()));
+  // We'll be using ns during symbolic execution and it needs to know
+  // about the names minted in `state`, so make it point both to
+  // `state`'s symbol table and the symbol table of the original
+  // goto-program.
+  ns = namespacet(outer_symbol_table, state.symbol_table);
+
   PRECONDITION(state.top().end_of_function->is_end_function());
 
+  symex_threaded_step(state, get_goto_function);
   while(!state.call_stack().empty())
+  {
+    state.has_saved_target = false;
     symex_threaded_step(state, get_goto_function);
+  }
+
+  // Clients may need to construct a namespace with both the names in
+  // the original goto-program and the names generated during symbolic
+  // execution, so return the names generated through symbolic execution
+  // through `new_symbol_table`.
+  new_symbol_table = state.symbol_table;
+}
+
+void goto_symext::resume_symex_from_saved_state(
+  const goto_functionst &goto_functions,
+  const statet &saved_state,
+  symex_target_equationt *const saved_equation,
+  symbol_tablet &new_symbol_table)
+{
+  const get_goto_functiont get_goto_function = get_function_from_goto_functions(
+      goto_functions);
 
-  state.dirty=nullptr;
+  // saved_state contains a pointer to a symex_target_equationt that is
+  // almost certainly stale. This is because equations are owned by bmcts,
+  // and we construct a new bmct for every path that we execute. We're on a
+  // new path now, so the old bmct and the equation that it owned have now
+  // been deallocated. So, construct a new state from the old one, and make
+  // its equation member point to the (valid) equation passed as an argument.
+  statet state(saved_state, saved_equation);
+
+  symex_transition(state, state.source.pc);
+  // Do NOT do the same initialization that `symex_with_state` does for a
+  // fresh state, as that would clobber the saved state's program counter
+  symex_with_state(
+      state,
+      get_goto_function,
+      new_symbol_table);
 }
 
 void goto_symext::symex_instruction_range(
@@ -218,19 +253,22 @@ void goto_symext::symex_instruction_range(
   const goto_programt::const_targett limit)
 {
   initialize_entry_point(state, get_goto_function, first, limit);
+  ns = namespacet(outer_symbol_table, state.symbol_table);
   while(state.source.pc->function!=limit->function || state.source.pc!=limit)
     symex_threaded_step(state, get_goto_function);
 }
 
 void goto_symext::symex_from_entry_point_of(
-  const goto_functionst &goto_functions)
+  const goto_functionst &goto_functions,
+  symbol_tablet &new_symbol_table)
 {
-  symex_from_entry_point_of(get_function_from_goto_functions(goto_functions));
+  symex_from_entry_point_of(
+    get_function_from_goto_functions(goto_functions), new_symbol_table);
 }
 
-/// symex from entry point
 void goto_symext::symex_from_entry_point_of(
-  const get_goto_functiont &get_goto_function)
+  const get_goto_functiont &get_goto_function,
+  symbol_tablet &new_symbol_table)
 {
   const goto_functionst::goto_functiont *start_function;
   try
@@ -243,7 +281,15 @@ void goto_symext::symex_from_entry_point_of(
   }
 
   statet state;
-  symex_with_state(state, get_goto_function, start_function->body);
+
+  initialize_entry_point(
+    state,
+    get_goto_function,
+    start_function->body.instructions.begin(),
+    prev(start_function->body.instructions.end()));
+
+  symex_with_state(
+    state, get_goto_function, new_symbol_table);
 }
 
 /// do just one step
@@ -263,7 +309,8 @@ void goto_symext::symex_step(
 
   const goto_programt::instructiont &instruction=*state.source.pc;
 
-  merge_gotos(state);
+  if(!options.get_bool_option("paths"))
+    merge_gotos(state);
 
   // depth exceeded?
   {
diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp
index 5738f3d0c14..9ec1adc4efe 100644
--- a/src/goto-symex/symex_target_equation.cpp
+++ b/src/goto-symex/symex_target_equation.cpp
@@ -11,8 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "symex_target_equation.h"
 
-#include <cassert>
-
 #include <util/std_expr.h>
 
 #include <langapi/language_util.h>
@@ -22,15 +20,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "goto_symex_state.h"
 
-symex_target_equationt::symex_target_equationt(
-  const namespacet &_ns):ns(_ns)
-{
-}
-
-symex_target_equationt::~symex_target_equationt()
-{
-}
-
 /// read from a shared variable
 void symex_target_equationt::shared_read(
   const exprt &guard,
@@ -138,7 +127,7 @@ void symex_target_equationt::assignment(
   const sourcet &source,
   assignment_typet assignment_type)
 {
-  assert(ssa_lhs.is_not_nil());
+  PRECONDITION(ssa_lhs.is_not_nil());
 
   SSA_steps.push_back(SSA_stept());
   SSA_stept &SSA_step=SSA_steps.back();
@@ -166,7 +155,7 @@ void symex_target_equationt::decl(
   const sourcet &source,
   assignment_typet assignment_type)
 {
-  assert(ssa_lhs.is_not_nil());
+  PRECONDITION(ssa_lhs.is_not_nil());
 
   SSA_steps.push_back(SSA_stept());
   SSA_stept &SSA_step=SSA_steps.back();
@@ -601,7 +590,9 @@ void symex_target_equationt::merge_ireps(SSA_stept &SSA_step)
   // converted_io_args is merged in convert_io
 }
 
-void symex_target_equationt::output(std::ostream &out) const
+void symex_target_equationt::output(
+  std::ostream &out,
+  const namespacet &ns) const
 {
   for(const auto &step : SSA_steps)
   {
@@ -709,22 +700,3 @@ void symex_target_equationt::SSA_stept::output(
 
   out << "Guard: " << from_expr(ns, "", guard) << '\n';
 }
-
-std::ostream &operator<<(
-  std::ostream &out,
-  const symex_target_equationt &equation)
-{
-  equation.output(out);
-  return out;
-}
-
-std::ostream &operator<<(
-  std::ostream &out,
-  const symex_target_equationt::SSA_stept &step)
-{
-  // may cause lookup failures, since it's blank
-  symbol_tablet symbol_table;
-  namespacet ns(symbol_table);
-  step.output(ns, out);
-  return out;
-}
diff --git a/src/goto-symex/symex_target_equation.h b/src/goto-symex/symex_target_equation.h
index 06fb2342161..178cbeae7ab 100644
--- a/src/goto-symex/symex_target_equation.h
+++ b/src/goto-symex/symex_target_equation.h
@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <list>
 #include <iosfwd>
 
+#include <util/invariant.h>
 #include <util/merge_irep.h>
 
 #include <goto-programs/goto_program.h>
@@ -31,8 +32,8 @@ class prop_convt;
 class symex_target_equationt:public symex_targett
 {
 public:
-  explicit symex_target_equationt(const namespacet &_ns);
-  virtual ~symex_target_equationt();
+  symex_target_equationt() = default;
+  virtual ~symex_target_equationt() = default;
 
   // read event
   virtual void shared_read(
@@ -291,13 +292,13 @@ class symex_target_equationt:public symex_targett
     SSA_stepst::iterator it=SSA_steps.begin();
     for(; s!=0; s--)
     {
-      assert(it!=SSA_steps.end());
+      PRECONDITION(it != SSA_steps.end());
       it++;
     }
     return it;
   }
 
-  void output(std::ostream &out) const;
+  void output(std::ostream &out, const namespacet &ns) const;
 
   void clear()
   {
@@ -316,8 +317,6 @@ class symex_target_equationt:public symex_targett
   }
 
 protected:
-  const namespacet &ns;
-
   // for enforcing sharing in the expressions stored
   merge_irept merge_irep;
   void merge_ireps(SSA_stept &SSA_step);
@@ -330,11 +329,4 @@ inline bool operator<(
   return &(*a)<&(*b);
 }
 
-std::ostream &operator<<(
-  std::ostream &out,
-  const symex_target_equationt::SSA_stept &step);
-std::ostream &operator<<(
-  std::ostream &out,
-  const symex_target_equationt &equation);
-
 #endif // CPROVER_GOTO_SYMEX_SYMEX_TARGET_EQUATION_H
diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp
index 65075e12abf..e1a598a6588 100644
--- a/src/jbmc/jbmc_parse_options.cpp
+++ b/src/jbmc/jbmc_parse_options.cpp
@@ -19,7 +19,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/string2int.h>
 #include <util/config.h>
 #include <util/unicode.h>
-#include <util/memory_info.h>
 #include <util/invariant.h>
 
 #include <langapi/language.h>
@@ -58,8 +57,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <java_bytecode/java_bytecode_language.h>
 #include <java_bytecode/java_enum_static_init_unwind_handler.h>
 
-#include <cbmc/cbmc_solvers.h>
-#include <cbmc/bmc.h>
 #include <cbmc/version.h>
 
 jbmc_parse_optionst::jbmc_parse_optionst(int argc, const char **argv):
@@ -492,55 +489,34 @@ int jbmc_parse_optionst::doit()
   if(set_properties(goto_model))
     return 7; // should contemplate EX_USAGE from sysexits.h
 
-  // get solver
-  cbmc_solverst jbmc_solvers(
-    options,
-    goto_model.symbol_table,
-    get_message_handler());
-
-  jbmc_solvers.set_ui(ui_message_handler.get_ui());
-
-  std::unique_ptr<cbmc_solverst::solvert> jbmc_solver;
-
-  try
+  std::function<void(bmct &, const goto_modelt &)> configure_bmc;
+  if(options.get_bool_option("java-unwind-enum-static"))
   {
-    jbmc_solver=jbmc_solvers.get_solver();
+    configure_bmc = [](
+      bmct &bmc, const goto_modelt &goto_model) { // NOLINT (*)
+        bmc.add_loop_unwind_handler([&goto_model](
+                                      const irep_idt &function_id,
+                                      unsigned loop_number,
+                                      unsigned unwind,
+                                      unsigned &max_unwind) { // NOLINT (*)
+          return java_enum_static_init_unwind_handler(
+            function_id,
+            loop_number,
+            unwind,
+            max_unwind,
+            goto_model.symbol_table);
+        });
+    };
   }
-
-  catch(const char *error_msg)
+  else
   {
-    error() << error_msg << eom;
-    return 1; // should contemplate EX_SOFTWARE from sysexits.h
+    configure_bmc = [](
+      bmct &bmc, const goto_modelt &goto_model) { // NOLINT (*)
+      // NOOP
+    };
   }
-
-  prop_convt &prop_conv=jbmc_solver->prop_conv();
-
-  bmct bmc(
-    options,
-    goto_model.symbol_table,
-    get_message_handler(),
-    prop_conv);
-
-  // unwinds <clinit> loops to number of enum elements
-  if(options.get_bool_option("java-unwind-enum-static"))
-  {
-    bmc.add_loop_unwind_handler(
-      [&goto_model]
-      (const irep_idt &function_id,
-       unsigned loop_number,
-       unsigned unwind,
-       unsigned &max_unwind) { // NOLINT (*)
-        return java_enum_static_init_unwind_handler(
-          function_id,
-          loop_number,
-          unwind,
-          max_unwind,
-          goto_model.symbol_table);
-      });
-  }
-
-  // do actual BMC
-  return do_bmc(bmc, goto_model);
+  return bmct::do_language_agnostic_bmc(
+    options, goto_model, ui_message_handler.get_ui(), *this, configure_bmc);
 }
 
 bool jbmc_parse_optionst::set_properties(goto_modelt &goto_model)
@@ -838,35 +814,6 @@ bool jbmc_parse_optionst::process_goto_functions(
   return false;
 }
 
-/// invoke main modules
-int jbmc_parse_optionst::do_bmc(bmct &bmc, goto_modelt &goto_model)
-{
-  bmc.set_ui(ui_message_handler.get_ui());
-
-  int result=6;
-
-  // do actual BMC
-  switch(bmc.run(goto_model.goto_functions))
-  {
-    case safety_checkert::resultt::SAFE:
-      result=0;
-      break;
-    case safety_checkert::resultt::UNSAFE:
-      result=10;
-      break;
-    case safety_checkert::resultt::ERROR:
-      result=6;
-      break;
-  }
-
-  // let's log some more statistics
-  debug() << "Memory consumption:" << messaget::endl;
-  memory_info(debug());
-  debug() << eom;
-
-  return result;
-}
-
 /// display command line help
 void jbmc_parse_optionst::help()
 {
@@ -921,18 +868,7 @@ void jbmc_parse_optionst::help()
     " --java-unwind-enum-static    try to unwind loops in static initialization of enums\n" // NOLINT(*)
     "\n"
     "BMC options:\n"
-    " --program-only               only show program expression\n"
-    " --show-loops                 show the loops in the program\n"
-    " --depth nr                   limit search depth\n"
-    " --unwind nr                  unwind nr times\n"
-    " --unwindset L:B,...          unwind loop L with a bound of B\n"
-    "                              (use --show-loops to get the loop IDs)\n"
-    " --show-vcc                   show the verification conditions\n"
-    " --slice-formula              remove assignments unrelated to property\n"
-    " --unwinding-assertions       generate unwinding assertions\n"
-    " --partial-loops              permit paths with partial loops\n"
-    " --no-pretty-names            do not simplify identifiers\n"
-    " --graphml-witness filename   write the witness in GraphML format to filename\n" // NOLINT(*)
+    HELP_BMC
     "\n"
     "Backend options:\n"
     " --object-bits n              number of bits used for object addresses\n"
diff --git a/src/jbmc/jbmc_parse_options.h b/src/jbmc/jbmc_parse_options.h
index c2793540805..10305b88d7d 100644
--- a/src/jbmc/jbmc_parse_options.h
+++ b/src/jbmc/jbmc_parse_options.h
@@ -20,6 +20,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <analyses/goto_check.h>
 
+#include <cbmc/bmc.h>
+
 #include <goto-programs/goto_trace.h>
 #include <goto-programs/lazy_goto_model.h>
 #include <goto-programs/show_properties.h>
@@ -32,21 +34,21 @@ class optionst;
 
 // clang-format off
 #define JBMC_OPTIONS \
-  "(program-only)(preprocess)(slice-by-trace):" \
+  OPT_BMC \
+  "(preprocess)(slice-by-trace):" \
   OPT_FUNCTIONS \
-  "(no-simplify)(unwind):(unwindset):(slice-formula)(full-slice)" \
+  "(no-simplify)(full-slice)" \
   "(debug-level):(no-propagation)(no-simplify-if)" \
   "(document-subgoals)(outfile):" \
   "(object-bits):" \
   "(classpath):(cp):(main-class):" \
-  "(depth):(partial-loops)(no-unwinding-assertions)(unwinding-assertions)" \
   OPT_GOTO_CHECK \
   "(no-assertions)(no-assumptions)" \
   "(no-built-in-assertions)" \
   "(xml-ui)(json-ui)" \
   "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(opensmt)(mathsat)" \
   "(no-sat-preprocessor)" \
-  "(no-pretty-names)(beautify)" \
+  "(beautify)" \
   "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\
   "(refine-strings)" \
   "(string-printable)" \
@@ -55,7 +57,7 @@ class optionst;
   "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
   OPT_SHOW_GOTO_FUNCTIONS \
   "(show-loops)" \
-  "(show-symbol-table)(show-parse-tree)(show-vcc)" \
+  "(show-symbol-table)(show-parse-tree)" \
   OPT_SHOW_PROPERTIES \
   "(drop-unused-functions)" \
   "(property):(stop-on-fail)(trace)" \
@@ -67,7 +69,6 @@ class optionst;
   "(ppc-macos)" \
   "(arrays-uf-always)(arrays-uf-never)" \
   "(no-arch)(arch):" \
-  "(graphml-witness):" \
   JAVA_BYTECODE_LANGUAGE_OPTIONS \
   "(java-unwind-enum-static)" \
   "(localize-faults)(localize-faults-method):" \
@@ -103,7 +104,6 @@ class jbmc_parse_optionst:
     std::unique_ptr<goto_modelt> &goto_model, const optionst &);
 
   bool set_properties(goto_modelt &goto_model);
-  int do_bmc(bmct &, goto_modelt &goto_model);
 };
 
 #endif // CPROVER_JBMC_JBMC_PARSE_OPTIONS_H