Connecting Inner and Outer Quantifiers (Nesting)

[viper-admin]

Created by bitbucket user nilsbecker_ on 2019-02-27 20:21

In some cases, when z3 doesn't rewrite nested quantifiers into a single quantifier, it may be useful to be able to tell which instantiation of the outer quantifier lead to the creation of the inner quantifier.