Update user manual

Simplify calls to JBMC

Author: peterschrammel

doc/cprover-manual/jbmc-user-manual.md

@@ -123,7 +123,7 @@ depends on an input):
 To limit the number of times the for-loop is unwound, we use the `--unwind N`
 options, in which case the following call to JBMC:
 ```
-$ jbmc tutorial.ExampleUnwind --function tutorial.ExampleUnwind.isPrime --unwind 10
+$ jbmc tutorial.ExampleUnwind.isPrime --unwind 10
 ```
 will terminate correctly. In this case, we will see `VERIFICATION SUCCESSFUL`,
 as no automatic assertions are violated.
@@ -139,7 +139,7 @@ JBMC will try to refute. On line 7, we check the assertion that all odd
 numbers greater than 1 are prime. To be sure that this always holds, we run
 JBMC on the example, with a reasonable `unwind` value:
 ```
-$ jbmc tutorial.ExampleUnwind --function tutorial.ExampleUnwind.doSomething --unwind 10
+$ jbmc tutorial.ExampleUnwind.doSomething --unwind 10
 ```
 Unsurprisingly JBMC doesn't agree, and prints an assertion failure
 (truncated here for readability):
@@ -223,7 +223,7 @@ Consider the following code:
 
 When given the `--throw-runtime-exceptions` options:
 ```
-$ jbmc tutorial.ExampleExceptions --tutorial.ExampleExceptions.strLength --throw-runtime-exceptions
+$ jbmc tutorial.ExampleExceptions.strLength --throw-runtime-exceptions
 ```
 JBMC will signal that the `str.length()` call may throw a runtime exception
 and that this exception is not caught.