diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-09-29 19:37:22 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-09-30 02:37:22 +0000 |
| commit | 181cac8b630609dc982887c5c4cea1e46b319811 (patch) | |
| tree | 029c5fd599649c2512bcaeda7ec141501dbc8a09 /src/printer/smt2/smt2_printer.cpp | |
| parent | 9cb5726a3a26c329ef5310b0b461b03dd0864799 (diff) | |
[Printer] Only quote `set-info` value if necessary (#7262)
PR #7240 changed the printing of set-info to always include quote the
value. This commit changes the policy to only quote a symbol if
necessary using existing an existing helper method. Otherwise,
(set-info :status sat) is for example printed as (set-info :status |sat|), which is a bit unusual and may break certain scripts.
Diffstat (limited to 'src/printer/smt2/smt2_printer.cpp')
| -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 e6aff1ace..fd98bdeca 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1622,7 +1622,8 @@ void Smt2Printer::toStreamCmdSetInfo(std::ostream& out, const std::string& flag, const std::string& value) const { - out << "(set-info :" << flag << " |" << value << "|)" << std::endl; + out << "(set-info :" << flag << " " << cvc5::quoteSymbol(value) << ")" + << std::endl; } void Smt2Printer::toStreamCmdGetInfo(std::ostream& out, |