summaryrefslogtreecommitdiff
path: root/src/expr/uninterpreted_constant.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr/uninterpreted_constant.cpp')
-rw-r--r--src/expr/uninterpreted_constant.cpp10
1 files changed, 1 insertions, 9 deletions
diff --git a/src/expr/uninterpreted_constant.cpp b/src/expr/uninterpreted_constant.cpp
index 2187d9cdf..9898bcb3f 100644
--- 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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback