Fix smt2 printing (#6558)

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.