1 files changed, 8 insertions, 17 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 6a045797a..e1f8031da 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -673,17 +673,14 @@ sygusGrammarV1[CVC4::Type & ret,
   : LPAREN_TOK { PARSER_STATE->pushScope(); }
   (LPAREN_TOK
        symbol[name, CHECK_NONE, SYM_VARIABLE] sortSymbol[t, CHECK_DECLARED] {
-         std::stringstream ss;
-         ss << fun << "_" << name;
          if (name == "Start")
          {
            startIndex = datatypes.size();
          }
-         std::string dname = ss.str();
          sgts.push_back(std::vector<CVC4::SygusGTerm>());
          sgts.back().push_back(CVC4::SygusGTerm());
          PARSER_STATE->pushSygusDatatypeDef(t,
-                                            dname,
+                                            name,
                                             datatypes,
                                             sorts,
                                             ops,
@@ -692,18 +689,18 @@ sygusGrammarV1[CVC4::Type & ret,
                                             allow_const,
                                             unresolved_gterm_sym);
          Type unres_t;
-         if (!PARSER_STATE->isUnresolvedType(dname))
+         if (!PARSER_STATE->isUnresolvedType(name))
          {
            // if not unresolved, must be undeclared
-           Debug("parser-sygus") << "Make unresolved type : " << dname
+           Debug("parser-sygus") << "Make unresolved type : " << name
                                  << std::endl;
-           PARSER_STATE->checkDeclaration(dname, CHECK_UNDECLARED, SYM_SORT);
-           unres_t = PARSER_STATE->mkUnresolvedType(dname);
+           PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_SORT);
+           unres_t = PARSER_STATE->mkUnresolvedType(name);
          }
          else
          {
-           Debug("parser-sygus") << "Get sort : " << dname << std::endl;
-           unres_t = PARSER_STATE->getSort(dname);
+           Debug("parser-sygus") << "Get sort : " << name << std::endl;
+           unres_t = PARSER_STATE->getSort(name);
          }
          sygus_to_builtin[unres_t] = t;
          Debug("parser-sygus") << "--- Read sygus grammar " << name
@@ -899,10 +896,6 @@ sygusGTerm[CVC4::SygusGTerm& sgt, const std::string& fun]
         sgt.d_name = name;
         sgt.d_gterm_type = SygusGTerm::gterm_op;
       }else{
-        //prepend function name to base sorts when reading an operator
-        std::stringstream ss;
-        ss << fun << "_" << name;
-        name = ss.str();
         if( PARSER_STATE->isDeclared(name, SYM_SORT) ){
           Debug("parser-sygus") << "Sygus grammar " << fun
                                 << " : nested sort " << name << std::endl;
@@ -957,9 +950,7 @@ sygusGrammar[CVC4::Type & ret,
     {
       Trace("parser-sygus2") << "Declare datatype " << i.first << std::endl;
       // make the datatype, which encodes terms generated by this non-terminal
-      std::stringstream ss;
-      ss << "dt_" << fun << "_" << i.first;
-      std::string dname = ss.str();
+      std::string dname = i.first;
       datatypes.push_back(Datatype(EXPR_MANAGER, dname));
       // make its unresolved type, used for referencing the final version of
       // the datatype