" --paths [strategy] explore paths one at a time\n" \
" --show-symex-strategies list strategies for use with --paths\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 (cannot be\n" \
" used with --cover or --partial-loops)\n" \
" --partial-loops permit paths with partial loops\n" \
" --no-self-loops-to-assumptions\n" \
" do not simplify while(1){} to assume(0)\n" \
" --no-pretty-names do not simplify identifiers\n" \
" --graphml-witness filename write the witness in GraphML format to " \
"filename\n"