Change wording of unsoundness category and add page to CProver manual

Author: NlightNFotis

doc/cprover-manual/index.md

@@ -9,6 +9,7 @@
    * [A Short Tutorial](cbmc/tutorial/)
    * [Loop Unwinding](cbmc/unwinding/)
    * [Assertion Checking](cbmc/assertions/)
+   * [Unsound options](unsound_options.md)
 
 4. [Compositional Reasoning using Code Contracts](contracts/)
 

doc/cprover-manual/unsound_options.md

@@ -10,8 +10,8 @@ conversation about what it means for certain options to produce *unsound* behavi
 We concluded that *unsound* in this context is a proxy for the following two behaviours
 that we want to avoid:
 
-* **A spurious counter example to an assertion**, which gives a proof that the assertion
-  is refuted when it's not, and
+* **A spurious counter example to an assertion**, which means that the tool may report
+  a coverage property (or a line of code) as reachable when in fact it is not, and
 * **Wrong proof to an assertion**, which means that it might indicate an assertion passing
   when it's not.