Since the execution of certain Java/BSL operators can throw
run-time exceptions (e.g., NullPointerException), expressions
containing such operators are conjoined with implicit constraints
prohibiting such exceptions (which might otherwise interfere with
the model checking). For example, the predicate expression
x.f is interpretted as (x != null) && x.f--if
x == null, the predicate is false. If static analysis
can determine that such exceptions will not be thrown, then
the constraints can be omitted.