diff --git a/doc/man/cbmc.1 b/doc/man/cbmc.1
index 0e454caf4c1..4f587608d65 100644
--- a/doc/man/cbmc.1
+++ b/doc/man/cbmc.1
@@ -620,6 +620,24 @@ verbosity level
 \fB\-\-timestamp\fR [\fBmonotonic\fR|\fBwall\fR]
 Print microsecond\-precision timestamps.  \fBmonotonic\fR: stamps increase
 monotonically.  \fBwall\fR: ISO\-8601 wall clock timestamps.
+.TP
+\fB\-\-symex\-callgrind\fR \fIfile\fR
+Write per\-source\-location symbolic execution step counts in callgrind
+format to \fIfile\fR.  The output can be visualized with
+.BR kcachegrind (1)
+or
+.BR qcachegrind (1)
+to identify expensive code paths.
+.TP
+\fB\-\-show\-symex\-progress\fR
+Show a live display of the call stack and loop nesting during symbolic
+execution.  When output is a terminal, the display is redrawn in place
+every 2 seconds showing the current call stack with indentation, the
+active function highlighted, and loop iteration counts.  When output is
+not a terminal, a one\-line progress summary is printed periodically
+instead.  At the end of symbolic execution, the maximum call depth and
+loop nesting observed are reported.  Per\-function step counts and peak
+memory usage are always reported at verbosity level 9 (statistics).
 .SH ENVIRONMENT
 All tools honor the TMPDIR environment variable when generating temporary
 files and directories. Furthermore note that
diff --git a/regression/cbmc/resource_monitoring/callgrind.desc b/regression/cbmc/resource_monitoring/callgrind.desc
new file mode 100644
index 00000000000..d3a25d87d28
--- /dev/null
+++ b/regression/cbmc/resource_monitoring/callgrind.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+--unwind 7 --symex-callgrind ../callgrind_test.out
+^Symex callgrind data written to
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Tests that --symex-callgrind produces a callgrind-format output file
+that can be visualized with KCachegrind/QCachegrind.
diff --git a/regression/cbmc/resource_monitoring/main.c b/regression/cbmc/resource_monitoring/main.c
new file mode 100644
index 00000000000..89c69e8a0e9
--- /dev/null
+++ b/regression/cbmc/resource_monitoring/main.c
@@ -0,0 +1,14 @@
+int factorial(int n)
+{
+  if(n <= 1)
+    return 1;
+  return n * factorial(n - 1);
+}
+
+int main()
+{
+  int x;
+  __CPROVER_assume(x >= 1 && x <= 5);
+  int result = factorial(x);
+  __CPROVER_assert(result >= 1, "positive");
+}
diff --git a/regression/cbmc/resource_monitoring/progress.desc b/regression/cbmc/resource_monitoring/progress.desc
new file mode 100644
index 00000000000..50c3ac99093
--- /dev/null
+++ b/regression/cbmc/resource_monitoring/progress.desc
@@ -0,0 +1,12 @@
+CORE
+main.c
+--unwind 7 --show-symex-progress --verbosity 9
+^Max call depth: [1-9]\d*, max active loops: \d+$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Tests that --show-symex-progress reports max call depth and loop nesting.
+The interactive terminal display is not tested here (requires a real
+terminal), but the summary statistics are always emitted.
diff --git a/regression/cbmc/resource_monitoring/test.desc b/regression/cbmc/resource_monitoring/test.desc
new file mode 100644
index 00000000000..4a8d9d881e8
--- /dev/null
+++ b/regression/cbmc/resource_monitoring/test.desc
@@ -0,0 +1,13 @@
+CORE
+main.c
+--unwind 7 --verbosity 9
+^Symex steps: \d+ total$
+^  factorial: \d+ steps \(\d+%\)$
+^Peak memory: \d+ MB$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Tests that per-function symex step counts and peak memory are reported
+at statistics verbosity level.
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 6548067d791..cc8ca161ba1 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -216,8 +216,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("no-array-field-sensitivity", true);
   }
 
-  if(cmdline.isset("reachability-slice") &&
-     cmdline.isset("reachability-slice-fb"))
+  if(
+    cmdline.isset("reachability-slice") &&
+    cmdline.isset("reachability-slice-fb"))
   {
     log.error()
       << "--reachability-slice and --reachability-slice-fb must not be "
@@ -300,9 +301,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("no-simplify"))
     options.set_option("simplify", false);
 
-  if(cmdline.isset("stop-on-fail") ||
-     cmdline.isset("dimacs") ||
-     cmdline.isset("outfile"))
+  if(
+    cmdline.isset("stop-on-fail") || cmdline.isset("dimacs") ||
+    cmdline.isset("outfile"))
     options.set_option("stop-on-fail", true);
 
   if(
@@ -447,11 +448,18 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("symex-coverage-report"))
   {
     options.set_option(
-      "symex-coverage-report",
-      cmdline.get_value("symex-coverage-report"));
+      "symex-coverage-report", cmdline.get_value("symex-coverage-report"));
     options.set_option("paths-symex-explore-all", true);
   }
 
+  if(cmdline.isset("symex-callgrind"))
+  {
+    options.set_option("symex-callgrind", cmdline.get_value("symex-callgrind"));
+  }
+
+  if(cmdline.isset("show-symex-progress"))
+    options.set_option("show-symex-progress", true);
+
   if(cmdline.isset("validate-ssa-equation"))
   {
     options.set_option("validate-ssa-equation", true);
@@ -508,8 +516,7 @@ int cbmc_parse_optionst::doit()
   // Unwinding of transition systems is done by hw-cbmc.
   //
 
-  if(cmdline.isset("module") ||
-     cmdline.isset("gen-interface"))
+  if(cmdline.isset("module") || cmdline.isset("gen-interface"))
   {
     log.error() << "This version of CBMC has no support for "
                    " hardware modules. Please use hw-cbmc."
@@ -570,7 +577,7 @@ int cbmc_parse_optionst::doit()
       return CPROVER_EXIT_INCORRECT_TASK;
     }
 
-    std::string filename=cmdline.args[0];
+    std::string filename = cmdline.args[0];
 
     std::ifstream infile(widen_if_needed(filename));
 
@@ -581,10 +588,9 @@ int cbmc_parse_optionst::doit()
       return CPROVER_EXIT_INCORRECT_TASK;
     }
 
-    std::unique_ptr<languaget> language=
-      get_language_from_filename(filename);
+    std::unique_ptr<languaget> language = get_language_from_filename(filename);
 
-    if(language==nullptr)
+    if(language == nullptr)
     {
       log.error() << "failed to figure out type of file '" << filename << "'"
                   << messaget::eom;
@@ -608,11 +614,12 @@ int cbmc_parse_optionst::doit()
   int get_goto_program_ret =
     get_goto_program(goto_model, options, cmdline, ui_message_handler);
 
-  if(get_goto_program_ret!=-1)
+  if(get_goto_program_ret != -1)
     return get_goto_program_ret;
 
-  if(cmdline.isset("show-claims") || // will go away
-     cmdline.isset("show-properties")) // use this one
+  if(
+    cmdline.isset("show-claims") ||   // will go away
+    cmdline.isset("show-properties")) // use this one
   {
     show_properties(goto_model, ui_message_handler);
     return CPROVER_EXIT_SUCCESS;
@@ -1024,6 +1031,10 @@ void cbmc_parse_optionst::help()
     HELP_SHOW_PROPERTIES
     " {y--symex-coverage-report} {uf} \t generate a Cobertura XML coverage"
     " report in {uf}\n"
+    " {y--symex-callgrind} {uf} \t write symex step profile in callgrind"
+    " format to {uf} (view with kcachegrind)\n"
+    " {y--show-symex-progress} \t show live call stack and loop nesting during"
+    " symbolic execution (terminal only)\n"
     " {y--property} {uid} \t only check one specific property\n"
     " {y--trace} \t give a counterexample trace for failed properties\n"
     " {y--stop-on-fail} \t stop analysis once a failed property is detected"
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
index a5890bfb88d..8a07f765ee8 100644
--- a/src/cbmc/cbmc_parse_options.h
+++ b/src/cbmc/cbmc_parse_options.h
@@ -62,6 +62,8 @@ class optionst;
   "(export-symex-ready-goto):" \
   OPT_COVER \
   "(symex-coverage-report):" \
+  "(symex-callgrind):" \
+  "(show-symex-progress)" \
   "(mm):" \
   OPT_TIMESTAMP \
   "(arrays-uf-always)(arrays-uf-never)" \
diff --git a/src/goto-checker/bmc_util.cpp b/src/goto-checker/bmc_util.cpp
index 5bb3d9ce459..e6fe40c6fd0 100644
--- a/src/goto-checker/bmc_util.cpp
+++ b/src/goto-checker/bmc_util.cpp
@@ -12,6 +12,7 @@ Author: Daniel Kroening, Peter Schrammel
 #include "bmc_util.h"
 
 #include <util/json_stream.h>
+#include <util/memory_info.h>
 #include <util/ui_message.h>
 
 #include <goto-programs/graphml_witness.h>
@@ -386,9 +387,8 @@ void run_property_decider(
     << messaget::eom;
 
   property_decider.add_constraint_from_goals(
-    [&properties](const irep_idt &property_id) {
-      return is_property_to_check(properties.at(property_id).status);
-    });
+    [&properties](const irep_idt &property_id)
+    { return is_property_to_check(properties.at(property_id).status); });
 
   auto const sat_solver_start = std::chrono::steady_clock::now();
 
@@ -407,6 +407,8 @@ void run_property_decider(
   solver_runtime += std::chrono::duration<double>(solver_stop - solver_start);
   log.statistics() << "Runtime decision procedure: " << solver_runtime.count()
                    << "s" << messaget::eom;
+  log.statistics() << "Peak memory: " << peak_memory_bytes() / (1024 * 1024)
+                   << " MB" << messaget::eom;
 
   if(dec_result == decision_proceduret::resultt::D_SATISFIABLE)
   {
diff --git a/src/goto-checker/multi_path_symex_checker.cpp b/src/goto-checker/multi_path_symex_checker.cpp
index 40f60b6ed85..8379ba9c248 100644
--- a/src/goto-checker/multi_path_symex_checker.cpp
+++ b/src/goto-checker/multi_path_symex_checker.cpp
@@ -23,6 +23,8 @@ Author: Daniel Kroening, Peter Schrammel
 #include "counterexample_beautification.h"
 #include "goto_symex_fault_localizer.h"
 
+#include <fstream>
+
 multi_path_symex_checkert::multi_path_symex_checkert(
   const optionst &options,
   ui_message_handlert &ui_message_handler,
@@ -37,8 +39,8 @@ multi_path_symex_checkert::multi_path_symex_checkert(
   PRECONDITION(!has_vector(goto_model.get_goto_functions()));
 }
 
-incremental_goto_checkert::resultt multi_path_symex_checkert::
-operator()(propertiest &properties)
+incremental_goto_checkert::resultt
+multi_path_symex_checkert::operator()(propertiest &properties)
 {
   resultt result(resultt::progresst::DONE);
 
@@ -60,6 +62,21 @@ operator()(propertiest &properties)
       symex,
       ui_message_handler);
 
+    // Write callgrind-format symex profile if requested
+    {
+      const std::string callgrind_file = options.get_option("symex-callgrind");
+      if(!callgrind_file.empty())
+      {
+        std::ofstream out(callgrind_file);
+        if(out)
+        {
+          symex.write_callgrind(out);
+          log.status() << "Symex callgrind data written to " << callgrind_file
+                       << messaget::eom;
+        }
+      }
+    }
+
     update_properties(properties, result.updated_properties);
 
     // Have we got anything to check? Otherwise we return DONE.
diff --git a/src/goto-checker/multi_path_symex_only_checker.cpp b/src/goto-checker/multi_path_symex_only_checker.cpp
index ce81e072e1d..ca2d6499d9f 100644
--- a/src/goto-checker/multi_path_symex_only_checker.cpp
+++ b/src/goto-checker/multi_path_symex_only_checker.cpp
@@ -11,6 +11,8 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include "multi_path_symex_only_checker.h"
 
+#include <util/console.h>
+#include <util/memory_info.h>
 #include <util/ui_message.h>
 
 #include <goto-symex/shadow_memory.h>
@@ -19,6 +21,9 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include "bmc_util.h"
 
+#include <algorithm>
+#include <fstream>
+
 multi_path_symex_only_checkert::multi_path_symex_only_checkert(
   const optionst &options,
   ui_message_handlert &ui_message_handler,
@@ -41,8 +46,8 @@ multi_path_symex_only_checkert::multi_path_symex_only_checkert(
     options.get_list_option("unwindset"), goto_model, ui_message_handler);
 }
 
-incremental_goto_checkert::resultt multi_path_symex_only_checkert::
-operator()(propertiest &properties)
+incremental_goto_checkert::resultt
+multi_path_symex_only_checkert::operator()(propertiest &properties)
 {
   generate_equation();
 
@@ -52,6 +57,21 @@ operator()(propertiest &properties)
     symex,
     ui_message_handler);
 
+  // Write callgrind-format symex profile if requested
+  {
+    const std::string callgrind_file = options.get_option("symex-callgrind");
+    if(!callgrind_file.empty())
+    {
+      std::ofstream out(callgrind_file);
+      if(out)
+      {
+        symex.write_callgrind(out);
+        log.status() << "Symex callgrind data written to " << callgrind_file
+                     << messaget::eom;
+      }
+    }
+  }
+
   if(options.get_bool_option("show-vcc"))
   {
     show_vcc(options, ui_message_handler, equation);
@@ -80,15 +100,65 @@ void multi_path_symex_only_checkert::generate_equation()
 
   const auto symex_start = std::chrono::steady_clock::now();
 
+  symex.interactive_display_enabled =
+    options.get_bool_option("show-symex-progress");
+
   symex_symbol_table = symex.symex_from_entry_point_of(
     goto_symext::get_goto_function(goto_model), fields);
 
+  // Clear interactive display before printing final stats
+  if(symex.interactive_display_enabled && consolet::is_terminal())
+  {
+    auto &out = consolet::out();
+    for(std::size_t i = 0; i < symex.interactive_display_lines; ++i)
+      out << consolet::cursorup << consolet::cleareol;
+    symex.interactive_display_lines = 0;
+  }
+
   const auto symex_stop = std::chrono::steady_clock::now();
   std::chrono::duration<double> symex_runtime =
     std::chrono::duration<double>(symex_stop - symex_start);
   log.statistics() << "Runtime Symex: " << symex_runtime.count() << "s"
                    << messaget::eom;
 
+  // Report per-function symex step counts (top contributors)
+  const auto &step_counts = symex.get_function_step_counts();
+  if(!step_counts.empty())
+  {
+    // Sort by step count descending
+    std::vector<std::pair<irep_idt, std::size_t>> sorted(
+      step_counts.begin(), step_counts.end());
+    std::sort(
+      sorted.begin(),
+      sorted.end(),
+      [](const auto &a, const auto &b) { return a.second > b.second; });
+
+    std::size_t total = 0;
+    for(const auto &entry : sorted)
+      total += entry.second;
+
+    log.statistics() << "Symex steps: " << total << " total" << messaget::eom;
+
+    if(symex.interactive_display_enabled)
+    {
+      log.statistics() << "Max call depth: " << symex.max_call_depth_seen
+                       << ", max active loops: " << symex.max_active_loops_seen
+                       << messaget::eom;
+    }
+
+    const std::size_t max_entries = 10;
+    for(std::size_t i = 0; i < std::min(max_entries, sorted.size()); ++i)
+    {
+      log.statistics() << "  " << sorted[i].first << ": " << sorted[i].second
+                       << " steps ("
+                       << (100 * sorted[i].second + total / 2) / total << "%)"
+                       << messaget::eom;
+    }
+  }
+
+  log.statistics() << "Peak memory: " << peak_memory_bytes() / (1024 * 1024)
+                   << " MB" << messaget::eom;
+
   postprocess_equation(symex, equation, options, ns, ui_message_handler);
 }
 
diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
index 5980573f0cd..fe23e631356 100644
--- a/src/goto-symex/goto_symex.h
+++ b/src/goto-symex/goto_symex.h
@@ -19,6 +19,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "symex_config.h"
 #include "symex_target_equation.h"
 
+#include <chrono>
+#include <map>
+
 class address_of_exprt;
 class function_application_exprt;
 class goto_symex_statet;
@@ -89,8 +92,8 @@ class goto_symext
   /// \remarks
   /// This allows goto_symext to be divorced from the particular type of
   /// goto_modelt that provides the function bodies
-  typedef
-    std::function<const goto_functionst::goto_functiont &(const irep_idt &)>
+  typedef std::function<const goto_functionst::goto_functiont &(
+    const irep_idt &)>
     get_goto_functiont;
 
   /// Return a function to get/load a goto function from the given goto model
@@ -305,10 +308,7 @@ class goto_symext
     statet &state,
     bool write,
     bool is_in_quantifier);
-  exprt address_arithmetic(
-    const exprt &,
-    statet &,
-    bool keep_array);
+  exprt address_arithmetic(const exprt &, statet &, bool keep_array);
 
   /// Symbolically execute a GOTO instruction
   /// \param state: Symbolic execution state for current instruction
@@ -831,6 +831,47 @@ class goto_symext
   unsigned _total_vccs, _remaining_vccs;
   ///@}
 
+  /// Per-function symex step counts, populated when resource monitoring
+  /// is enabled. Maps function identifier to number of symex steps.
+  std::map<irep_idt, std::size_t> function_step_counts;
+
+  /// Per-source-location step counts for callgrind output.
+  /// Key is (file, function, line) tuple.
+  struct source_keyt
+  {
+    irep_idt file;
+    irep_idt function;
+    irep_idt line;
+    bool operator<(const source_keyt &o) const
+    {
+      if(file != o.file)
+        return file < o.file;
+      if(function != o.function)
+        return function < o.function;
+      return line < o.line;
+    }
+  };
+  std::map<source_keyt, std::size_t> source_location_step_counts;
+
+  /// Total symex steps and timestamp for periodic progress reporting.
+  std::size_t total_symex_steps = 0;
+  std::size_t last_equation_size = 0;
+  std::chrono::steady_clock::time_point last_progress_report =
+    std::chrono::steady_clock::now();
+
+public:
+  /// When true, show live call stack and loop nesting on the terminal.
+  /// Enabled by --show-symex-progress.
+  bool interactive_display_enabled = false;
+
+  /// Maximum call stack depth and loop nesting observed during symex.
+  std::size_t max_call_depth_seen = 0;
+  std::size_t max_active_loops_seen = 0;
+
+  /// Number of lines drawn by the last interactive display, for redrawing.
+  std::size_t interactive_display_lines = 0;
+
+protected:
   complexity_limitert complexity_module;
 
   /// Shadow memory instrumentation API
@@ -855,6 +896,16 @@ class goto_symext
     return _remaining_vccs;
   }
 
+  /// Get per-function symex step counts for resource monitoring.
+  const std::map<irep_idt, std::size_t> &get_function_step_counts() const
+  {
+    return function_step_counts;
+  }
+
+  /// Write symex step counts in callgrind format for visualization
+  /// with KCachegrind/QCachegrind.
+  void write_callgrind(std::ostream &out) const;
+
   void validate(const validation_modet vm) const
   {
     target.validate(ns, vm);
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
index a6ca641f16e..015d1724310 100644
--- a/src/goto-symex/symex_main.cpp
+++ b/src/goto-symex/symex_main.cpp
@@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com
 /// \file
 /// Symbolic Execution
 
+#include <util/console.h>
 #include <util/exception_utils.h>
 #include <util/expr_iterator.h>
 #include <util/expr_util.h>
@@ -17,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/invariant.h>
 #include <util/magic.h>
 #include <util/mathematical_expr.h>
+#include <util/memory_info.h>
 #include <util/replace_symbol.h>
 #include <util/std_expr.h>
 
@@ -25,6 +27,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "goto_symex.h"
 #include "path_storage.h"
 
+#include <fstream>
 #include <memory>
 
 symex_configt::symex_configt(const optionst &options)
@@ -42,12 +45,10 @@ symex_configt::symex_configt(const optionst &options)
     show_symex_steps(options.get_bool_option("show-goto-symex-steps")),
     show_points_to_sets(options.get_bool_option("show-points-to-sets")),
     max_field_sensitivity_array_size(
-      options.is_set("no-array-field-sensitivity")
-        ? 0
-        : options.is_set("max-field-sensitivity-array-size")
-            ? options.get_unsigned_int_option(
-                "max-field-sensitivity-array-size")
-            : DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE),
+      options.is_set("no-array-field-sensitivity") ? 0
+      : options.is_set("max-field-sensitivity-array-size")
+        ? options.get_unsigned_int_option("max-field-sensitivity-array-size")
+        : DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE),
     complexity_limits_active(
       options.get_signed_int_option("symex-complexity-limit") > 0),
     cache_dereferences{options.get_bool_option("symex-cache-dereferences")}
@@ -87,7 +88,7 @@ void symex_transition(
     // This is because the way we detect loops is pretty imprecise.
 
     framet &frame = state.call_stack().top();
-    const goto_programt::instructiont &instruction=*to;
+    const goto_programt::instructiont &instruction = *to;
     for(const auto &i_e : instruction.incoming_edges)
     {
       if(
@@ -138,7 +139,7 @@ void symex_transition(
     }
   }
 
-  state.source.pc=to;
+  state.source.pc = to;
 }
 
 void symex_transition(goto_symext::statet &state)
@@ -229,7 +230,7 @@ void goto_symext::symex_assume_l2(statet &state, const exprt &cond)
   if(has_subexpr(rewritten_cond, ID_exists))
     rewrite_quantifiers(rewritten_cond, state);
 
-  if(state.threads.size()==1)
+  if(state.threads.size() == 1)
   {
     exprt tmp = state.guard.guard_expr(rewritten_cond);
     target.assumption(state.guard.as_expr(), tmp, state.source);
@@ -243,8 +244,7 @@ void goto_symext::symex_assume_l2(statet &state, const exprt &cond)
   else
     state.guard.add(rewritten_cond);
 
-  if(state.atomic_section_id!=0 &&
-     state.guard.is_false())
+  if(state.atomic_section_id != 0 && state.guard.is_false())
     symex_atomic_end(state);
 }
 
@@ -297,7 +297,8 @@ switch_to_thread(goto_symex_statet &state, const unsigned int thread_nb)
 }
 
 void goto_symext::symex_threaded_step(
-  statet &state, const get_goto_functiont &get_goto_function)
+  statet &state,
+  const get_goto_functiont &get_goto_function)
 {
   symex_step(get_goto_function, state);
 
@@ -308,10 +309,11 @@ void goto_symext::symex_threaded_step(
     return;
 
   // is there another thread to execute?
-  if(state.call_stack().empty() &&
-     state.source.thread_nr+1<state.threads.size())
+  if(
+    state.call_stack().empty() &&
+    state.source.thread_nr + 1 < state.threads.size())
   {
-    unsigned t=state.source.thread_nr+1;
+    unsigned t = state.source.thread_nr + 1;
 #if 0
     std::cout << "********* Now executing thread " << t << '\n';
 #endif
@@ -492,10 +494,9 @@ void goto_symext::initialize_path_storage_from_entry_point_of(
 goto_symext::get_goto_functiont
 goto_symext::get_goto_function(abstract_goto_modelt &goto_model)
 {
-  return [&goto_model](
-           const irep_idt &id) -> const goto_functionst::goto_functiont & {
-    return goto_model.get_goto_function(id);
-  };
+  return
+    [&goto_model](const irep_idt &id) -> const goto_functionst::goto_functiont &
+  { return goto_model.get_goto_function(id); };
 }
 
 messaget::mstreamt &
@@ -595,7 +596,120 @@ void goto_symext::symex_step(
 {
   // Print debug statements if they've been enabled.
   print_symex_step(state);
+
+  // Track per-function step counts
+  if(!state.source.function_id.empty())
+  {
+    ++function_step_counts[state.source.function_id];
+
+    const auto &loc = state.source.pc->source_location();
+    if(!loc.get_file().empty())
+    {
+      source_keyt key{loc.get_file(), state.source.function_id, loc.get_line()};
+      ++source_location_step_counts[key];
+    }
+  }
+
+  // Periodic progress reporting (every 2 seconds)
+  ++total_symex_steps;
+
+  // Track max call depth and loop nesting
+  if(interactive_display_enabled)
+  {
+    const auto depth = state.call_stack().size();
+    if(depth > max_call_depth_seen)
+      max_call_depth_seen = depth;
+
+    std::size_t active_loops = 0;
+    for(const auto &frame : state.call_stack())
+      for(const auto &loop : frame.loop_iterations)
+        if(loop.second.count > 0)
+          ++active_loops;
+    if(active_loops > max_active_loops_seen)
+      max_active_loops_seen = active_loops;
+  }
+
+  const auto now = std::chrono::steady_clock::now();
+  if(std::chrono::duration<double>(now - last_progress_report).count() >= 2.0)
+  {
+    last_progress_report = now;
+
+    if(interactive_display_enabled && consolet::is_terminal())
+    {
+      // Erase previous display
+      auto &out = consolet::out();
+      for(std::size_t i = 0; i < interactive_display_lines; ++i)
+        out << consolet::cursorup << consolet::cleareol;
+
+      std::size_t lines = 0;
+
+      // Header line
+      out << consolet::bold << "Symex: " << consolet::reset << total_symex_steps
+          << " steps, SSA " << target.SSA_steps.size() << ", "
+          << peak_memory_bytes() / (1024 * 1024) << " MB\n";
+      ++lines;
+
+      // Call stack
+      const auto &stack = state.call_stack();
+      for(std::size_t i = 0; i < stack.size(); ++i)
+      {
+        const auto &frame = stack[i];
+        const auto &fn = frame.function_identifier;
+        if(fn.empty())
+          continue;
+
+        out << std::string(2 * i, ' ');
+        if(i + 1 == stack.size())
+          out << consolet::orange;
+        out << id2string(fn);
+
+        // Show active loops in this frame
+        for(const auto &loop : frame.loop_iterations)
+        {
+          if(loop.second.count > 0)
+          {
+            out << consolet::cyan << " [" << id2string(loop.first) << " iter "
+                << loop.second.count << "]" << consolet::reset;
+          }
+        }
+
+        if(i + 1 == stack.size())
+          out << consolet::reset;
+        out << '\n';
+        ++lines;
+      }
+
+      interactive_display_lines = lines;
+      out << std::flush;
+    }
+    else
+    {
+      log.statistics() << "Symex: " << total_symex_steps << " steps, in "
+                       << id2string(state.source.function_id) << ", SSA size "
+                       << target.SSA_steps.size() << ", peak memory "
+                       << peak_memory_bytes() / (1024 * 1024) << " MB"
+                       << messaget::eom;
+    }
+  }
+
   execute_next_instruction(get_goto_function, state);
+
+  // Track formula growth — warn when a single instruction adds many SSA steps
+  {
+    const std::size_t new_size = target.SSA_steps.size();
+    const std::size_t growth = new_size - last_equation_size;
+    if(growth > 100)
+    {
+      const auto &loc = state.source.pc->source_location();
+      log.statistics() << "Large SSA growth: +" << growth << " steps at "
+                       << id2string(state.source.function_id);
+      if(!loc.get_file().empty())
+        log.statistics() << " (" << id2string(loc.get_file()) << ":"
+                         << id2string(loc.get_line()) << ")";
+      log.statistics() << ", total " << new_size << messaget::eom;
+    }
+    last_equation_size = new_size;
+  }
   kill_instruction_local_symbols(state);
 }
 
@@ -606,7 +720,7 @@ void goto_symext::execute_next_instruction(
   PRECONDITION(!state.threads.empty());
   PRECONDITION(!state.call_stack().empty());
 
-  const goto_programt::instructiont &instruction=*state.source.pc;
+  const goto_programt::instructiont &instruction = *state.source.pc;
 
   if(!symex_config.doing_path_exploration)
     merge_gotos(state);
@@ -880,3 +994,29 @@ void goto_symext::try_filter_value_sets(
       *entry_index, erase_from_jump_not_taken_value_set);
   }
 }
+
+void goto_symext::write_callgrind(std::ostream &out) const
+{
+  out << "events: SymexSteps\n\n";
+
+  // Group by file, then function, then line
+  irep_idt current_file;
+  irep_idt current_function;
+
+  for(const auto &entry : source_location_step_counts)
+  {
+    if(entry.first.file != current_file)
+    {
+      current_file = entry.first.file;
+      out << "fl=" << id2string(current_file) << '\n';
+    }
+    if(entry.first.function != current_function)
+    {
+      current_function = entry.first.function;
+      out << "fn=" << id2string(current_function) << '\n';
+    }
+    const auto &line = entry.first.line;
+    out << (line.empty() ? "0" : id2string(line)) << ' ' << entry.second
+        << '\n';
+  }
+}
diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp
index 0bb35155e01..3f73f4b87d6 100644
--- a/src/goto-symex/symex_target_equation.cpp
+++ b/src/goto-symex/symex_target_equation.cpp
@@ -22,9 +22,8 @@ Author: Daniel Kroening, kroening@kroening.com
 static std::function<void(solver_hardnesst &)>
 hardness_register_ssa(std::size_t step_index, const SSA_stept &step)
 {
-  return [step_index, &step](solver_hardnesst &hardness) {
-    hardness.register_ssa(step_index, step.cond_expr, step.source.pc);
-  };
+  return [step_index, &step](solver_hardnesst &hardness)
+  { hardness.register_ssa(step_index, step.cond_expr, step.source.pc); };
 }
 
 void symex_target_equationt::shared_read(
@@ -34,11 +33,11 @@ void symex_target_equationt::shared_read(
   const sourcet &source)
 {
   SSA_steps.emplace_back(source, goto_trace_stept::typet::SHARED_READ);
-  SSA_stept &SSA_step=SSA_steps.back();
+  SSA_stept &SSA_step = SSA_steps.back();
 
-  SSA_step.guard=guard;
-  SSA_step.ssa_lhs=ssa_object;
-  SSA_step.atomic_section_id=atomic_section_id;
+  SSA_step.guard = guard;
+  SSA_step.ssa_lhs = ssa_object;
+  SSA_step.atomic_section_id = atomic_section_id;
 
   merge_ireps(SSA_step);
 }
@@ -50,23 +49,21 @@ void symex_target_equationt::shared_write(
   const sourcet &source)
 {
   SSA_steps.emplace_back(source, goto_trace_stept::typet::SHARED_WRITE);
-  SSA_stept &SSA_step=SSA_steps.back();
+  SSA_stept &SSA_step = SSA_steps.back();
 
-  SSA_step.guard=guard;
-  SSA_step.ssa_lhs=ssa_object;
-  SSA_step.atomic_section_id=atomic_section_id;
+  SSA_step.guard = guard;
+  SSA_step.ssa_lhs = ssa_object;
+  SSA_step.atomic_section_id = atomic_section_id;
 
   merge_ireps(SSA_step);
 }
 
 /// spawn a new thread
-void symex_target_equationt::spawn(
-  const exprt &guard,
-  const sourcet &source)
+void symex_target_equationt::spawn(const exprt &guard, const sourcet &source)
 {
   SSA_steps.emplace_back(source, goto_trace_stept::typet::SPAWN);
-  SSA_stept &SSA_step=SSA_steps.back();
-  SSA_step.guard=guard;
+  SSA_stept &SSA_step = SSA_steps.back();
+  SSA_step.guard = guard;
 
   merge_ireps(SSA_step);
 }
@@ -76,8 +73,8 @@ void symex_target_equationt::memory_barrier(
   const sourcet &source)
 {
   SSA_steps.emplace_back(source, goto_trace_stept::typet::MEMORY_BARRIER);
-  SSA_stept &SSA_step=SSA_steps.back();
-  SSA_step.guard=guard;
+  SSA_stept &SSA_step = SSA_steps.back();
+  SSA_step.guard = guard;
 
   merge_ireps(SSA_step);
 }
@@ -89,9 +86,9 @@ void symex_target_equationt::atomic_begin(
   const sourcet &source)
 {
   SSA_steps.emplace_back(source, goto_trace_stept::typet::ATOMIC_BEGIN);
-  SSA_stept &SSA_step=SSA_steps.back();
-  SSA_step.guard=guard;
-  SSA_step.atomic_section_id=atomic_section_id;
+  SSA_stept &SSA_step = SSA_steps.back();
+  SSA_step.guard = guard;
+  SSA_step.atomic_section_id = atomic_section_id;
 
   merge_ireps(SSA_step);
 }
@@ -103,9 +100,9 @@ void symex_target_equationt::atomic_end(
   const sourcet &source)
 {
   SSA_steps.emplace_back(source, goto_trace_stept::typet::ATOMIC_END);
-  SSA_stept &SSA_step=SSA_steps.back();
-  SSA_step.guard=guard;
-  SSA_step.atomic_section_id=atomic_section_id;
+  SSA_stept &SSA_step = SSA_steps.back();
+  SSA_step.guard = guard;
+  SSA_step.atomic_section_id = atomic_section_id;
 
   merge_ireps(SSA_step);
 }
@@ -121,13 +118,14 @@ void symex_target_equationt::assignment(
 {
   PRECONDITION(ssa_lhs.is_not_nil());
 
-  SSA_steps.emplace_back(SSA_assignment_stept{source,
-                                              guard,
-                                              ssa_lhs,
-                                              ssa_full_lhs,
-                                              original_full_lhs,
-                                              ssa_rhs,
-                                              assignment_type});
+  SSA_steps.emplace_back(SSA_assignment_stept{
+    source,
+    guard,
+    ssa_lhs,
+    ssa_full_lhs,
+    original_full_lhs,
+    ssa_rhs,
+    assignment_type});
 
   merge_ireps(SSA_steps.back());
 }
@@ -142,17 +140,17 @@ void symex_target_equationt::decl(
   PRECONDITION(ssa_lhs.is_not_nil());
 
   SSA_steps.emplace_back(source, goto_trace_stept::typet::DECL);
-  SSA_stept &SSA_step=SSA_steps.back();
+  SSA_stept &SSA_step = SSA_steps.back();
 
-  SSA_step.guard=guard;
-  SSA_step.ssa_lhs=ssa_lhs;
+  SSA_step.guard = guard;
+  SSA_step.ssa_lhs = ssa_lhs;
   SSA_step.ssa_full_lhs = initializer;
-  SSA_step.original_full_lhs=ssa_lhs.get_original_expr();
-  SSA_step.hidden=(assignment_type!=assignment_typet::STATE);
+  SSA_step.original_full_lhs = ssa_lhs.get_original_expr();
+  SSA_step.hidden = (assignment_type != assignment_typet::STATE);
 
   // the condition is trivially true, and only
   // there so we see the symbols
-  SSA_step.cond_expr=equal_exprt(SSA_step.ssa_lhs, SSA_step.ssa_lhs);
+  SSA_step.cond_expr = equal_exprt(SSA_step.ssa_lhs, SSA_step.ssa_lhs);
 
   merge_ireps(SSA_step);
 }
@@ -166,14 +164,12 @@ void symex_target_equationt::dead(
   // we currently don't record these
 }
 
-void symex_target_equationt::location(
-  const exprt &guard,
-  const sourcet &source)
+void symex_target_equationt::location(const exprt &guard, const sourcet &source)
 {
   SSA_steps.emplace_back(source, goto_trace_stept::typet::LOCATION);
-  SSA_stept &SSA_step=SSA_steps.back();
+  SSA_stept &SSA_step = SSA_steps.back();
 
-  SSA_step.guard=guard;
+  SSA_step.guard = guard;
 
   merge_ireps(SSA_step);
 }
@@ -186,7 +182,7 @@ void symex_target_equationt::function_call(
   const bool hidden)
 {
   SSA_steps.emplace_back(source, goto_trace_stept::typet::FUNCTION_CALL);
-  SSA_stept &SSA_step=SSA_steps.back();
+  SSA_stept &SSA_step = SSA_steps.back();
 
   SSA_step.guard = guard;
   SSA_step.called_function = function_id;
@@ -204,7 +200,7 @@ void symex_target_equationt::function_return(
   const bool hidden)
 {
   SSA_steps.emplace_back(source, goto_trace_stept::typet::FUNCTION_RETURN);
-  SSA_stept &SSA_step=SSA_steps.back();
+  SSA_stept &SSA_step = SSA_steps.back();
 
   SSA_step.guard = guard;
   SSA_step.called_function = function_id;
@@ -220,12 +216,12 @@ void symex_target_equationt::output(
   const std::list<renamedt<exprt, L2>> &args)
 {
   SSA_steps.emplace_back(source, goto_trace_stept::typet::OUTPUT);
-  SSA_stept &SSA_step=SSA_steps.back();
+  SSA_stept &SSA_step = SSA_steps.back();
 
-  SSA_step.guard=guard;
+  SSA_step.guard = guard;
   for(const auto &arg : args)
     SSA_step.io_args.emplace_back(arg.get());
-  SSA_step.io_id=output_id;
+  SSA_step.io_id = output_id;
 
   merge_ireps(SSA_step);
 }
@@ -238,13 +234,13 @@ void symex_target_equationt::output_fmt(
   const std::list<exprt> &args)
 {
   SSA_steps.emplace_back(source, goto_trace_stept::typet::OUTPUT);
-  SSA_stept &SSA_step=SSA_steps.back();
+  SSA_stept &SSA_step = SSA_steps.back();
 
-  SSA_step.guard=guard;
-  SSA_step.io_args=args;
-  SSA_step.io_id=output_id;
-  SSA_step.formatted=true;
-  SSA_step.format_string=fmt;
+  SSA_step.guard = guard;
+  SSA_step.io_args = args;
+  SSA_step.io_id = output_id;
+  SSA_step.formatted = true;
+  SSA_step.format_string = fmt;
 
   merge_ireps(SSA_step);
 }
@@ -256,11 +252,11 @@ void symex_target_equationt::input(
   const std::list<exprt> &args)
 {
   SSA_steps.emplace_back(source, goto_trace_stept::typet::INPUT);
-  SSA_stept &SSA_step=SSA_steps.back();
+  SSA_stept &SSA_step = SSA_steps.back();
 
-  SSA_step.guard=guard;
-  SSA_step.io_args=args;
-  SSA_step.io_id=input_id;
+  SSA_step.guard = guard;
+  SSA_step.io_args = args;
+  SSA_step.io_id = input_id;
 
   merge_ireps(SSA_step);
 }
@@ -271,10 +267,10 @@ void symex_target_equationt::assumption(
   const sourcet &source)
 {
   SSA_steps.emplace_back(source, goto_trace_stept::typet::ASSUME);
-  SSA_stept &SSA_step=SSA_steps.back();
+  SSA_stept &SSA_step = SSA_steps.back();
 
-  SSA_step.guard=guard;
-  SSA_step.cond_expr=cond;
+  SSA_step.guard = guard;
+  SSA_step.cond_expr = cond;
 
   merge_ireps(SSA_step);
 }
@@ -287,11 +283,11 @@ void symex_target_equationt::assertion(
   const sourcet &source)
 {
   SSA_steps.emplace_back(source, goto_trace_stept::typet::ASSERT);
-  SSA_stept &SSA_step=SSA_steps.back();
+  SSA_stept &SSA_step = SSA_steps.back();
 
-  SSA_step.guard=guard;
-  SSA_step.cond_expr=cond;
-  SSA_step.comment=msg;
+  SSA_step.guard = guard;
+  SSA_step.cond_expr = cond;
+  SSA_step.comment = msg;
   SSA_step.property_id = property_id;
 
   merge_ireps(SSA_step);
@@ -303,9 +299,9 @@ void symex_target_equationt::goto_instruction(
   const sourcet &source)
 {
   SSA_steps.emplace_back(source, goto_trace_stept::typet::GOTO);
-  SSA_stept &SSA_step=SSA_steps.back();
+  SSA_stept &SSA_step = SSA_steps.back();
 
-  SSA_step.guard=guard;
+  SSA_step.guard = guard;
   SSA_step.cond_expr = cond.get();
 
   merge_ireps(SSA_step);
@@ -318,11 +314,11 @@ void symex_target_equationt::constraint(
 {
   // like assumption, but with global effect
   SSA_steps.emplace_back(source, goto_trace_stept::typet::CONSTRAINT);
-  SSA_stept &SSA_step=SSA_steps.back();
+  SSA_stept &SSA_step = SSA_steps.back();
 
-  SSA_step.guard=true_exprt();
-  SSA_step.cond_expr=cond;
-  SSA_step.comment=msg;
+  SSA_step.guard = true_exprt();
+  SSA_step.cond_expr = cond;
+  SSA_step.comment = msg;
 
   merge_ireps(SSA_step);
 }
@@ -330,9 +326,10 @@ void symex_target_equationt::constraint(
 void symex_target_equationt::convert_without_assertions(
   decision_proceduret &decision_procedure)
 {
-  with_solver_hardness(decision_procedure, [&](solver_hardnesst &hardness) {
-    hardness.register_ssa_size(SSA_steps.size());
-  });
+  with_solver_hardness(
+    decision_procedure,
+    [&](solver_hardnesst &hardness)
+    { hardness.register_ssa_size(SSA_steps.size()); });
 
   convert_guards(decision_procedure);
   convert_assignments(decision_procedure);
@@ -362,21 +359,39 @@ void symex_target_equationt::convert_assignments(
   decision_proceduret &decision_procedure)
 {
   std::size_t step_index = 0;
+  std::size_t converted_count = 0;
+  const std::size_t total = SSA_steps.size();
+  auto last_report = std::chrono::steady_clock::now();
+
   for(auto &step : SSA_steps)
   {
     if(step.is_assignment() && !step.ignore && !step.converted)
     {
-      log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) {
-        step.output(mstream);
-        mstream << messaget::eom;
-      });
+      log.conditional_output(
+        log.debug(),
+        [&step](messaget::mstreamt &mstream)
+        {
+          step.output(mstream);
+          mstream << messaget::eom;
+        });
 
       decision_procedure.set_to_true(step.cond_expr);
       step.converted = true;
+      ++converted_count;
       with_solver_hardness(
         decision_procedure, hardness_register_ssa(step_index, step));
     }
     ++step_index;
+
+    // Periodic progress during SSA conversion
+    const auto now = std::chrono::steady_clock::now();
+    if(std::chrono::duration<double>(now - last_report).count() >= 2.0)
+    {
+      last_report = now;
+      log.statistics() << "Converting SSA: " << step_index << "/" << total
+                       << " steps (" << converted_count << " assignments)"
+                       << messaget::eom;
+    }
   }
 }
 
@@ -411,16 +426,19 @@ void symex_target_equationt::convert_guards(
       step.guard_handle = false_exprt();
     else
     {
-      log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) {
-        step.output(mstream);
-        mstream << messaget::eom;
-      });
+      log.conditional_output(
+        log.debug(),
+        [&step](messaget::mstreamt &mstream)
+        {
+          step.output(mstream);
+          mstream << messaget::eom;
+        });
 
       step.guard_handle = decision_procedure.handle(step.guard);
       with_solver_hardness(
-        decision_procedure, [step_index, &step](solver_hardnesst &hardness) {
-          hardness.register_ssa(step_index, step.guard, step.source.pc);
-        });
+        decision_procedure,
+        [step_index, &step](solver_hardnesst &hardness)
+        { hardness.register_ssa(step_index, step.guard, step.source.pc); });
     }
     ++step_index;
   }
@@ -439,7 +457,9 @@ void symex_target_equationt::convert_assumptions(
       else
       {
         log.conditional_output(
-          log.debug(), [&step](messaget::mstreamt &mstream) {
+          log.debug(),
+          [&step](messaget::mstreamt &mstream)
+          {
             step.output(mstream);
             mstream << messaget::eom;
           });
@@ -467,7 +487,9 @@ void symex_target_equationt::convert_goto_instructions(
       else
       {
         log.conditional_output(
-          log.debug(), [&step](messaget::mstreamt &mstream) {
+          log.debug(),
+          [&step](messaget::mstreamt &mstream)
+          {
             step.output(mstream);
             mstream << messaget::eom;
           });
@@ -489,10 +511,13 @@ void symex_target_equationt::convert_constraints(
   {
     if(step.is_constraint() && !step.ignore && !step.converted)
     {
-      log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) {
-        step.output(mstream);
-        mstream << messaget::eom;
-      });
+      log.conditional_output(
+        log.debug(),
+        [&step](messaget::mstreamt &mstream)
+        {
+          step.output(mstream);
+          mstream << messaget::eom;
+        });
 
       decision_procedure.set_to_true(step.cond_expr);
       step.converted = true;
@@ -511,9 +536,9 @@ void symex_target_equationt::convert_assertions(
   // we find out if there is only _one_ assertion,
   // which allows for a simpler formula
 
-  std::size_t number_of_assertions=count_assertions();
+  std::size_t number_of_assertions = count_assertions();
 
-  if(number_of_assertions==0)
+  if(number_of_assertions == 0)
     return;
 
   if(number_of_assertions == 1 && optimized_for_single_assertions)
@@ -553,7 +578,7 @@ void symex_target_equationt::convert_assertions(
   or_exprt::operandst disjuncts;
   disjuncts.reserve(number_of_assertions);
 
-  exprt assumption=true_exprt();
+  exprt assumption = true_exprt();
 
   std::vector<goto_programt::const_targett> involved_steps;
 
@@ -567,23 +592,23 @@ void symex_target_equationt::convert_assertions(
     {
       step.converted = true;
 
-      log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) {
-        step.output(mstream);
-        mstream << messaget::eom;
-      });
+      log.conditional_output(
+        log.debug(),
+        [&step](messaget::mstreamt &mstream)
+        {
+          step.output(mstream);
+          mstream << messaget::eom;
+        });
 
-      implies_exprt implication(
-        assumption,
-        step.cond_expr);
+      implies_exprt implication(assumption, step.cond_expr);
 
       // do the conversion
       step.cond_handle = decision_procedure.handle(implication);
 
       with_solver_hardness(
         decision_procedure,
-        [&involved_steps, &step](solver_hardnesst &hardness) {
-          involved_steps.push_back(step.source.pc);
-        });
+        [&involved_steps, &step](solver_hardnesst &hardness)
+        { involved_steps.push_back(step.source.pc); });
 
       // store disjunct
       disjuncts.push_back(not_exprt(step.cond_handle));
@@ -592,16 +617,15 @@ void symex_target_equationt::convert_assertions(
     {
       // the assumptions have been converted before
       // avoid deep nesting of ID_and expressions
-      if(assumption.id()==ID_and)
+      if(assumption.id() == ID_and)
         assumption.copy_to_operands(step.cond_handle);
       else
         assumption = and_exprt(assumption, step.cond_handle);
 
       with_solver_hardness(
         decision_procedure,
-        [&involved_steps, &step](solver_hardnesst &hardness) {
-          involved_steps.push_back(step.source.pc);
-        });
+        [&involved_steps, &step](solver_hardnesst &hardness)
+        { involved_steps.push_back(step.source.pc); });
     }
   }
 
@@ -625,16 +649,17 @@ void symex_target_equationt::convert_function_calls(
     if(!step.ignore)
     {
       and_exprt::operandst conjuncts;
-      step.converted_function_arguments.reserve(step.ssa_function_arguments.size());
+      step.converted_function_arguments.reserve(
+        step.ssa_function_arguments.size());
 
       for(const auto &arg : step.ssa_function_arguments)
       {
-        if(arg.is_constant() ||
-           arg.id()==ID_string_constant)
+        if(arg.is_constant() || arg.id() == ID_string_constant)
           step.converted_function_arguments.push_back(arg);
         else
         {
-          const irep_idt identifier="symex::args::"+std::to_string(argument_count++);
+          const irep_idt identifier =
+            "symex::args::" + std::to_string(argument_count++);
           symbol_exprt symbol(identifier, arg.type());
 
           equal_exprt eq(arg, symbol);
@@ -666,8 +691,7 @@ void symex_target_equationt::convert_io(decision_proceduret &decision_procedure)
       and_exprt::operandst conjuncts;
       for(const auto &arg : step.io_args)
       {
-        if(arg.is_constant() ||
-           arg.id()==ID_string_constant)
+        if(arg.is_constant() || arg.id() == ID_string_constant)
           step.converted_io_args.push_back(arg);
         else
         {
diff --git a/src/util/memory_info.cpp b/src/util/memory_info.cpp
index 81d206322fe..20783c54a10 100644
--- a/src/util/memory_info.cpp
+++ b/src/util/memory_info.cpp
@@ -81,3 +81,32 @@ void memory_info(std::ostream &out)
   out << "  maximum resident set size [bytes]: " << r_usage.ru_maxrss << '\n';
 #endif
 }
+
+std::size_t peak_memory_bytes()
+{
+#ifdef __GLIBC__
+  struct mallinfo m = mallinfo();
+  return m.uordblks + m.hblkhd;
+#elif defined(_WIN32)
+  PROCESS_MEMORY_COUNTERS pmc;
+  if(GetProcessMemoryInfo(GetCurrentProcess(), &pmc, sizeof(pmc)))
+    return pmc.PeakWorkingSetSize;
+  return 0;
+#elif defined(__APPLE__)
+  struct task_basic_info t_info;
+  mach_msg_type_number_t t_info_count = TASK_BASIC_INFO_COUNT;
+  if(
+    task_info(
+      current_task(), TASK_BASIC_INFO, (task_info_t)&t_info, &t_info_count) ==
+    KERN_SUCCESS)
+  {
+    return t_info.virtual_size;
+  }
+  return 0;
+#else
+  struct rusage r_usage;
+  if(getrusage(RUSAGE_SELF, &r_usage) == 0)
+    return static_cast<std::size_t>(r_usage.ru_maxrss) * 1024;
+  return 0;
+#endif
+}
diff --git a/src/util/memory_info.h b/src/util/memory_info.h
index 7364e0e2bd6..b4e87706c85 100644
--- a/src/util/memory_info.h
+++ b/src/util/memory_info.h
@@ -10,8 +10,12 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_UTIL_MEMORY_INFO_H
 #define CPROVER_UTIL_MEMORY_INFO_H
 
+#include <cstddef>
 #include <iosfwd>
 
 void memory_info(std::ostream &);
 
+/// Return current peak resident set size in bytes, or 0 if unavailable.
+std::size_t peak_memory_bytes();
+
 #endif // CPROVER_UTIL_MEMORY_INFO_H