private void addMethodAnnotations(@NotNull Map<EKey, Value> solution, @NotNull MethodAnnotations methodAnnotations, @NotNull EKey methodKey, int arity)
    throws EquationsLimitException {
    List<StandardMethodContract> contractClauses = new ArrayList<>();
    Set<EKey> notNulls = methodAnnotations.notNulls;
    Map<EKey, String> contracts = methodAnnotations.contractsValues;

    ContractReturnValue fullReturnValue = methodAnnotations.returnValue.asContractReturnValue();
    for (Map.Entry<EKey, Value> entry : solution.entrySet()) {
      // NB: keys from Psi are always stable, so we need to stabilize keys from equations
      Value value = entry.getValue();
      if (value == Value.Top || value == Value.Bot) continue;
      EKey key = entry.getKey().mkStable();
      Direction direction = key.getDirection();
      EKey baseKey = key.mkBase();
      if (!methodKey.equals(baseKey)) {
        continue;
      }
      if (value == Value.Fail && direction.isNullFail() && !methodAnnotations.mutates.isPure()) {
        if (!isPureModuloFailCause(solution, key, direction)) {
          // Impure methods with "null->fail" contract are just assumed to have `@NotNull` annotation on the corresponding parameter
          continue;
        }
      }
      if (value == Value.NotNull && direction == Out) {
        notNulls.add(methodKey);
      }
      else if (direction instanceof ParamValueBasedDirection) {
        ContractReturnValue contractReturnValue =
          fullReturnValue.equals(ContractReturnValue.returnAny()) || value == Value.Fail ? value.toReturnValue() : fullReturnValue;
        contractClauses.add(contractElement(arity, (ParamValueBasedDirection)direction, contractReturnValue));
      }
    }

    Map<Boolean, List<StandardMethodContract>> partition =
      StreamEx.of(contractClauses).partitioningBy(c -> c.getReturnValue().isFail());
    List<StandardMethodContract> failingContracts = squashContracts(partition.get(true));
    List<StandardMethodContract> nonFailingContracts = squashContracts(partition.get(false));
    // Sometimes "null,_->!null;!null,_->!null" contracts are inferred for some reason
    // They are squashed to "_,_->!null" which is better expressed as @NotNull annotation
    if (nonFailingContracts.size() == 1) {
      StandardMethodContract contract = nonFailingContracts.get(0);
      if (contract.getReturnValue().equals(ContractReturnValue.returnNotNull()) && contract.isTrivial()) {
        nonFailingContracts = Collections.emptyList();
        notNulls.add(methodKey);
      }
    }
    List<StandardMethodContract> allContracts = StreamEx.of(failingContracts, nonFailingContracts).toFlatList(Function.identity());
    removeConstraintFromNonNullParameter(methodKey, allContracts);

    if (allContracts.isEmpty() && !fullReturnValue.equals(ContractReturnValue.returnAny())) {
      allContracts.add(StandardMethodContract.trivialContract(arity, fullReturnValue));
    }
    if (notNulls.contains(methodKey)) {
      // filter contract clauses for @NotNull methods
      allContracts.removeIf(smc -> smc.getReturnValue().equals(ContractReturnValue.returnNotNull()));
    }
    // Failing contracts go first
    String result = StreamEx.of(allContracts)
                            .sorted(Comparator.comparingInt((StandardMethodContract smc) -> smc.getReturnValue().isFail() ? 0 : 1)
                                              .thenComparing(StandardMethodContract::toString))
                            .map(Object::toString)
                            .distinct()
                            .map(str -> str.replace(" ", "")) // for compatibility with existing tests
                            .joining(";");
    contracts.put(methodKey, result);
  }
private void addMethodAnnotations(@NotNull Map<EKey, Value> solution, @NotNull MethodAnnotations methodAnnotations, @NotNull EKey methodKey, int arity)