As soon as a quantifier (@ForAll, @Exists) can foresee the final outcome it should stop. The shortcut can be taken if: (a) @Exists sees a value which is "true", or (b) @ForAll sees a value which is "false".
Log in to post a comment.