Renamed core-goto to symex-ready-goto

As agreed we changed the concept of core-goto to symex-ready-goto as the
symex after the transformations.
This commit rewrites the documentation accordingly.

Author: Enrico Steffinlongo

doc/ADR/README.md

@@ -6,8 +6,8 @@ where taken at the time they were, so that future maintainers
 can more easily identify constraints that shaped the architecture
 of the system and the surrounding infrastructure.
 
-## Core goto form
-\subpage core-goto
+## Symex ready goto form
+\subpage symex-ready-goto
 
 ## Release & Packaging
 

doc/ADR/core_goto.md renamed to doc/ADR/symex_ready_goto.md

@@ -1,13 +1,13 @@
-\page core-goto Core goto definition
+\page symex-ready-goto Symex ready goto definition
 
 During the analysis of a program CBMC transforms the input program in an intermediate language
 called extended goto. Then the tool performs a series of simplifications on the obtained goto
 program until the program is given to the solver.
 
-We say that a program is in the **core goto form** when all the extended goto features have
+We say that a program is in the **symex ready goto form** when all the extended goto features have
 been simplified.
 
-More specifically, a program that is in **core goto form** is one that can be passed to **symex** by
+More specifically, a program that is in **symex ready goto form** is one that can be passed to **symex** by
 using any solver deriving from `goto_verifiert` without requiring any lowering step.
 
 At the time of writing, verifiers extending `goto_verifiert` are:

doc/architectural/goto-program-transformations.md

@@ -5,7 +5,7 @@
 \section required-transforms Core Transformation Passes
 
 This section lists the transformation passes that must have been applied for the
-goto model to be in core goto format.
+goto model to be in symex ready goto format.
 
 Note that the passes are listed below in the order they are currently called in
 CBMC. While all dependencies on the ordering are not fully documented, the
@@ -184,11 +184,11 @@ nondet-transform if it is being used.</em>
 
 This transformation removes skip instructions. Note that this transformation is
 called in many places and may be called as part of other transformations. This
-instance here is part of the mandatory transformation to reach core goto format.
-If there is a use case where it is desirable to preserve a "no operation"
-instruction, a `LOCATION` type instruction may be used in place of a `SKIP`
-instruction. The `LOCATION` instruction has the same semantics as the `SKIP`
-instruction, but is not removed by the remove skip instructions pass.
+instance here is part of the mandatory transformation to reach symex ready goto
+format. If there is a use case where it is desirable to preserve a "no
+operation" instruction, a `LOCATION` type instruction may be used in place of a
+`SKIP` instruction. The `LOCATION` instruction has the same semantics as the
+`SKIP` instruction, but is not removed by the remove skip instructions pass.
 
 The implementation of this pass is called via \ref remove_skip(goto_modelt &)
 
@@ -215,7 +215,7 @@ coverage-transform if it is being used.</em>
 
 The sections lists the optional transformation passes that are optional and will
 modify a goto model. Note that these are documented here for consistency, but
-not required for core goto format.
+not required for symex ready goto format.
 
 Note for each optional pass there is a listed predeceesor pass. This is the pass
 currently called before the listed pass in CBMC. While the ordering may not be