public static void introduceModule(Module module) {
    module.surrogateValueInverse = null;
    { Object old$Context$000 = Stella.$CONTEXT$.get();
      Object old$Module$000 = Stella.$MODULE$.get();

      try {
        Native.setSpecial(Stella.$CONTEXT$, Logic.$PL_KERNEL_MODULE$);
        Native.setSpecial(Stella.$MODULE$, ((Context)(Stella.$CONTEXT$.get())).baseModule);
        if (module.surrogateValueInverse == null) {
          { boolean successP = false;
            Stella_Object unused = null;
            Surrogate surrogate = null;

            { Object [] caller_MV_returnarray = new Object[2];

              successP = Stella_Object.bindToSurrogateP(module, module.name(), true, true, caller_MV_returnarray);
              unused = ((Stella_Object)(caller_MV_returnarray[0]));
              surrogate = ((Surrogate)(caller_MV_returnarray[1]));
            }
            unused = unused;
            if (successP) {
              module.surrogateValueInverse = surrogate;
            }
          }
        }
        Logic.assertIsaProposition(module, Logic.SGT_STELLA_MODULE);

      } finally {
        Stella.$MODULE$.set(old$Module$000);
        Stella.$CONTEXT$.set(old$Context$000);
      }
    }
  }