summaryrefslogtreecommitdiff
path: root/src/util
diff options
context:
space:
mode:
authorAbdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com>2021-02-01 12:40:58 -0600
committerGitHub <noreply@github.com>2021-02-01 12:40:58 -0600
commita85fec1cc9fc4f42dcfefd8c27171d8ce5647449 (patch)
tree4b6820199f4f2763b821de6eda1bfc839448122b /src/util
parentc0937f742479d8a5054e42597da9447d55e876c0 (diff)
Avoid calling the printers while converting sexpr to string. (#5842)
This PR modifies sexprToString to use Term::getString to get string constants instead of Term::toString, which depends on the output language. The previous behavior caused CVC4 to crash when AST is picked as the output language.
Diffstat (limited to 'src/util')
-rw-r--r--src/util/string.cpp2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/util/string.cpp b/src/util/string.cpp
index e625c2199..893bf9825 100644
--- a/src/util/string.cpp
+++ b/src/util/string.cpp
@@ -510,7 +510,7 @@ Rational String::toNumber() const
}
std::ostream &operator<<(std::ostream &os, const String &s) {
- return os << "\"" << s.toString(true) << "\"";
+ return os << "\"" << s.toString() << "\"";
}
} // namespace CVC4
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback