Fix and refactor relevant domain (#6528)

Fix and refactor relevant domain (#6528)

In a handcrafted case, one can make the body of quantified formula another quantified formula when special attributes are used. The relevant domain utility was not robust to this case, leading to instantiations with free variables.

This fixes the issue and also updates its style to use a term context stack, which also avoids a tree traversal of the bodies of quantified formulas in this utility.

Fixes #6476. The benchmark from that issue now times out.