public static Proposition buildTopLevelProposition(Stella_Object tree, boolean trueassertionP) {
    if (Stella_Object.isaP(tree, Logic.SGT_STELLA_STRING_WRAPPER)) {
      return (Logic.buildTopLevelProposition(Stella.readSExpressionFromString(((StringWrapper)(tree)).wrapperValue), trueassertionP));
    }
    { Proposition proposition = null;
      Cons logicvariabletable = ((Cons)(Logic.$LOGICVARIABLETABLE$.get()));

      { Object old$Logicvariabletable$000 = Logic.$LOGICVARIABLETABLE$.get();
        Object old$Variableidcounter$000 = Logic.$VARIABLEIDCOUNTER$.get();
        Object old$Termunderconstruction$000 = Logic.$TERMUNDERCONSTRUCTION$.get();

        try {
          Native.setSpecial(Logic.$LOGICVARIABLETABLE$, ((Cons)(((logicvariabletable != null) ? logicvariabletable : Stella.NIL))));
          Native.setIntSpecial(Logic.$VARIABLEIDCOUNTER$, ((Integer)(Logic.$VARIABLEIDCOUNTER$.get())).intValue());
          Native.setSpecial(Logic.$TERMUNDERCONSTRUCTION$, tree);
          proposition = ((Proposition)(Logic.buildProposition(tree)));
          if (proposition != null) {
            Proposition.normalizeTopLevelProposition(proposition);
            Proposition.verifyForallPropositions(proposition);
            if (!(Proposition.collectUnresolvedSlotReferences(proposition) == Stella.NIL)) {
              if (trueassertionP) {
                Proposition.updateSkolemTypeFromIsaAssertions(proposition);
              }
              Logic.resolveUnresolvedSlotReferences(proposition);
            }
            if (trueassertionP &&
                ((proposition.kind == Logic.KWD_EXISTS) &&
                 (!Logic.descriptionModeP()))) {
              Proposition.instantiateUndefinedSurrogates(proposition);
            }
            proposition = Proposition.recursivelyFastenDownPropositions(proposition, false);
          }

        } finally {
          Logic.$TERMUNDERCONSTRUCTION$.set(old$Termunderconstruction$000);
          Logic.$VARIABLEIDCOUNTER$.set(old$Variableidcounter$000);
          Logic.$LOGICVARIABLETABLE$.set(old$Logicvariabletable$000);
        }
      }
      return (proposition);
    }
  }