Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Disable core __get_related logic #1674

Merged
merged 1 commit into from
Apr 24, 2020
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 13 additions & 1 deletion manticore/core/smtlib/constraints.py
Original file line number Diff line number Diff line change
Expand Up @@ -106,7 +106,19 @@ def _get_sid(self) -> int:
return self._sid

def __get_related(self, related_to=None):
if related_to is not None:
# sam.moelius: 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, {}.
# In light of the above, the core __get_related logic is currently disabled.
# if related_to is not None:
if False:
number_of_constraints = len(self.constraints)
remaining_constraints = set(self.constraints)
related_variables = get_variables(related_to)
Expand Down