Correct the documentation of ASSERT : it does not alter control flow.

After a discussion on issue #2031, this was agreed to be the correct
semantics for the following reasons:

1. We want to check for conditions that do not result in termination.
For example, generation of Inf and NaN, reachability of locations and
unsigned overflow / underflow, error locations, exceptions or the use of
program approximations.  This is particularly important for binary
analysis and security.

2. Allowing traces with multiple assertion failures reduces the number of
solver calls and test cases generated, allowing minimisation without
complex program manipulation.

3. If ASSERT alters control flow then the truth of assertions can change
as more assertions are added, as the failures may get blocked.  Adding
more checks can result in less failures.

4. If ASSERT alters control flow, then it must be taken into account when
slicing, meaning that every variable in any assert must be part of the
slice.

5. ASSUME allows arbitrary blocking of execution, it is better than ASSERT
is orthogonal and:
ASSERT(X)
ASSUME(X)
is used for cases where assertion failure results in termination (such as
null pointer dereference or array bounds failures).

Author: martin

src/goto-programs/goto_program.h

@@ -134,8 +134,9 @@ class goto_programt
   ///     Assume does not "retro-actively" affect the thread or any ASSERTs.
   /// - ASSERT:
   ///     Using ASSERT instructions is the one and only way to express
-  ///     properties to be verified. Execution paths abort if `guard` evaluates
-  ///     to false.
+  ///     properties to be verified.  An assertion is true / safe if `guard`
+  ///     is true in all possible executions, otherwise it is false / unsafe.
+  ///     The status of the assertion does not affect execution in any way.
   /// - SKIP, LOCATION:
   ///     No-op.
   /// - ATOMIC_BEGIN, ATOMIC_END: