Do not rename uninterpreted constants (#2098)

diff --git a/src/expr/uninterpreted_constant.cpp b/src/expr/uninterpreted_constant.cpp
index 2187d9cdf4bb244372b23c0848006d3d516edc78..9898bcb3f22a8bfc72b61925fc8b224c3e9e9cb0 100644 (file)
--- a/src/expr/uninterpreted_constant.cpp
+++ b/src/expr/uninterpreted_constant.cpp
@@ -34,15 +34,7 @@ UninterpretedConstant::UninterpretedConstant(Type type, Integer index)
 }
 
 std::ostream& operator<<(std::ostream& out, const UninterpretedConstant& uc) {
-  stringstream ss;
-  ss << uc.getType();
-  string t = ss.str();
-  size_t i = 0;
-  // replace everything that isn't in [a-zA-Z0-9_] with an _
-  while((i = t.find_first_not_of("abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ1234567890_", i)) != string::npos) {
-    t.replace(i, 1, 1, '_');
-  }
-  return out << "uc_" << t << '_' << uc.getIndex();
+  return out << "uc_" << uc.getType() << '_' << uc.getIndex();
 }
 
 }/* CVC4 namespace */

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index f6d3cc743ba99379382ec1feb53109b3113a57b1..0e1df15b55d481c02e0f6c1f93d9b5bb5e672130 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -267,7 +267,9 @@ void Smt2Printer::toStream(std::ostream& out,
 
     case kind::UNINTERPRETED_CONSTANT: {
       const UninterpretedConstant& uc = n.getConst<UninterpretedConstant>();
-      out << '@' << uc;
+      std::stringstream ss;
+      ss << '@' << uc;
+      out << maybeQuoteSymbol(ss.str());
       break;
     }