public static void collectOptimizerVariables(Proposition proposition, List collection) {
    { Keyword testValue000 = proposition.kind;

      if ((testValue000 == Logic.KWD_ISA) ||
          ((testValue000 == Logic.KWD_FUNCTION) ||
           ((testValue000 == Logic.KWD_PREDICATE) ||
            ((testValue000 == Logic.KWD_EQUIVALENT) ||
             (testValue000 == Logic.KWD_IMPLIES))))) {
        { Stella_Object arg = null;
          Vector vector000 = proposition.arguments;
          int index000 = 0;
          int length000 = vector000.length();

          for (;index000 < length000; index000 = index000 + 1) {
            arg = (vector000.theArray)[index000];
            if (Logic.unboundVariableP(arg)) {
              { PatternVariable variable = ((PatternVariable)(arg));

                if (!(variable == Logic.innermostOf(variable))) {
                  Logic.simulateBindVariableToValue(variable);
                }
                else if ((variable.definingProposition == null) &&
                    (!Skolem.anonymousVariableP(variable))) {
                  collection.insertNew(variable);
                }
              }
            }
          }
        }
      }
      else {
      }
    }
  }