Returns True if the expression `e` has only one solution by querying
        the constraint solver. It does also add that unique solution to the
        solver's constraints.

def unique(self, e, **kwargs):
        """
        Returns True if the expression `e` has only one solution by querying
        the constraint solver. It does also add that unique solution to the
        solver's constraints.
        """
        if not isinstance(e, claripy.ast.Base):
            return True

        # if we don't want to do symbolic checks, assume symbolic variables are multivalued
        if o.SYMBOLIC not in self.state.options and self.symbolic(e):
            return False

        r = self.eval_upto(e, 2, **kwargs)
        if len(r) == 1:
            self.add(e == r[0])
            return True
        elif len(r) == 0:
            raise SimValueError("unsatness during uniqueness check(ness)")
        else:
            return False