summaryrefslogtreecommitdiff
path: root/src/theory/strings/rewrites.cpp
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2021-05-18 11:36:22 -0500
committerGitHub <noreply@github.com>2021-05-18 09:36:22 -0700
commit4987fc9800830d37d22c7e4f31a3f258146cdf66 (patch)
tree228ffd27ac886f7864a3dabf735bd265fa9605c2 /src/theory/strings/rewrites.cpp
parentc781d274fbaf6f4b3e419140c5834511d6b7c7a0 (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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback