Fix minor typos

Author: Owen Jones

doc/architectural/cbmc-architecture.md

@@ -52,7 +52,7 @@ be output to files (this is what `goto-cc` does) and are (informally)
 referred to as “goto binaries” or “goto programs”. The back-end are
 tools process this format, either directly from the front-end or from
 it’s saved output. These include a wide range of analysis and
-transformation tools (see \ref section-other-tools).
+transformation tools (see \ref other-tools).
 
 # Concepts #
 ## {C, java bytecode} → Parse tree → Symbol table → GOTO programs → GOTO program transformations → BMC → counterexample (goto_tracet) → printing ##

doc/architectural/compilation-and-development.md

@@ -24,7 +24,7 @@ To be documented.
 The regression tests are contained in the `regression/` folder.
 They are grouped into directories for each of the tools/modules.
 Each of these contains multiple directories, each of which contains
-input files and one or more`.desc` files that describe what command
+input files and one or more `.desc` files that describe what command
 to run, what output is expected and so on. There is a Perl script,
 `test.pl` that is used to invoke the tests as:
 

src/goto-programs/README.md

@@ -5,7 +5,7 @@
 
 \author Kareem Khazem, Martin Brain
 
-\section overview Overview
+\section goto-programs-overview Overview
 Goto programs are the intermediate representation of the CPROVER tool
 chain. They are language independent and similar to many of the compiler
 intermediate languages. Section \ref goto-programs describes the

src/solvers/README.md

@@ -4,7 +4,7 @@
 
 \authors Romain Brenguier, Kareem Khazem, Martin Brain
 
-\section overview Overview
+\section solvers-overview Overview
 
 The basic role of solvers is to answer whether the set of equations given
 is satisfiable.