code: def add_condition(self, condition: z3.BoolRef) -> None:
          
          variables = set(_get_expr_variables(condition))
          relevant_buckets = set()
          for variable in variables:
              try:
                  bucket = self.variable_map[str(variable)]
                  relevant_buckets.add(bucket)
              except KeyError:
                  continue
  
          new_bucket = DependenceBucket(variables, [condition])
          self.buckets.append(new_bucket)
  
          if relevant_buckets:
              # Merge buckets, and rewrite variable map accordingly
              relevant_buckets.add(new_bucket)
              new_bucket = self._merge_buckets(relevant_buckets)
  
          for variable in new_bucket.variables:
              self.variable_map[str(variable)] = new_bucket
docs: Add condition to the dependence map
          :param condition: The condition that is to be added to the dependence map