Fix printing issue related to nested quotes (#3154)

3 files changed, 16 insertions, 3 deletions

diff --git a/src/expr/uninterpreted_constant.cpp b/src/expr/uninterpreted_constant.cpp
index 5c9daf784..64180c377 100644
--- a/src/expr/uninterpreted_constant.cpp
+++ b/src/expr/uninterpreted_constant.cpp
@@ -16,6 +16,7 @@
 
 #include "expr/uninterpreted_constant.h"
 
+#include <algorithm>
 #include <iostream>
 #include <sstream>
 #include <string>
@@ -34,7 +35,18 @@ UninterpretedConstant::UninterpretedConstant(Type type, Integer index)
 }
 
 std::ostream& operator<<(std::ostream& out, const UninterpretedConstant& uc) {
-  return out << "uc_" << uc.getType() << '_' << uc.getIndex();
+  std::stringstream ss;
+  ss << uc.getType();
+  std::string st(ss.str());
+  // must remove delimiting quotes from the name of the type
+  // this prevents us from printing symbols like |@uc_|T|_n|
+  std::string q("|");
+  size_t pos;
+  while ((pos = st.find(q)) != std::string::npos)
+  {
+    st.replace(pos, 1, "");
+  }
+  return out << "uc_" << st.c_str() << "_" << uc.getIndex();
 }
 
 }/* CVC4 namespace */
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index fd8b4ce85..dbb89d857 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1760,7 +1760,8 @@ static void toStreamRational(std::ostream& out,
 
 static void toStream(std::ostream& out, const DeclareTypeCommand* c)
 {
-  out << "(declare-sort " << c->getSymbol() << " " << c->getArity() << ")";
+  out << "(declare-sort " << maybeQuoteSymbol(c->getSymbol()) << " "
+      << c->getArity() << ")";
 }
 
 static void toStream(std::ostream& out, const DefineTypeCommand* c)
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index b032dfec4..c4be41084 100644
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -1005,7 +1005,7 @@ void TheoryEngineModelBuilder::assignFunction(TheoryModel* m, Node f)
     ufmt.simplify();
   }
   std::stringstream ss;
-  ss << "_arg_" << f << "_";
+  ss << "_arg_";
   Node val = ufmt.getFunctionValue(ss.str().c_str(), condenseFuncValues);
   m->assignFunctionDefinition(f, val);
   // ufmt.debugPrint( std::cout, m );