Source code:
Result:

Additonal options:

Output options
--parse-tree-onlyonly show parse tree
--parse-tree-tooshow parse tree and verify
--symbol-table-onlyonly show symbol table
--symbol-table-tooshow symbol table and verify
--goto-functions-onlyonly show goto program
--goto-functions-tooshow goto program and verify
--program-onlyonly show program expression
--program-tooshow program expression and verify
--ssa-symbol-tableshow symbol table along with SSA
--ssa-guardsprint SSA's guards, if any
--ssa-no-locationdo not print the SSA's original location
--ssa-no-sliceddo not print the sliced SSAs
--ssa-full-namesprint SSAs with full variable names
--smt-formula-onlyonly show SMT formula (not supported by all solvers)
--smt-formula-tooshow SMT formula (not supported by all solvers) and verify
--smt-modelshow SMT model (not supported by all solvers), if the formula is SAT
Trace options
--quietdo not print unwinding information during symbolic execution
--symex-traceprint instructions during symbolic execution
--symex-ssa-traceprint generated SSA during symbolic execution
--ssa-traceprint SSA during SMT encoding
--ssa-smt-traceprint generated SMT during SMT encoding
--show-goto-value-setsshow value-set analysis for the goto functions
--show-symex-value-setsshow value-set analysis during symbolic execution
Front-end options
--preprocessstop after preprocessing
--no-inliningdisable inlining function calls
--full-inliningperform full inlining of function calls
--all-claimskeep all claims
--show-loopsshow the loops in the program
--show-claimsonly show claims
--show-vccshow the verification conditions
--document-subgoalsgenerate subgoals documentation
--no-archdon't set up an architecture
--no-librarydisable built-in abstract C library
--little-endianallow little-endian word-byte conversions
--big-endianallow big-endian word-byte conversions
--16, --32, --64 set width of machine word (default is 64)
--unsigned-charmake "char" unsigned by default
--versionshow current ESBMC version and exit
--old-frontendparse source files using our old frontend (deprecated)
--result-onlydo not print the counter-example
--i386-macosset MACOS/I386 architecture
--ppc-macosset PPC/I386 architecture
--i386-linuxset Linux/I386 architecture (default)
--i386-win32set Windows/I386 architecture
BMC options
--function set main function name
--claim nronly check specific claim
--depth nr limit search depth
--unwind nr unwind nr times
--unwindset nr unwind given loop nr times
--no-unwinding-assertionsdo not generate unwinding assertions
--partial-loopspermit paths with partial loops
--unroll-loopsunwind all loops by the value defined by the --unwind option
--no-slicedo not remove unused equations
--extended-try-analysischeck all the try block, even when an exception is thrown
Incremental BMC
--falsificationincremental loop unwinding for bug searching
--incremental-bmcincremental loop unwinding verification
--terminationincremental loop unwinding assertion verification
--k-step nr set k increment (default is 1)
--max-k-step nr set max number of iteration (default is 50)
--unlimited-k-stepsset max number of iteration to UINT_MAX
Solver configuration
--list-solverslist available solvers and exit
--boolectoruse Boolector (default)
--bvuse solver with bit-vector arithmetic
--iruse solver with integer/real arithmetic
--smtlibuse SMT lib format
--fixedbvencode floating-point as fixed bit-vectors
--floatbvencode floating-point using the SMT floating-point theory (default)
--fp2bvencode floating-point as bit-vectors.
(default for solvers that don't support the SMT floating-point theory)
--tuple-node-flattenerencode tuples using our tuple to node API
--tuple-sym-flattenerencode tuples using our tuple to symbol API
--array-flattenerencode arrays using our array API
Incremental SMT solving
--smt-during-symexenable incremental SMT solving (experimental)
--smt-thread-guardcall the solver during thread exploration (experimental)
--smt-symex-guardcall the solver during symbolic execution (experimental)
Property checking
--no-assertionsignore assertions
--no-bounds-checkdo not do array bounds check
--no-div-by-zero-checkdo not do division by zero check
--no-pointer-checkdo not do pointer check
--no-align-checkdo not check pointer alignment
--memory-leak-checkenable memory leak check check
--nan-checkcheck floating-point for NaN
--overflow-checkenable arithmetic over- and underflow check
--deadlock-checkenable global and local deadlock check with mutex
--data-races-checkenable data races check
--lock-order-checkenable for lock acquisition ordering check
--atomicity-checkenable atomicity check at visible assignments
--error-label labelcheck if label is unreachable
--force-malloc-successdo not check for malloc/new failure
K-induction
--base-casecheck the base case
--forward-conditioncheck the forward condition
--inductive-stepcheck the inductive step
--k-inductionprove by k-induction
--k-induction-parallelprove by k-induction, running each step on a separate process
--k-step nr set k increment (default is 1)
--max-k-step nrset max number of iteration (default is 50)
--unlimited-k-stepsset max number of iteration to UINT_MAX
--show-cexprint the counter-example produced by the inductive step
Scheduling approaches
--scheduleuse schedule recording approach
--round-robinuse the round robin scheduling approach
--time-slice nrset the time slice of the round robin algorithm (default is 1)
Concurrency checking
--context-bound nrlimit number of context switches for each thread
--state-hashingenable state-hashing, prunes duplicate states
--no-pordo not do partial order reduction
--all-runscheck all interleavings, even if a bug was already found
Miscellaneous options
--memstatsprint memory usage statistics
--no-simplifydo not simplify any expression
--enable-core-dumpdo not disable core dump output
--interval-analysisenable interval analysis and add assumes to the program