SMTChecker: Loop conditions should be analyzed as in loop context in BMC

[blishko]

Value of loop condition can change between iterations of the loop. Therefore, BMC should be in the "inside loop" state when analyzing loop conditions.

Previously, when visiting loop condition of a top-level loop, BMC engine did not consider itself being "inside loop", and therefore was checking if the condition is constant (always true or always false). When the condition is always true in the first iteration and always false in the second iteration, BMC would try to report these two contradicting statements for the same source code expression, leading to an assertion violation in the UniqueErrorReporter. Because the value of the condition can change between iteration, BMC should not try to check for constant condition in these cases.

As part of this PR the handling of the ConstantCondition verification target has been refactored (first commit).

Fixes #15847.