static Set<DfaCallState> addContractResults(@NotNull MethodContract contract,
                                              @NotNull Set<DfaCallState> states,
                                              @NotNull DfaValueFactory factory,
                                              @NotNull Set<DfaMemoryState> finalStates) {
    if (contract.isTrivial()) {
      for (DfaCallState callState : states) {
        DfaValue result = contract.getReturnValue().getDfaValue(factory, callState);
        callState.getMemoryState().push(result);
        finalStates.add(callState.getMemoryState());
      }
      return Collections.emptySet();
    }

    Set<DfaCallState> falseStates = new LinkedHashSet<>();

    for (DfaCallState callState : states) {
      for (ContractValue condition : contract.getConditions()) {
        callState = condition.updateState(callState);
      }
      DfaMemoryState state = callState.getMemoryState();
      DfaCallArguments arguments = callState.getCallArguments();
      for (ContractValue contractValue : contract.getConditions()) {
        DfaCondition condition = contractValue.makeCondition(factory, callState.getCallArguments());
        DfaMemoryState falseState = state.createCopy();
        DfaCondition falseCondition = condition.negate();
        if (contract.getReturnValue().isFail() ?
            falseState.applyCondition(falseCondition) :
            falseState.applyContractCondition(falseCondition)) {
          falseStates.add(callState.withMemoryState(falseState).withArguments(arguments));
        }
        if (!state.applyContractCondition(condition)) {
          state = null;
          break;
        }
      }
      if (state != null) {
        DfaValue result = contract.getReturnValue().getDfaValue(factory, callState.withArguments(arguments));
        state.push(result);
        finalStates.add(state);
      }
    }

    return falseStates;
  }
static Set<DfaCallState> addContractResults(@NotNull MethodContract contract,
                                              @NotNull Set<DfaCallState> states,
                                              @NotNull DfaValueFactory factory,
                                              @NotNull Set<DfaMemoryState> finalStates)