Improve “Running Smack” documentation

[michael-emmi]

The documentation should address the most basic concerns about running Smack, including loops and (bounded) unrolling, assertions, assumptions, and nondeterministic inputs.

One approach would be to start with a very simple example, e.g., a tiny straight-line program with a single assertion, and incrementally make it more interesting by adding a loop, and nondeterministic input.

While the current example in smack/docs/running.md does highlight some of the complex features that Smack can deal with, it does not deal with the basic issues about running Smack, e.g., those mentioned above. If we want to keep this example — although not clear it should go here — it should at the very least appear after the basic operating instructions.