Peter's comments 3

Consider that compiled class file is in a folder named after its
package.

Author: Joel Allred

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

@@ -22,9 +22,9 @@ features of JBMC, and explore the most useful features.
 
 \subsection jbmc-manual-auto-assert Automatic assertions
 
-Consider the following simplistic `ExampleArray.java` file which we have compiled
-into `ExampleArray.class` and which contains a utility method to query a given
-array at a given index:
+Consider the following simplistic `ExampleArray.java` file which we have
+compiled into `tutorial/ExampleArray.class` and which contains a utility method
+to query a given array at a given index:
 ```
  1| package tutorial;
  2|
@@ -39,7 +39,7 @@ array at a given index:
 Now let's run the following command to let JBMC tell us about potential errors
 in our `query` method.
 
-    $ jbmc ExampleArray.class --function tutorial.ExampleArray.query
+    $ jbmc tutorial/ExampleArray.class --function tutorial.ExampleArray.query
 
 
 The output contains the following:
@@ -116,7 +116,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 ExampleUnwind.class --function tutorial.ExampleUnwind.isPrime --unwind 10
+    $ jbmc tutorial/ExampleUnwind.class --function tutorial.ExampleUnwind.isPrime --unwind 10
 
 will terminate correctly. In this case, we will see `VERIFICATION SUCCESSFUL`,
 as no automatic assertions are violated.
@@ -129,7 +129,7 @@ JBMC will try do 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 ExampleUnwind.class --function tutorial.ExampleUnwind.doSomething --unwind 10
+    $ jbmc tutorial/ExampleUnwind.class --function tutorial.ExampleUnwind.doSomething --unwind 10
 
 Unsurprisingly JBMC doesn't agree, and prints an assertion failure
 (truncated here for readability):
@@ -178,7 +178,7 @@ from `java.lang.String`, e.g.
 The following command line (note that the current directory is also added to
 the classpath):
 
-    $ jbmc ExampleModels.class --cp <path_to_cbmc>/jbmc/src/java_bytecode/library/core-models.jar:.
+    $ jbmc tutorial/ExampleModels.class --cp <path_to_cbmc>/jbmc/src/java_bytecode/library/core-models.jar:.
 
 will flag this violation (truncated):
 ```c