Fix based on comments

Clarifications in the language of the manual entry.

Author: Petr Bauch

doc/cprover-manual/goto-harness.md

@@ -314,12 +314,12 @@ VERIFICATION SUCCESSFUL
 
 ### The memory snapshot harness
 
-The `function-call` harness is used in situations when we want the analysed
+The `function-call` harness is used in situations in which we want the analysed
 function to work in arbitrary environment. If we want a more restricted
-environment or if we have the program in which our function will only be called,
-we call the `memory-snapshot` harness instead.
+environment or if we have the program in which our function will be called,
+we can call the `memory-snapshot` harness instead.
 
-Furthermore, the program state of interest may be taken a particular location
+Furthermore, the program state of interest may be taken at a particular location
 within a function. In that case we do not want the harness to instrument the
 whole function but rather to allow starting the execution from a specific
 initial location (specified via `--initial-location func[:<n>]`).
@@ -374,8 +374,8 @@ int main() {
 }
 ```
 
-But are not particularly interested in the analysing the complex function, since
-we trust that its implementation is correct. Hence we run the above program
+But are not particularly interested in analysing the complex function, since we
+trust that its implementation is correct. Hence we run the above program
 stopping after the assignments to `x` and `x` and storing the program state,
 e.g. using the `memory-analyzer`, in a JSON file `snapshot.json`. Then run the
 harness and verify the assertion with: