diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-05-18 11:36:22 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-05-18 09:36:22 -0700 |
commit | 4987fc9800830d37d22c7e4f31a3f258146cdf66 (patch) | |
tree | 228ffd27ac886f7864a3dabf735bd265fa9605c2 /src/theory/strings/rewrites.cpp | |
parent | c781d274fbaf6f4b3e419140c5834511d6b7c7a0 (diff) |
Fix smt2 printing (#6558)
This fixes bugs related to the smt2 printer where we rely on stream operators for recursive printing calls for certain parts of terms.
Notice that a call to
`out << n;`
within `SmtPrinter::toStream(...)` is wrong since then recursively `n` is printed with the current output language. This means that if one were to ask to print a term in SMT2 format and the output language is not SMT2, then the above call would print `n` in a different format.
This is required to fix bugs in the LFSC proof converter, which explicitly changes the output format to SMT2.
Diffstat (limited to 'src/theory/strings/rewrites.cpp')
0 files changed, 0 insertions, 0 deletions