Flaw in __get_related core logic

[smoelius]

There is a flaw in how __get_related works: when called on certain unsatisfiable sets, it can return a satisfiable one. The flaw arises when:

• self consists of a single constraint C
• C is the value of the related_to parameter
• C contains no variables
• C is unsatisfiable

Since C contains no variables, it is not considered "related to" itself and is thrown out by __get_related. Since C was the sole element of self, __get_related returns the empty set. Thus, __get_related was called on an unsatisfiable set, {C}, but it returned a satisfiable one, {}.

I suspect this is the reason for #1678.

[ehennenfent]

It looks like the changes introduced in #1674 introduce some problems of their own. In #1677, I discovered that we end up with constraint sets where constraints from the related set have the same name (but a different size) than constraints from the original set, which could probably lead to incorrect results from Z3. The old get_related logic seemed to handle some edge cases that the default case doesn't, so we should try to fix this soon.

Sam, do you have an existing example of the flaw above that you're able to share? If not, no worries - it should be easy enough to replicate from your description.