Implement documentation roadmap and fix no-op asserts in examples

[shaobo-he]

Summary

Implements the documentation roadmap in #828 by consolidating and expanding
SMACK's user guidance in the repository, updated and checked against the current
command-line interface and verifier behavior.

Closes #828.

What changed

User documentation

• Expanded docs/running.md into an entry-level guide covering assertions,
  assumptions, nondeterministic inputs, result interpretation, property checks,
  multi-file programs, prelinked bitcode, and back-end selection.
• Added docs/command-line-options.md as a task-oriented guide to the options
  users most commonly need.
• Added docs/build-workflows.md for source, multi-file, saved-artifact,
  prelinked-bitcode, and Makefile workflows.
• Added docs/advanced.md for modeling, experimental contracts, inline Boogie,
  uninterpreted functions, initialization hooks, and trace annotations.
• Added docs/troubleshooting.md for common assertion, modeling, memory,
  toolchain, timeout, and generated-artifact problems.
• Updated the README table of contents and cross-links, while preserving the
  legacy misspelled loops-and-recusive-functions blog anchor.

Correctness clarifications

• Documented that an explicit --check list replaces the default assertions
  property; examples select assertions explicitly when combining checks.
• Corrected the loop example to require --unroll 4 and clarified that
  --fail-on-loop-exit reports reachable normal exits, not paths truncated by
  bound exhaustion.
• Described successful results and counterexample traces as bounded and
  model-relative, including limitations of approximate integer, bitwise, and
  floating-point encodings.
• Clarified wrapped-integer versus bit-vector use, precise valid-free
  semantics, and the scope of --checked-functions (including the shared
  valid-free model exception).
• Marked source-level contracts as experimental and documented the current
  return-value limitation.
• Documented all four result kinds: no errors, error, timeout, and unknown.

Examples and LLVM workflows

• Added <assert.h> to the introductory C examples so their assertions are
  translated into verifier assertions rather than unresolved function calls.
• Updated manual bitcode instructions to use the LLVM major version configured
  for this checkout (clang-14 and llvm-link-14).
• Documented that raw/prelinked bitcode must be compiled with
  -fsanitize=signed-integer-overflow,shift before SMACK can check integer
  overflow; selecting the property after compilation is too late.
• Updated examples/simple-project/Makefile to use the matching LLVM tools,
  preserve analyzable -O0 IR, and include overflow instrumentation.

No production verifier implementation is changed; the non-documentation edits
are limited to the two example includes and the example Makefile.

Testing

• git diff --check
• Verified relative Markdown links, internal fragments, legacy anchors, and
  balanced code fences.
• Exercised --check replacement and combined-property behavior.
• Confirmed the loop fixture is missed at bound 3 and found at bound 4, and that
  --fail-on-loop-exit reports the injected normal-exit check at bound 4.
• Confirmed raw bitcode misses signed overflow without Clang sanitizer
  instrumentation and reports it after compilation with
  -fsanitize=signed-integer-overflow,shift.
• Built the copied multi-file example with clang-14/llvm-link-14 and verified
  the resulting bitcode with assertion and overflow checks enabled.
• Exercised the memory-safety, bit-vector, modular-contract, multi-source, and
  --checked-functions examples.