Weaken the stack scoping assumptions to avoid assuming false

[danmatichuk]

By default (without the no-assume-stack-scope flag) we inject an additional assumption into each equivalence domain that implicitly assumes everything past the scope of the current stack frame is equal. Effectively this avoids needing to reason about a fair number of spurious edge cases related to pointer aliasing, and is generally true in the cases where good stack hygiene is practiced by the program.

However it is often too strong of an assumption when the original and patched programs have even slightly different stack behavior (i.e. the patched program pushes a value onto the stack when the original doesn't). Given a sufficiently strong value domain, this can end up assuming "false" when attempting to assume the normal validity constraints for a given CFAR, thus crashing the verifier.

Two steps are warranted given this:

1. Swap the default behavior of this flag to not be enabled.
2. Weaken the assumption to exclude values that are provably inequivalent, since this will necessarily assume false and crash.