public static void handleArityViolation(Proposition proposition, int requiredarity) {
    if (((Keyword)(Logic.$TYPECHECKMODE$.get())) == Logic.KWD_POST_TYPE_VIOLATIONS) {
      Proposition.postToCheckTypesAgenda(proposition);
    }
    else if ((((Keyword)(Logic.$TYPECHECKMODE$.get())) == Logic.KWD_SIGNAL_TYPE_VIOLATIONS) ||
        ((((Keyword)(Logic.$TYPECHECKMODE$.get())) == Logic.KWD_REPORT_TYPE_VIOLATIONS) ||
         (((Keyword)(Logic.$TYPECHECKMODE$.get())) == Logic.KWD_AUTOMATICALLY_FIX_TYPE_VIOLATIONS))) {
      { OutputStringStream stream000 = OutputStringStream.newOutputStringStream();

        { Object old$PrintreadablyP$000 = Stella.$PRINTREADABLYp$.get();

          try {
            Native.setBooleanSpecial(Stella.$PRINTREADABLYp$, true);
            {
              stream000.nativeStream.println("ERROR: Too `" + (((proposition.arguments.length() > requiredarity) ? "many" : "few")) + "' arguments in the proposition");
              stream000.nativeStream.println("   `" + Logic.generateTerm(proposition) + "'");
              stream000.nativeStream.println("   Expected `" + requiredarity + "' argument(s)..");
            }
;
            Logic.helpSignalPropositionError(stream000, Logic.KWD_ERROR);

          } finally {
            Stella.$PRINTREADABLYp$.set(old$PrintreadablyP$000);
          }
        }
        throw ((PropositionError)(PropositionError.newPropositionError(stream000.theStringReader()).fillInStackTrace()));
      }
    }
    else {
      { OutputStringStream stream001 = OutputStringStream.newOutputStringStream();

        stream001.nativeStream.print("`" + ((Keyword)(Logic.$TYPECHECKMODE$.get())) + "' is not a valid case option");
        throw ((StellaException)(StellaException.newStellaException(stream001.theStringReader()).fillInStackTrace()));
      }
    }
  }