exportTo only if needed for --sygus-rr-synth-check

With this commit, we only use an SmtEngine with a separate ExprManager
for --sygus-rr-synth-check if necessary (currently, this is only the
case when --sygus-rr-synth-check-timeout is active). The reason for
this is that we do not support exportTo for all kinds. Additionally,
this commit adds support for exporting floating-point types and adds a
check that throws an exception if an unsupported type is being
exported (previously, it just crashed). Finally, it fixes a minor
issue with -d export, where an expression was printed while the wrong
ExprManager was active, leading to an assertion failure when getting
the types of expressions (which is required for operators like
equality where the sort of the children is not fixed).

0 files changed, 0 insertions, 0 deletions