public final AntlrPilarParser.virtualSetDeclaration_return virtualSetDeclaration()
      throws RecognitionException {
    AntlrPilarParser.virtualSetDeclaration_return retval = new AntlrPilarParser.virtualSetDeclaration_return();
    retval.start = input.LT(1);
    int virtualSetDeclaration_StartIndex = input.index();
    Object root_0 = null;

    Token t = null;
    Token ID138 = null;
    Token char_literal140 = null;
    Token char_literal142 = null;
    Token char_literal144 = null;
    AntlrPilarParser.annotationList_return annotationList139 = null;

    AntlrPilarParser.vsetElement_return vsetElement141 = null;

    AntlrPilarParser.vsetElement_return vsetElement143 = null;

    Object t_tree = null;
    Object ID138_tree = null;
    Object char_literal140_tree = null;
    Object char_literal142_tree = null;
    Object char_literal144_tree = null;
    RewriteRuleTokenStream stream_172 = new RewriteRuleTokenStream(adaptor,
        "token 172");
    RewriteRuleTokenStream stream_186 = new RewriteRuleTokenStream(adaptor,
        "token 186");
    RewriteRuleTokenStream stream_ID = new RewriteRuleTokenStream(adaptor,
        "token ID");
    RewriteRuleTokenStream stream_178 = new RewriteRuleTokenStream(adaptor,
        "token 178");
    RewriteRuleTokenStream stream_177 = new RewriteRuleTokenStream(adaptor,
        "token 177");
    RewriteRuleSubtreeStream stream_annotationList = new RewriteRuleSubtreeStream(
        adaptor, "rule annotationList");
    RewriteRuleSubtreeStream stream_vsetElement = new RewriteRuleSubtreeStream(
        adaptor, "rule vsetElement");
    try {
      if (state.backtracking > 0 && alreadyParsedRule(input, 40)) {
        return retval;
      }
      // /Users/robby/Repositories/sireum-parser/sireum-parser/src/main/java/org/sireum/pilar/parser/AntlrPilar.g:362:2: (t= 'vset' ID annotationList '{' vsetElement ( ',' vsetElement )* '}' -> ^( VSET[$t] ID annotationList ^( LIST ( vsetElement )+ ) ) )
      // /Users/robby/Repositories/sireum-parser/sireum-parser/src/main/java/org/sireum/pilar/parser/AntlrPilar.g:362:4: t= 'vset' ID annotationList '{' vsetElement ( ',' vsetElement )* '}'
      {
        t = (Token) match(input, 186, FOLLOW_186_in_virtualSetDeclaration2955);
        if (state.failed) return retval;
        if (state.backtracking == 0) stream_186.add(t);

        ID138 = (Token) match(input, ID, FOLLOW_ID_in_virtualSetDeclaration2957);
        if (state.failed) return retval;
        if (state.backtracking == 0) stream_ID.add(ID138);

        pushFollow(FOLLOW_annotationList_in_virtualSetDeclaration2959);
        annotationList139 = annotationList();

        state._fsp--;
        if (state.failed) return retval;
        if (state.backtracking == 0)
          stream_annotationList.add(annotationList139.getTree());
        char_literal140 = (Token) match(
            input,
            177,
            FOLLOW_177_in_virtualSetDeclaration2964);
        if (state.failed) return retval;
        if (state.backtracking == 0) stream_177.add(char_literal140);

        pushFollow(FOLLOW_vsetElement_in_virtualSetDeclaration2969);
        vsetElement141 = vsetElement();

        state._fsp--;
        if (state.failed) return retval;
        if (state.backtracking == 0)
          stream_vsetElement.add(vsetElement141.getTree());
        // /Users/robby/Repositories/sireum-parser/sireum-parser/src/main/java/org/sireum/pilar/parser/AntlrPilar.g:364:16: ( ',' vsetElement )*
        loop41: do {
          int alt41 = 2;
          int LA41_0 = input.LA(1);

          if ((LA41_0 == 172)) {
            alt41 = 1;
          }

          switch (alt41) {
            case 1:
            // /Users/robby/Repositories/sireum-parser/sireum-parser/src/main/java/org/sireum/pilar/parser/AntlrPilar.g:364:18: ',' vsetElement
            {
              char_literal142 = (Token) match(
                  input,
                  172,
                  FOLLOW_172_in_virtualSetDeclaration2973);
              if (state.failed) return retval;
              if (state.backtracking == 0) stream_172.add(char_literal142);

              pushFollow(FOLLOW_vsetElement_in_virtualSetDeclaration2975);
              vsetElement143 = vsetElement();

              state._fsp--;
              if (state.failed) return retval;
              if (state.backtracking == 0)
                stream_vsetElement.add(vsetElement143.getTree());

            }
              break;

            default:
              break loop41;
          }
        } while (true);

        char_literal144 = (Token) match(
            input,
            178,
            FOLLOW_178_in_virtualSetDeclaration2983);
        if (state.failed) return retval;
        if (state.backtracking == 0) stream_178.add(char_literal144);

        // AST REWRITE
        // elements: vsetElement, ID, annotationList
        // token labels: 
        // rule labels: retval
        // token list labels: 
        // rule list labels: 
        // wildcard labels: 
        if (state.backtracking == 0) {
          retval.tree = root_0;
          RewriteRuleSubtreeStream stream_retval = new RewriteRuleSubtreeStream(
              adaptor, "rule retval", retval != null ? retval.tree : null);

          root_0 = (Object) adaptor.nil();
          // 365:41: -> ^( VSET[$t] ID annotationList ^( LIST ( vsetElement )+ ) )
          {
            // /Users/robby/Repositories/sireum-parser/sireum-parser/src/main/java/org/sireum/pilar/parser/AntlrPilar.g:365:44: ^( VSET[$t] ID annotationList ^( LIST ( vsetElement )+ ) )
            {
              Object root_1 = (Object) adaptor.nil();
              root_1 = (Object) adaptor.becomeRoot(
                  (Object) adaptor.create(VSET, t),
                  root_1);

              adaptor.addChild(root_1, stream_ID.nextNode());
              adaptor.addChild(root_1, stream_annotationList.nextTree());
              // /Users/robby/Repositories/sireum-parser/sireum-parser/src/main/java/org/sireum/pilar/parser/AntlrPilar.g:365:73: ^( LIST ( vsetElement )+ )
              {
                Object root_2 = (Object) adaptor.nil();
                root_2 = (Object) adaptor.becomeRoot(
                    (Object) adaptor.create(LIST, "LIST"),
                    root_2);

                if (!(stream_vsetElement.hasNext())) {
                  throw new RewriteEarlyExitException();
                }
                while (stream_vsetElement.hasNext()) {
                  adaptor.addChild(root_2, stream_vsetElement.nextTree());

                }
                stream_vsetElement.reset();

                adaptor.addChild(root_1, root_2);
              }

              adaptor.addChild(root_0, root_1);
            }

          }

          retval.tree = root_0;
        }
      }

      retval.stop = input.LT(-1);

      if (state.backtracking == 0) {

        retval.tree = (Object) adaptor.rulePostProcessing(root_0);
        adaptor.setTokenBoundaries(retval.tree, retval.start, retval.stop);
      }
    } catch (RecognitionException re) {
      reportError(re);
      recover(input, re);
      retval.tree = (Object) adaptor.errorNode(
          input,
          retval.start,
          input.LT(-1),
          re);

    } finally {
      if (state.backtracking > 0) {
        memoize(input, 40, virtualSetDeclaration_StartIndex);
      }
    }
    return retval;
  }