diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-03 11:56:51 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-08-03 11:56:51 -0500 |
| commit | 243a1d58a139077ecf19ac8a68573e51c08e4621 (patch) | |
| tree | 8fa7ae926032b6c6d7c10b269ba4b32afbf6af62 /src/printer | |
| parent | fbc61a7bbe75c99b29cd238f552c18542deb5c32 (diff) | |
Fix printing issue related to nested quotes (#3154)
Diffstat (limited to 'src/printer')
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
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) |