diff --git a/doc/cprover-manual/api.md b/doc/cprover-manual/api.md
index 5cfa86b7c71..05327203f5e 100644
--- a/doc/cprover-manual/api.md
+++ b/doc/cprover-manual/api.md
@@ -87,7 +87,7 @@ void __CPROVER_cover(_Bool condition);
 ```
 
 This statement defines a custom coverage criterion, for usage with the
-[test suite generation feature](cover.shtml).
+[test suite generation feature](../test-suite/).
 
 #### \_\_CPROVER\_isnan, \_\_CPROVER\_isfinite, \_\_CPROVER\_isinf, \_\_CPROVER\_isnormal, \_\_CPROVER\_sign
 
diff --git a/doc/cprover-manual/cbmc-tutorial.md b/doc/cprover-manual/cbmc-tutorial.md
index 6e0f8ba3063..133f01cebb1 100644
--- a/doc/cprover-manual/cbmc-tutorial.md
+++ b/doc/cprover-manual/cbmc-tutorial.md
@@ -284,7 +284,7 @@ violates an assertion. Without unwinding assertions, or when using the
 `--depth` command line switch, CBMC does not prove the program correct,
 but it can be helpful to find program bugs. The various command line
 options that CBMC offers for loop unwinding are described in the section
-on [understanding loop unwinding](../../cbmc-unwinding/).
+on [understanding loop unwinding](../../cbmc/unwinding/).
 
 ### A Note About Compilers and the ANSI-C Library
 
diff --git a/doc/cprover-manual/goto-cc-variants.md b/doc/cprover-manual/goto-cc-variants.md
index 7deadcf8495..2793f532737 100644
--- a/doc/cprover-manual/goto-cc-variants.md
+++ b/doc/cprover-manual/goto-cc-variants.md
@@ -1,4 +1,4 @@
-[CPROVER Manual TOC](../)
+[CPROVER Manual TOC](../../)
 
 ## Variants of goto-cc
 
diff --git a/doc/cprover-manual/goto-cc.md b/doc/cprover-manual/goto-cc.md
index 0e3e9b75bd3..b0fe2899885 100644
--- a/doc/cprover-manual/goto-cc.md
+++ b/doc/cprover-manual/goto-cc.md
@@ -20,7 +20,7 @@ The normal build system for the project may be used to build the
 software, but the outcome will be a model file with suitable detail for
 verification, as opposed to a flat executable program. Note that goto-cc
 comes in different variants depending on the compilation environment.
-These variants are described [here](goto-cc-variants.shtml).
+These variants are described [here](variants/).
 
 ### Example: Building wu-ftpd
 
diff --git a/doc/cprover-manual/goto-harness.md b/doc/cprover-manual/goto-harness.md
index f7ae8fb5032..6476b415b7f 100644
--- a/doc/cprover-manual/goto-harness.md
+++ b/doc/cprover-manual/goto-harness.md
@@ -91,7 +91,7 @@ entry function for analysis, or further modify it with `goto-harness` or
 `goto-instrument` or other tools.
 
 The example above demonstrates the most simple case, which is roughly the same
-as the entry point `cbmc` automically generates for functions. However, the
+as the entry point `cbmc` automatically generates for functions. However, the
 `function-call` harness can also non-deterministically initialise global
 variables, array and struct elements. Consider this more complicated example:
 
diff --git a/doc/cprover-manual/jbmc-user-manual.md b/doc/cprover-manual/jbmc-user-manual.md
index 5d8179c403a..f2a00f71a1f 100644
--- a/doc/cprover-manual/jbmc-user-manual.md
+++ b/doc/cprover-manual/jbmc-user-manual.md
@@ -1,26 +1,26 @@
-\ingroup module_hidden
-\page jbmc-user-manual JBMC User Manual
+[CPROVER Manual TOC](../)
 
+# Verifying Java with JBMC
 
-\section jbmc-manual-intro Introduction
+## Introduction
 
 JBMC is a bounded model checking tool for the Java language. It follows the
 same principles as CBMC, thus the existing
-[documentation for CBMC](http://www.cprover.org/cprover-manual/cbmc.html)
+[documentation for CBMC](../cbmc/tutorial/)
 largely applies to JBMC.
 
-In brief, JBMC creates a model from Java Bytecode (given as input as a .class
-file or a .jar) and performs static analysis and symbolic execution which allow
-us to prove or refute properties. These properties are either automatically
-generated (runtime errors), or provided by the user in the form of assertions.
+In brief, JBMC creates a model from Java Bytecode (given as input as a
+`.class` file or a `.jar`) and performs static analysis and symbolic
+execution which allow us to prove or refute properties.  These properties
+are either automatically generated (runtime errors), or provided by the user
+in the form of assertions.
 
 Using examples, the following section will guide you through the basic
 features of JBMC.
 
+## JBMC tutorial
 
-\section jbmc-tutorial JBMC tutorial
-
-\subsection jbmc-manual-auto-assert Automatic assertions
+### Automatic assertions
 
 Consider the following simplistic `ExampleArray.java` file which we have
 compiled into `tutorial/ExampleArray.class` and which queries the array of
@@ -40,11 +40,12 @@ input arguments at index 3:
 
 Now let's run the following command to let JBMC tell us about potential errors
 in our program.
-
-    $ jbmc tutorial/ExampleArray.class
+```
+$ jbmc tutorial/ExampleArray.class
+```
 
 The output contains the following:
-```c
+```plaintext
 [java::tutorial.ExampleArray.main:([Ljava/lang/String;)V.null-pointer-exception.1] line 7 Null pointer check: SUCCESS
 [java::tutorial.ExampleArray.main:([Ljava/lang/String;)V.array-index-out-of-bounds-low.1] line 7 Array index should be >= 0: SUCCESS
 [java::tutorial.ExampleArray.main:([Ljava/lang/String;)V.array-index-out-of-bounds-high.1] line 7 Array index should be < length: FAILURE
@@ -75,12 +76,13 @@ safe as follows:
  13| }
 ```
 then when running JBMC on that corrected version:
-
-    $ jbmc tutorial/ExampleArraySafe.class
+```
+$ jbmc tutorial/ExampleArraySafe.class
+```
 
 all the automatic assertions become valid, meaning that there is no
 possible inputs (argument values) for which they can be violated:
-```c
+```plaintext
 [java::tutorial.ExampleArraySafe.main:([Ljava/lang/String;)V.1] line 7 no uncaught exception: SUCCESS
 [java::tutorial.ExampleArraySafe.main:([Ljava/lang/String;)V.null-pointer-exception.1] line 8 Null pointer check: SUCCESS
 [java::tutorial.ExampleArraySafe.main:([Ljava/lang/String;)V.null-pointer-exception.2] line 9 Null pointer check: SUCCESS
@@ -88,7 +90,7 @@ possible inputs (argument values) for which they can be violated:
 [java::tutorial.ExampleArraySafe.main:([Ljava/lang/String;)V.array-index-out-of-bounds-high.1] line 9 Array index should be < length: SUCCESS
 ```
 
-\subsection jbmc-manual-unwind Loop unwinding
+## Loop unwinding
 
 As CBMC, JBMC needs to unwind loops up to a given value. Consider the `isPrime`
 method in the code below. Without specifying an unwind limit, JBMC will not
@@ -120,9 +122,9 @@ 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.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.
 
@@ -130,18 +132,18 @@ Note that in that example, there are is no main function, so we give specify
 the desired entry point via the `--function` option.
 
 
-\subsection jbmc-manual-user-assert User assertions
+## User assertions
 
 Elaborating on the example above, users may provide their own assertions, that
 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.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):
-```c
+```plaintext
 [...doSomething:(I)V.assertion.1] line 7 assertion at file tutorial/ExampleUnwind.java: FAILURE
 ```
 
@@ -149,20 +151,20 @@ Rerunning the analysis with the `--trace` option, the following line appears
 somewhere in the trace output and tells us which input value JBMC found to
 trigger the violation (note that to see the original parameter names in the
 trace output, the Java source must be compiled in debug mode: `javac -g`):
-```c
+```plaintext
 INPUT inputVal: 15
 ```
 The value chosen by JBMC is arbitrary, and could as well be 9
 or 2084569161.
 
-\subsection jbmc-manual-library Java Library support
+## Java Library support
 
 The examples above only involve primitive types. In order to analyse code
 involving Java Library classes, the core models (located in the same
 repository) need to be added to the classpath:
-
-    --cp <path_to_cbmc>/jbmc/src/java_bytecode/library/core-models.jar
-
+```
+--cp <path_to_cbmc>/jbmc/src/java_bytecode/library/core-models.jar
+```
 
 The core models library simulate the behavior of the Java Library and
 contains some commonly used classes, such as Object, Class, String, Enum.
@@ -185,21 +187,21 @@ from `java.lang.String`, e.g.
 ```
 The following command line (note that the current directory is also added to
 the classpath):
-
-    $ jbmc tutorial/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
+```plaintext
 [java::tutorial.ExampleModels.stringOp:()V.assertion.1] line 8 assertion: FAILURE
 ```
 
 Again, the trace (when re-running with `--trace`) shows the string violating
 the condition in the assertion:
-```c
+```plaintext
 dynamic_object2={ 'a', 'b', '$', 'c', 'd' }
 ```
 
-\subsection jbmc-manual-exceptions Exceptions
+## Exceptions
 
 In its analysis, JBMC can take into account exceptions thrown by user code or
 library classes, as well as runtime exceptions such as NullPointerException.
@@ -220,13 +222,12 @@ Consider the following code:
 ```
 
 When given the `--throw-runtime-exceptions` options:
-
-    $ jbmc tutorial/ExampleExceptions --tutorial.ExampleExceptions.strLength --throw-runtime-exceptions
-
+```
+$ jbmc tutorial/ExampleExceptions --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.
-
-```c
+```plaintext
 [java::tutorial.ExampleExceptions.strLength:(Ljava/lang/String;)I.1] line 6 no uncaught exception: FAILURE
 ```
 This could be fixed by adding a try-catch statement, or else checking that
@@ -243,9 +244,9 @@ VERIFICATION SUCCESSFUL
 ```
 
 When analyzing this function without runtime exception support:
-
-    $ jbmc tutorial/ExampleExceptions
-
+```
+$ jbmc tutorial/ExampleExceptions
+```
 JBMC only reports the error as a null pointer check failure:
 ```
 [...null-pointer-exception.1] line 6 Null pointer check: FAILURE
@@ -258,11 +259,11 @@ on violation. This behavior can be replicated in JBMC by using the
 then be reported like any other uncaught exception.
 
 
-\subsection jbmc-manual-further-doc Further documentation
+## Further documentation
 
 JBMC has a wealth of other options that can either constrain the model (to
 cope with complexity issues), or output more relevant information. The list
 of all available options is printed by running:
-
-    $ jbmc --help
-
+```
+$ jbmc --help
+```
diff --git a/doc/cprover-manual/properties.md b/doc/cprover-manual/properties.md
index 17d9e399ac6..a8a9aa273b2 100644
--- a/doc/cprover-manual/properties.md
+++ b/doc/cprover-manual/properties.md
@@ -203,20 +203,22 @@ goto-instrument error_example.goto error_example_replaced.goto \
 cbmc error_example_replaced.goto
 ```
 
-Which gets us the output
+This generates the following output:
 
-> ** Results:
-> error_example.c function api_error
-> [api_error.assertion.1] line 4 assertion false: FAILURE
->
-> error_example.c function internal_error
-> [internal_error.assertion.1] line 5 assertion false: FAILURE
->
-> ** 2 of 2 failed (2 iterations)
-> VERIFICATION FAILED
+```
+** Results:
+error_example.c function api_error
+[api_error.assertion.1] line 4 assertion false: FAILURE
+
+error_example.c function internal_error
+[internal_error.assertion.1] line 5 assertion false: FAILURE
+
+** 2 of 2 failed (2 iterations)
+VERIFICATION FAILED
+```
 
-As opposed to the verification success we would have seen without the
-instrumentation step.
+Without the instrumentation step we would have seen
+"VERIFICATION SUCCESSFUL".
 
 The havoc option takes further parameters `globals` and `params` with this
 syntax: `havoc[,globals:<regex>][,params:<regex>]` (where the square brackets
@@ -241,10 +243,10 @@ int do_something_with_complex(struct Complex *complex);
 And the command line
 
 ```
-    goto-instrument in.goto out.goto
-      --generate-function-body do_something_with_complex
-      --generate-function-body-options
-        'havoc,params:.*,globals:AGlobalComplex'
+goto-instrument in.goto out.goto
+  --generate-function-body do_something_with_complex
+  --generate-function-body-options
+    'havoc,params:.*,globals:AGlobalComplex'
 ```
 
 The goto code equivalent of the following will be generated:
@@ -264,7 +266,7 @@ int do_something_with_complex(struct Complex *complex)
 ```
 
 A note on limitations: Because only static information is used for code
-generation, arrays of unknown size and pointers will not be affected by this;
+generation, arrays of unknown size and pointers will not be affected by this.
 Which means that for code like this:
 
 ```C
diff --git a/doc/cprover-manual/test-suite.md b/doc/cprover-manual/test-suite.md
index d5cff30ee45..2bbcc2f6274 100644
--- a/doc/cprover-manual/test-suite.md
+++ b/doc/cprover-manual/test-suite.md
@@ -5,7 +5,7 @@
 ### A Small Tutorial with a Case Study
 
 We assume that CBMC is installed on your system. If not, follow
-[these instructions](../../installation/).
+[these instructions](../installation/).
 
 CBMC can be used to automatically generate test cases that satisfy a
 certain [code coverage](https://en.wikipedia.org/wiki/Code_coverage)
@@ -197,12 +197,12 @@ unwound enough times. For example, `climb_pid_run` needs to
 be called at least six times for evaluating the condition
 `climb_sum_err>MAX_CLIMB_SUM_ERR` in line 48 to *true*. This corresponds
 to Test 5. To learn more about loop unwinding take a look at [Understanding Loop
-Unwinding](../../cbmc-unwinding/).
+Unwinding](../cbmc/unwinding/).
 
 In this tutorial, we present the automatic test suite generation
 functionality of CBMC, by applying the MC/DC code coverage criterion to
 a PID controller case study. In addition to `--cover mcdc`, other
-coverage criteria such as `branch`, `decision`, and `path`. are also
+coverage criteria such as `branch`, `decision`, and `path` are also
 available when calling CBMC.
 
 ### Coverage Criteria