diff --git a/doc/man/cbmc.1 b/doc/man/cbmc.1
index c6f77e21d96..622be34c75a 100644
--- a/doc/man/cbmc.1
+++ b/doc/man/cbmc.1
@@ -1,7 +1,4 @@
-.\" Process this file with
-.\" groff -man -Tascii cbmc.1
-.\"
-.TH CBMC 1 "JUNE 2014" "cbmc-4.7" "User Manual"
+.TH CBMC "1" "June 2022" "cbmc-5.59.0" "User Commands"
 .SH NAME
 cbmc \- Bounded Model Checker for C/C++ and Java programs
 .SH SYNOPSIS
@@ -21,7 +18,7 @@ Only the most useful options are listed here; see below for the remainder.
 \fBcbmc\fR generates traces that demonstrate how an assertion can be
 violated, or proves that the assertion cannot be violated within a given
 number of loop iterations.  CBMC can read C/C++ source-code directly, or a
-goto-binary generated by goto-cc.  Java programs are given as class or JAR files. 
+GOTO binary generated by goto-cc.  Java programs are given as class or JAR files.
 Without any further options, cbmc checks all properties (automatically
 generated or user-specified) found in the program.  If any of the
 properties can be violated, a counterexample is printed and the analysis is
@@ -29,156 +26,425 @@ aborted.  The analysis can be restricted to a particular property with the
 \-\-property option.  The verification result for all properties can be obtained by
 means of the \-\-all-properties option.
 
-\fBgoto-cc\fR reads source code, and generates a goto-binary. Its
+\fBgoto-cc\fR(1) reads source code, and generates a GOTO binary. Its
 command-line interface is designed to mimic that of
 .BR gcc (1).
-Note in particular that \fBgoto-cc\fR distinguishes between compiling
-and linking phases, just as gcc does. \fBcbmc\fR expects a goto-binary
+Note in particular that \fBgoto-cc\fR(1) distinguishes between compiling
+and linking phases, just as gcc does. \fBcbmc\fR expects a GOTO binary
 for which linking has been completed.
 
-\fBgoto-instrument\fR reads a goto-binary, performs a given program
-transformation, and then writes the resulting program as goto-binary on
+\fBgoto-instrument\fR(1) reads a GOTO binary, performs a given program
+transformation, and then writes the resulting program as GOTO binary on
 disc.
 
-The usual flow is to (1) translate source into a goto-binary using
+The usual flow is to (1) translate source into a GOTO binary using
 goto-cc, then (2) perform instrumentation with goto-instrument, and
 finally (3) perform the analysis with cbmc.
 .SH OPTIONS
-.SS "FRONTEND OPTIONS (cbmc and goto-cc)"
-.IP "-I path"
-Set include path (C/C++)
-.IP "-D macro"
-Define preprocessor macro (C/C++)
-.IP --preprocess
-Stop after preprocessing
-.IP --show-symbol-table
-Show symbol table
-.IP --show-goto-functions
-Show goto program
-
-.SS "ARCHITECTURAL OPTIONS (cbmc and goto-cc)"
-\fBcbmc\fR by default uses architectural settings that match those of the
-machine \fBcbmc\fR is executed on, i.e., the settings below are only needed
-when verifying software that is meant to run on a different architecture
-or OS. \fBgoto-cc\fR generates a goto-binary for a particular architecture,
-i.e., the architecture cannot be changed after the goto-binary is generated.
-.IP "--16, --32, --64"
-Set width of int
-.IP "--LP64, --ILP64, --LLP64, --ILP32, --LP32"
-Set width of int, long and pointers
-.IP --little-endian
-Allow little-endian word-byte conversions
-.IP --big-endian
-Allow big-endian word-byte conversions
-.IP --unsigned-char
-Make "char" unsigned by default
-.IP --arch
-Set target architecture
-.IP --os
-Set target operating system
-.IP --no-library
-Disable built-in abstract C library
-.IP "--round-to-nearest, --round-to-plus-inf, --round-to-minus-inf, --round-to-zero"
-IEEE floating point rounding mode to use when the program begins (default is round to
-nearest). The program under verification can override this setting, e.g., with
-.BR fesetround (3).
-.SS "PROGRAM INSTRUMENTATION OPTIONS (cbmc and goto-instrument)"
-Both \fBcbmc\fR and \fBgoto-instrument\fR can generate assertions that
-catch specific common errors, as listed below.
-.IP --bounds-check
-Enable array bounds checks
-.IP --div-by-zero-check
-Enable division by zero checks
-.IP --pointer-check
-Enable pointer checks
-.IP --signed-overflow-check
-Enable arithmetic over- and underflow checks for signed integer arithmetic
-.IP --unsigned-overflow-check
-Enable arithmetic over- and underflow checks for unsigned integer arithmetic
-.IP --nan-check
-Check floating-point computations for NaN
-.IP --no-assertions
-Ignore user-provided assertions
-.IP --no-assumptions
-Ignore user-provided assumptions
-.IP "--error-label label"
-Check that the given label is unreachable
-.SS "PROGRAM INSTRUMENTATION OPTIONS (goto-instrument only)"
-\fBgoto-instrument\fR supports further, more complex, program
-transformations.
-.IP --nondet-volatile
-Makes reads from volatile variables non-deterministic
-.IP "--isr function"
-Instruments an interrupt service routine with the given name
-.IP --mmio
-Instruments memory-mapped I/O
-.IP --nondet-static
-Variables with static lifetime are initialized non-deterministically
-.IP --dump-c
-Output ANSI-C source code instead of a goto binary.
-.SS "BMC OPTIONS (cbmc)"
-.IP --all-properties
-Report status of all properties
-.IP --show-properties
-Only show properties
-.IP --show-loops
-Show the loops in the program
-.IP --cover-assertions
-Check which assertions are reachable
-.IP "--function name"
-Set main function name
-.IP "--property id"
-Only check specific property with given identifier
-.IP --program-only
-Only show program expression
-.IP "--depth nr "
-Limit search depth
-.IP "--unwind nr "
-Unwind loops nr times
-.IP "--unwindset [T:]L:B,..."
-Unwind loop L with a bound of B, optionally restricted to thread T. Use
-\-\-show\-loops to get the loop IDs. Thread numbers are set as follows: The
-initial thread has index 0, and threads are consecutively numbered in program
-order of threads being spawned.  The`--unwindset` option can be given multiple
-times.
-.IP --show-vcc
-Show the verification conditions
-.IP --slice-formula
-Remove assignments unrelated to property
-.IP --no-unwinding-assertions
-Do not generate unwinding assertions
-.SS "BACKEND OPTIONS (cbmc)"
-.IP --dimacs
-Generate CNF in DIMACS format for use by external SAT solvers
-.IP --beautify-greedy
-Beautify the counterexample (greedy heuristic)
-.IP --smt2
-Output subgoals in SMT2 syntax
-.IP --boolector
-Use Boolector (experimental)
-.IP --mathsat
-Use MathSAT (experimental)
-.IP --cvc3
-Use CVC3 (experimental)
-.IP --cvc4
-Use CVC4 (experimental)
-.IP --yices
-Use Yices (experimental)
-.IP --z3
-Use Z3 (experimental)
-.IP --refine
-Use refinement procedure (experimental)
-.IP "--outfile filename"
-Output formula to given file
-.IP --arrays-uf-never
-Never turn arrays into uninterpreted functions
-.IP --arrays-uf-always
-Always turn arrays into uninterpreted functions
-.IP "--incremental-smt2-solver <cmd>"
-Use the incremental SMT backend where <cmd> is the command to invoke the SMT
+.SS "Analysis options:"
+.TP
+\fB\-\-show\-properties\fR
+show the properties, but don't run analysis
+.TP
+\fB\-\-symex\-coverage\-report\fR f
+generate a Cobertura XML coverage report in f
+.TP
+\fB\-\-property\fR id
+only check one specific property
+.TP
+\fB\-\-trace\fR
+give a counterexample trace for failed properties
+.TP
+\fB\-\-stop\-on\-fail\fR
+stop analysis once a failed property is detected
+(implies \fB\-\-trace\fR)
+.TP
+\fB\-\-localize\-faults\fR
+localize faults (experimental)
+.SS "C/C++ frontend options:"
+.TP
+\fB\-\-preprocess\fR
+stop after preprocessing
+.TP
+\fB\-\-test\-preprocessor\fR
+stop after preprocessing, discard output
+.TP
+\fB\-I\fR path
+set include path (C/C++)
+.TP
+\fB\-\-include\fR file
+set include file (C/C++)
+.TP
+\fB\-D\fR macro
+define preprocessor macro (C/C++)
+.TP
+\fB\-\-c89\fR, \fB\-\-c99\fR, \fB\-\-c11\fR
+set C language standard (default: c11)
+.TP
+\fB\-\-cpp98\fR, \fB\-\-cpp03\fR, \fB\-\-cpp11\fR
+set C++ language standard (default: cpp98)
+.TP
+\fB\-\-unsigned\-char\fR
+make "char" unsigned by default
+.TP
+\fB\-\-round\-to\-nearest\fR, \fB\-\-round\-to\-even\fR
+rounding towards nearest even (default)
+.TP
+\fB\-\-round\-to\-plus\-inf\fR
+rounding towards plus infinity
+.TP
+\fB\-\-round\-to\-minus\-inf\fR
+rounding towards minus infinity
+.TP
+\fB\-\-round\-to\-zero\fR
+rounding towards zero
+.TP
+\fB\-\-no\-library\fR
+disable built\-in abstract C library
+.TP
+\fB\-\-max\-nondet\-tree\-depth\fR N
+limit size of nondet (e.g. input) object tree;
+at level N pointers are set to null
+.TP
+\fB\-\-min\-null\-tree\-depth\fR N
+minimum level at which a pointer can first be
+NULL in a recursively nondet initialized struct
+.TP
+\fB\-\-function\fR name
+set main function name
+.SS "Platform options:"
+.TP
+\fB\-\-arch\fR \fIarch\fR
+Set analysis architecture, which defaults to the host architecture. Use one of:
+\fBalpha\fR, \fBarm\fR, \fBarm64\fR, \fBarmel\fR, \fBarmhf\fR, \fBhppa\fR, \fBi386\fR, \fBia64\fR,
+\fBmips\fR, \fBmips64\fR, \fBmips64el\fR, \fBmipsel\fR, \fBmipsn32\fR,
+\fBmipsn32el\fR, \fBpowerpc\fR, \fBppc64\fR, \fBppc64le\fR, \fBriscv64\fR, \fBs390\fR,
+\fBs390x\fR, \fBsh4\fR, \fBsparc\fR, \fBsparc64\fR, \fBv850\fR, \fBx32\fR, \fBx86_64\fR, or
+\fBnone\fR.
+.TP
+\fB\-\-os\fR \fIos\fR
+Set analysis operating system, which defaults to the host operating system. Use
+one of: \fBfreebsd\fR, \fBlinux\fR, \fBmacos\fR, \fBsolaris\fR, or
+\fBwindows\fR.
+.TP
+\fB\-\-i386\-linux\fR, \fB\-\-i386\-win32\fR, \fB\-\-i386\-macos\fR, \fB\-\-ppc\-macos\fR, \fB\-\-win32\fR, \fB\-\-winx64\fR
+Set analysis architecture and operating system.
+.TP
+\fB\-\-LP64\fR, \fB\-\-ILP64\fR, \fB\-\-LLP64\fR, \fB\-\-ILP32\fR, \fB\-\-LP32\fR
+Set width of int, long and pointers, but don't override default architecture and
+operating system.
+.TP
+\fB\-\-16\fR, \fB\-\-32\fR, \fB\-\-64\fR
+Equivalent to \fB\-\-LP32\fR, \fB\-\-ILP32\fR, \fB\-\-LP64\fR (on Windows:
+\fB\-\-LLP64\fR).
+.TP
+\fB\-\-little\-endian\fR
+allow little\-endian word\-byte conversions
+.TP
+\fB\-\-big\-endian\fR
+allow big\-endian word\-byte conversions
+.TP
+\fB\-\-gcc\fR
+use GCC as preprocessor
+.SS "Program representations:"
+.TP
+\fB\-\-show\-parse\-tree\fR
+show parse tree
+.TP
+\fB\-\-show\-symbol\-table\fR
+show loaded symbol table
+.TP
+\fB\-\-show\-goto\-functions\fR
+show loaded goto program
+.TP
+\fB\-\-list\-goto\-functions\fR
+list loaded goto functions
+.TP
+\fB\-\-validate\-goto\-model\fR
+enable additional well\-formedness checks on the
+goto program
+.TP
+\fB\-\-validate\-ssa\-equation\fR
+enable additional well\-formedness checks on the
+SSA representation
+.SS "Program instrumentation options:"
+.TP
+\fB\-\-bounds\-check\fR
+enable array bounds checks
+.TP
+\fB\-\-pointer\-check\fR
+enable pointer checks
+.TP
+\fB\-\-memory\-leak\-check\fR
+enable memory leak checks
+.TP
+\fB\-\-div\-by\-zero\-check\fR
+enable division by zero checks
+.TP
+\fB\-\-signed\-overflow\-check\fR
+enable signed arithmetic over\- and underflow checks
+.TP
+\fB\-\-unsigned\-overflow\-check\fR
+enable arithmetic over\- and underflow checks
+.TP
+\fB\-\-pointer\-overflow\-check\fR
+enable pointer arithmetic over\- and underflow checks
+.TP
+\fB\-\-conversion\-check\fR
+check whether values can be represented after type cast
+.TP
+\fB\-\-undefined\-shift\-check\fR
+check shift greater than bit\-width
+.TP
+\fB\-\-float\-overflow\-check\fR
+check floating\-point for +/\-Inf
+.TP
+\fB\-\-nan\-check\fR
+check floating\-point for NaN
+.TP
+\fB\-\-enum\-range\-check\fR
+checks that all enum type expressions have values in the enum range
+.TP
+\fB\-\-pointer\-primitive\-check\fR
+checks that all pointers in pointer primitives are valid or null
+.TP
+\fB\-\-retain\-trivial\-checks\fR
+include checks that are trivially true
+.TP
+\fB\-\-error\-label\fR label
+check that label is unreachable
+.TP
+\fB\-\-no\-built\-in\-assertions\fR
+ignore assertions in built\-in library
+.TP
+\fB\-\-no\-assertions\fR
+ignore user assertions
+.TP
+\fB\-\-no\-assumptions\fR
+ignore user assumptions
+.TP
+\fB\-\-assert\-to\-assume\fR
+convert user assertions to assumptions
+.TP
+\fB\-\-cover\fR CC
+create test\-suite with coverage criterion CC,
+where CC is one of assertion[s], assume[s],
+branch[es], condition[s], cover, decision[s],
+location[s], or mcdc
+.TP
+\fB\-\-cover\-failed\-assertions\fR
+do not stop coverage checking at failed assertions
+(this is the default for \fB\-\-cover\fR assertions)
+.TP
+\fB\-\-show\-test\-suite\fR
+print test suite for coverage criterion (requires \fB\-\-cover\fR)
+.TP
+\fB\-\-mm\fR MM
+memory consistency model for concurrent programs (default: sc)
+.TP
+\fB\-\-malloc\-may\-fail\fR
+allow malloc calls to return a null pointer
+.TP
+\fB\-\-malloc\-fail\-assert\fR
+set malloc failure mode to assert\-then\-assume
+.TP
+\fB\-\-malloc\-fail\-null\fR
+set malloc failure mode to return null
+.TP
+\fB\-\-string\-abstraction\fR
+track C string lengths and zero\-termination
+.TP
+\fB\-\-fp\-reachability\-slice\fR f
+remove instructions that cannot appear on a trace
+that visits all given functions. The list of
+functions has to be given as a comma separated
+list f.
+.TP
+\fB\-\-reachability\-slice\fR
+remove instructions that cannot appear on a trace
+from entry point to a property
+.TP
+\fB\-\-reachability\-slice\-fb\fR
+remove instructions that cannot appear on a trace
+from entry point through a property
+.TP
+\fB\-\-full\-slice\fR
+run full slicer (experimental)
+.TP
+\fB\-\-drop\-unused\-functions\fR
+drop functions trivially unreachable from main function
+.TP
+\fB\-\-havoc\-undefined\-functions\fR
+for any function that has no body, assign non\-deterministic values to
+any parameters passed as non\-const pointers and the return value
+.SS "Semantic transformations:"
+.TP
+\fB\-\-nondet\-static\fR
+add nondeterministic initialization of variables with static lifetime
+.SS "BMC options:"
+.TP
+\fB\-\-paths\fR [strategy]
+explore paths one at a time
+.TP
+\fB\-\-show\-symex\-strategies\fR
+list strategies for use with \fB\-\-paths\fR
+.TP
+\fB\-\-show\-goto\-symex\-steps\fR
+show which steps symex travels, includes
+diagnostic information
+.TP
+\fB\-\-show\-points\-to\-sets\fR
+show points\-to sets for
+pointer dereference. Requires \fB\-\-json\-ui\fR.
+.TP
+\fB\-\-program\-only\fR
+only show program expression
+.TP
+\fB\-\-show\-byte\-ops\fR
+show all byte extracts and updates
+.TP
+\fB\-\-depth\fR nr
+limit search depth
+.TP
+\fB\-\-max\-field\-sensitivity\-array\-size\fR M
+maximum size M of arrays for which field
+sensitivity will be applied to array,
+the default is 64
+.TP
+\fB\-\-no\-array\-field\-sensitivity\fR
+deactivate field sensitivity for arrays, this is
+equivalent to setting the maximum field
+sensitivity size for arrays to 0
+.TP
+\fB\-\-show\-loops\fR
+show the loops in the program
+.TP
+\fB\-\-unwind\fR nr
+unwind nr times
+.TP
+\fB\-\-unwindset\fR [T:]L:B,...
+unwind loop L with a bound of B
+(optionally restricted to thread T)
+(use \fB\-\-show\-loops\fR to get the loop IDs)
+.TP
+\fB\-\-incremental\-loop\fR L
+check properties after each unwinding
+of loop L
+(use \fB\-\-show\-loops\fR to get the loop IDs)
+.TP
+\fB\-\-unwind\-min\fR nr
+start incremental\-loop after nr unwindings
+but before solving that iteration. If for
+example it is 1, then the loop will be
+unwound once, and immediately checked.
+Note: this means for min\-unwind 1 or
+0 all properties are checked.
+.TP
+\fB\-\-unwind\-max\fR nr
+stop incremental\-loop after nr unwindings
+.TP
+\fB\-\-ignore\-properties\-before\-unwind\-min\fR
+do not check properties before unwind\-min
+when using incremental\-loop
+.TP
+\fB\-\-show\-vcc\fR
+show the verification conditions
+.TP
+\fB\-\-slice\-formula\fR
+remove assignments unrelated to property
+.TP
+\fB\-\-unwinding\-assertions\fR
+generate unwinding assertions (cannot be
+used with \fB\-\-cover\fR)
+.TP
+\fB\-\-partial\-loops\fR
+permit paths with partial loops
+.TP
+\fB\-\-no\-self\-loops\-to\-assumptions\fR
+do not simplify while(1){} to assume(0)
+.TP
+\fB\-\-symex\-complexity\-limit\fR N
+how complex (N) a path can become before
+symex abandons it. Currently uses guard
+size to calculate complexity.
+.TP
+\fB\-\-symex\-complexity\-failed\-child\-loops\-limit\fR N
+how many child branches (N) in an
+iteration are allowed to fail due to
+complexity violations before the loop
+gets blacklisted
+.TP
+\fB\-\-graphml\-witness\fR filename
+write the witness in GraphML format to filename
+.TP
+\fB\-\-symex\-cache\-dereferences\fR
+enable caching of repeated dereferences
+.SS "Backend options:"
+.TP
+\fB\-\-object\-bits\fR n
+number of bits used for object addresses
+.TP
+\fB\-\-external\-sat\-solver\fR cmd
+command to invoke SAT solver process
+.TP
+\fB\-\-no\-sat\-preprocessor\fR
+disable the SAT solver's simplifier
+.TP
+\fB\-\-dimacs\fR
+generate CNF in DIMACS format
+.TP
+\fB\-\-beautify\fR
+beautify the counterexample
+(greedy heuristic)
+.TP
+\fB\-\-smt1\fR
+use default SMT1 solver (obsolete)
+.TP
+\fB\-\-smt2\fR
+use default SMT2 solver (Z3)
+.TP
+\fB\-\-boolector\fR
+use Boolector
+.TP
+\fB\-\-cprover\-smt2\fR
+use CPROVER SMT2 solver
+.TP
+\fB\-\-cvc3\fR
+use CVC3
+.TP
+\fB\-\-cvc4\fR
+use CVC4
+.TP
+\fB\-\-mathsat\fR
+use MathSAT
+.TP
+\fB\-\-yices\fR
+use Yices
+.TP
+\fB\-\-z3\fR
+use Z3
+.TP
+\fB\-\-fpa\fR
+use theory of floating\-point arithmetic
+.TP
+\fB\-\-refine\fR
+use refinement procedure (experimental)
+.TP
+\fB\-\-refine\-arrays\fR
+use refinement for arrays only
+.TP
+\fB\-\-refine\-arithmetic\fR
+refinement of arithmetic expressions only
+.TP
+\fB\-\-max\-node\-refinement\fR
+maximum refinement iterations for
+arithmetic expressions
+.TP
+\fB\-\-incremental\-smt2\-solver\fR \fIcmd\fR
+Use the incremental SMT backend where \fIcmd\fR is the command to invoke the SMT
 solver of choice.
 .br
-Examples invocations:
+Example invocations:
 .br
   --incremental-smt2-solver 'z3 -smt2 -in' (use the Z3 solver).
 .br
@@ -192,12 +458,81 @@ The SMT solver should accept incremental SMTlib v2.6 formatted input from the st
 .br
 The SMT solver should support the QF_AUFBV logic.
 .br
-The flag --slice-formula should be added to remove some not-yet supported features.
+The flag \fB\-\-slice\-formula\fR should be added to remove some not-yet supported features.
+.TP
+\fB\-\-outfile\fR filename
+output formula to given file
+.TP
+\fB\-\-write\-solver\-stats\-to\fR json\-file
+collect the solver query complexity
+.TP
+\fB\-\-refine\-strings\fR
+use string refinement (experimental)
+.TP
+\fB\-\-string\-printable\fR
+restrict to printable strings (experimental)
+.TP
+\fB\-\-arrays\-uf\-never\fR
+never turn arrays into uninterpreted functions
+.TP
+\fB\-\-arrays\-uf\-always\fR
+always turn arrays into uninterpreted functions
+.TP
+\fB\-\-show\-array\-constraints\fR
+show array theory constraints added
+during post processing.
+Requires \fB\-\-json\-ui\fR.
+.SS "User-interface options:"
+.TP
+\fB\-\-xml\-ui\fR
+use XML\-formatted output
+.TP
+\fB\-\-xml\-interface\fR
+bi\-directional XML interface
+.TP
+\fB\-\-json\-ui\fR
+use JSON\-formatted output
+.TP
+\fB\-\-json\-interface\fR
+bi\-directional JSON interface
+.TP
+\fB\-\-trace\-json\-extended\fR
+add rawLhs property to trace
+.TP
+\fB\-\-trace\-show\-function\-calls\fR
+show function calls in plain trace
+.TP
+\fB\-\-trace\-show\-code\fR
+show original code in plain trace
+.TP
+\fB\-\-trace\-hex\fR
+represent plain trace values in hex
+.TP
+\fB\-\-compact\-trace\fR
+give a compact trace
+.TP
+\fB\-\-stack\-trace\fR
+give a stack trace only
+.TP
+\fB\-\-flush\fR
+flush every line of output
+.TP
+\fB\-\-verbosity\fR #
+verbosity level
+.TP
+\fB\-\-timestamp\fR [\fBmonotonic\fR|\fBwall\fR]
+Print microsecond\-precision timestamps.  \fBmonotonic\fR: stamps increase
+monotonically.  \fBwall\fR: ISO\-8601 wall clock timestamps.
 .SH ENVIRONMENT
 All tools honor the TMPDIR environment variable when generating temporary
 files and directories. Furthermore note that
-the preprocessor used by CBMC will use environment variables to locate
-header files. GOTO-CC aims to accept all environment variables that GCC
-does.
+the preprocessor used by \fBcbmc\R will use environment variables to locate
+header files.
+.SH BUGS
+If you encounter a problem please create an issue at
+.B https://github.com/diffblue/cbmc/issues
+.SH SEE ALSO
+.BR goto-cc (1),
+.BR goto-instrument (1)
 .SH COPYRIGHT
 2001-2016, Daniel Kroening, Edmund Clarke