Fix printing issue related to nested quotes (#3154)

1 files changed, 13 insertions, 1 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 */