From c53d630fed233c568e3a6476d5a11018eadaea26 Mon Sep 17 00:00:00 2001
From: Kareem Khazem <karkhaz@karkhaz.com>
Date: Mon, 6 Nov 2017 10:48:07 -0500
Subject: [PATCH 1/6] [path explore 2/7] Ignore jbmc binary

---
 .gitignore | 1 +
 1 file changed, 1 insertion(+)

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

From d7a70e1baf07fdb0410f21e40416040d5c1db1a6 Mon Sep 17 00:00:00 2001
From: Kareem Khazem <karkhaz@karkhaz.com>
Date: Thu, 15 Feb 2018 08:46:00 +0000
Subject: [PATCH 2/6] [path explore 3/7] Logical ops for resultt

The operators &= and |= can now be used between two
safety_checkert::resultt objects. They return the "best" or "worst" of
two results, and additionally assign that result to the LHS.  The
assignment operators are useful when repeatedly performing a safety
check and wanting to return a single error code that either describes
the best or worst outcome of all the safety checks combined.
---
 src/goto-programs/safety_checker.h | 36 ++++++++++++++++++++++++++++++
 1 file changed, 36 insertions(+)

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

From c88a3ab5a0aa38328f45c9c1174e63b723518c59 Mon Sep 17 00:00:00 2001
From: Kareem Khazem <karkhaz@karkhaz.com>
Date: Wed, 29 Nov 2017 13:48:49 -0500
Subject: [PATCH 3/6] [path explore 4/7] Factor out common BMC code

The CBMC and JBMC frontends included identical code for running BMC
after the language-specific preprocessing. This commit moves that common
code into a static method of bmct.

Parse options and help text related to bounded model checking are
defined in bmc.h.
---
 src/cbmc/bmc.cpp                |  68 +++++++++++++++++++
 src/cbmc/bmc.h                  |  50 ++++++++++++++
 src/cbmc/cbmc_parse_options.cpp |  81 ++---------------------
 src/cbmc/cbmc_parse_options.h   |  13 ++--
 src/jbmc/jbmc_parse_options.cpp | 114 +++++++-------------------------
 src/jbmc/jbmc_parse_options.h   |  13 ++--
 6 files changed, 161 insertions(+), 178 deletions(-)

diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
index 9bc86d3eec6..4e5a1c9bba2 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>
@@ -37,6 +40,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"
 
@@ -595,3 +599,67 @@ 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)
+{
+  cbmc_solverst solvers(
+    opts, goto_model.symbol_table, message.get_message_handler());
+  solvers.set_ui(ui);
+  std::unique_ptr<cbmc_solverst::solvert> solver;
+  try
+  {
+    solver = solvers.get_solver();
+  }
+  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();
+  }
+
+  bmct bmc(
+    opts,
+    goto_model.symbol_table,
+    message.get_message_handler(),
+    solver->prop_conv());
+
+  frontend_configure_bmc(bmc, goto_model);
+  bmc.set_ui(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
+  message.debug() << "Memory consumption:" << messaget::endl;
+  memory_info(message.debug());
+  message.debug() << eom;
+
+  return result;
+}
diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h
index b3f9a7846e1..d46ae0812cc 100644
--- a/src/cbmc/bmc.h
+++ b/src/cbmc/bmc.h
@@ -28,6 +28,7 @@ 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>
 
@@ -82,6 +83,25 @@ 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:
   const optionst &options;
   symbol_tablet new_symbol_table;
@@ -144,6 +164,36 @@ class bmct:public safety_checkert
   template <template <class goalt> class covert>
   friend class bmc_goal_covert;
   friend class fault_localizationt;
+
+#define OPT_BMC                                                                \
+  "(program-only)"                                                             \
+  "(show-loops)"                                                               \
+  "(show-vcc)"                                                                 \
+  "(slice-formula)"                                                            \
+  "(unwinding-assertions)"                                                     \
+  "(no-unwinding-assertions)"                                                  \
+  "(no-pretty-names)"                                                          \
+  "(partial-loops)"                                                            \
+  "(depth):"                                                                   \
+  "(unwind):"                                                                  \
+  "(unwindset):"                                                               \
+  "(graphml-witness):"                                                         \
+  "(unwindset):"
+
+#define HELP_BMC                                                               \
+  " --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..e70b0eac746 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"
 
@@ -373,13 +370,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 +539,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 +840,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 +929,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..835088622f0 100644
--- a/src/cbmc/cbmc_parse_options.h
+++ b/src/cbmc/cbmc_parse_options.h
@@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <goto-programs/goto_trace.h>
 
+#include "bmc.h"
 #include "xml_interface.h"
 
 class bmct;
@@ -30,21 +31,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 +55,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 +69,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)
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..804df90e9e9 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):" \

From e8eec2c8a81c793d4a7491607d9b43991097e92e Mon Sep 17 00:00:00 2001
From: Kareem Khazem <karkhaz@karkhaz.com>
Date: Wed, 29 Nov 2017 14:10:58 -0500
Subject: [PATCH 4/6] [path explore 5/7] Support path-based exploratio2

This commit introduces the --paths flag to CBMC, which makes CBMC
model-check each individual path of the program rather than merging
paths and model-checking the entire program.

The overall strategy involves allowing the "state" of symbolic
execution---i.e., a pair of goto_symex_statet and symex_target_equationt
---to be saved during an execution, and for an execution to be resumed
from a saved pair. By saving the state at every branch point and
disabling path merging, symbolic execution only runs along one path but
populates a worklist of saved states that should be executed later. At
the top level, CBMC or JBMC loops while the worklist of saved states is
non-empty, creating a new bmct object to resume executing each saved
path.

This commit includes the following supporting changes:

- goto_symex_statet now owns a symbol table, separate from the one
  supporting the goto_program, which is used for dynamically created
  objects during symbolic execution. goto_symex was previously using a
  symbol table that was passed to it by reference for this purpose, but
  that symbol table is needed when resuming symbolic execution from a
  saved point and so ought properly to be part of the symbolic execution
  state.

- goto_symex_statet now has a pointer to a symex_target_equationt, which
  can be updated with an equation from a previously-saved symbolic
  execution run. While equations are also conceptually part of the state
  of symbolic execution, they are heavily used after symbolic execution
  has completed (and the symex state has been deallocated) and so the
  equation is not owned by the state. An explicit copy constructor has
  been added to goto_symex_statet that initializes the equation member,
  so that symbolic execution can proceed either with an empty equation
  or with an equation that was earlier saved.

- goto_symex_statet no longer has a pointer to a dirtyt, as this was
  hindering it from being copied.
---
 src/analyses/dirty.cpp                        |   1 +
 src/analyses/dirty.h                          |  41 +++++-
 src/cbmc/bmc.cpp                              | 113 +++++++++++----
 src/cbmc/bmc.h                                | 136 +++++++++++++++++-
 src/cbmc/cbmc_parse_options.cpp               |   3 +
 src/cbmc/cbmc_parse_options.h                 |   2 +-
 src/cbmc/symex_bmc.cpp                        |  12 +-
 src/cbmc/symex_bmc.h                          |   6 +-
 .../accelerate/scratch_program.cpp            |   2 +-
 .../accelerate/scratch_program.h              |  12 +-
 src/goto-symex/auto_objects.cpp               |   7 +-
 src/goto-symex/goto_symex.h                   |  84 ++++++++---
 src/goto-symex/goto_symex_state.cpp           |  52 +++----
 src/goto-symex/goto_symex_state.h             |  68 +++++++--
 src/goto-symex/symex_builtin_functions.cpp    |  18 ++-
 src/goto-symex/symex_decl.cpp                 |   4 +-
 src/goto-symex/symex_dereference.cpp          |  11 +-
 src/goto-symex/symex_dereference_state.cpp    |   4 +-
 src/goto-symex/symex_function_call.cpp        |  15 +-
 src/goto-symex/symex_goto.cpp                 | 106 ++++++++++++--
 src/goto-symex/symex_main.cpp                 |  87 ++++++++---
 src/goto-symex/symex_target_equation.cpp      |  38 +----
 src/goto-symex/symex_target_equation.h        |  18 +--
 src/jbmc/jbmc_parse_options.h                 |   1 -
 24 files changed, 615 insertions(+), 226 deletions(-)

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 4e5a1c9bba2..66ff5cb90ce 100644
--- a/src/cbmc/bmc.cpp
+++ b/src/cbmc/bmc.cpp
@@ -29,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>
@@ -363,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())
@@ -607,13 +607,69 @@ int bmct::do_language_agnostic_bmc(
   messaget &message,
   std::function<void(bmct &, const goto_modelt &)> frontend_configure_bmc)
 {
-  cbmc_solverst solvers(
-    opts, goto_model.symbol_table, message.get_message_handler());
-  solvers.set_ui(ui);
-  std::unique_ptr<cbmc_solverst::solvert> solver;
+  message_handlert &mh = message.get_message_handler();
+  safety_checkert::resultt result;
+  goto_symext::branch_worklistt worklist;
   try
   {
-    solver = solvers.get_solver();
+    {
+      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)
   {
@@ -631,35 +687,30 @@ int bmct::do_language_agnostic_bmc(
     throw std::current_exception();
   }
 
-  bmct bmc(
-    opts,
-    goto_model.symbol_table,
-    message.get_message_handler(),
-    solver->prop_conv());
-
-  frontend_configure_bmc(bmc, goto_model);
-  bmc.set_ui(ui);
-
-  int result = CPROVER_EXIT_INTERNAL_ERROR;
-
-  // do actual BMC
-  switch(bmc.run(goto_model.goto_functions))
+  switch(result)
   {
   case safety_checkert::resultt::SAFE:
-    result = CPROVER_EXIT_VERIFICATION_SAFE;
-    break;
+    return CPROVER_EXIT_VERIFICATION_SAFE;
   case safety_checkert::resultt::UNSAFE:
-    result = CPROVER_EXIT_VERIFICATION_UNSAFE;
-    break;
+    return CPROVER_EXIT_VERIFICATION_UNSAFE;
   case safety_checkert::resultt::ERROR:
-    result = CPROVER_EXIT_INTERNAL_ERROR;
-    break;
+    return CPROVER_EXIT_INTERNAL_ERROR;
   }
+  UNREACHABLE;
+}
 
-  // let's log some more statistics
-  message.debug() << "Memory consumption:" << messaget::endl;
-  memory_info(message.debug());
-  message.debug() << eom;
+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");
+}
 
-  return result;
+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 d46ae0812cc..f3c4bdf3dfd 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>
@@ -34,19 +37,46 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "symex_bmc.h"
 
+class cbmc_solverst;
+
 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)
   {
@@ -103,10 +133,47 @@ class bmct:public safety_checkert
       });
 
 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;
@@ -165,6 +232,61 @@ class bmct:public safety_checkert
   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)"                                                               \
@@ -174,6 +296,7 @@ class bmct:public safety_checkert
   "(no-unwinding-assertions)"                                                  \
   "(no-pretty-names)"                                                          \
   "(partial-loops)"                                                            \
+  "(paths)"                                                                    \
   "(depth):"                                                                   \
   "(unwind):"                                                                  \
   "(unwindset):"                                                               \
@@ -181,6 +304,7 @@ class bmct:public safety_checkert
   "(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"                         \
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index e70b0eac746..0a6d7bee2d2 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -107,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);
 
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
index 835088622f0..4d5cc8ed943 100644
--- a/src/cbmc/cbmc_parse_options.h
+++ b/src/cbmc/cbmc_parse_options.h
@@ -24,6 +24,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "bmc.h"
 #include "xml_interface.h"
+#include "cbmc_solvers.h"
 
 class bmct;
 class goto_functionst;
@@ -100,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-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..cd3e6176062 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,49 @@ 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
 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 +87,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 +98,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 +118,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 +131,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 +143,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 +194,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 +208,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 +250,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 +459,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/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.h b/src/jbmc/jbmc_parse_options.h
index 804df90e9e9..10305b88d7d 100644
--- a/src/jbmc/jbmc_parse_options.h
+++ b/src/jbmc/jbmc_parse_options.h
@@ -104,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

From 53df56780e5e384b7dc9c820b84e3f2d8adabe9b Mon Sep 17 00:00:00 2001
From: Kareem Khazem <karkhaz@karkhaz.com>
Date: Sun, 3 Dec 2017 16:33:19 -0500
Subject: [PATCH 5/6] [path explore 6/7] cpplint & clang-fmt agree on :

cpplint now complains if a derived-class declaration is formatted as

  class derived: base

rather than complaining if it is formatted as

  class derived : base

(with a space on both sides of the colon). The latter style is the one
enforced by clang-format, meaning that the two linters were inconsistent.
---
 scripts/cpplint.py | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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

From d67fa60d06028adf6eeb28e818283307dbbca7c5 Mon Sep 17 00:00:00 2001
From: Kareem Khazem <karkhaz@karkhaz.com>
Date: Sat, 3 Feb 2018 10:08:53 +0000
Subject: [PATCH 6/6] [path explore 7/7] Path exploration documentation

---
 src/cbmc/bmc.h              |   5 ++
 src/goto-symex/goto_symex.h |   4 ++
 src/goto-symex/module.md    | 113 ++++++++++++++++++++++++++++++++++++
 3 files changed, 122 insertions(+)

diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h
index f3c4bdf3dfd..8357b609aed 100644
--- a/src/cbmc/bmc.h
+++ b/src/cbmc/bmc.h
@@ -39,6 +39,11 @@ Author: Daniel Kroening, kroening@kroening.com
 
 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:
diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
index cd3e6176062..f27a1f1ffac 100644
--- a/src/goto-symex/goto_symex.h
+++ b/src/goto-symex/goto_symex.h
@@ -38,6 +38,10 @@ class side_effect_exprt;
 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:
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