Difference between union and union_instantiations (for Analysis)

[skius]

Hi!

I was going through the Analysis examples and came across a small difference between tests/prop.rs and the Analysis docs: The former uses union_instantiations while the latter simply uses union.

What is the difference between the two? I know that union_instantiations doesn't exist in 0.6.0, but is there e.g. a performance or expressibility benefit to it (apart from constructing Explanations)?

[mwillsey]

Hi there! We still to working on the explanations feature, so maybe @oflatt will want to say more, but here is my current understanding.

You can use union if you want, but if you then ask for explanations, you won't get one for those unions. Using union_instantiations will work provide that explanation if they are enabled, but behave like union otherwise.

[oflatt]

That's right! In fact, union is disallowed when explanations are turned on.