Fix smt2 and cvc printers for testers when output and input languages are different.

1 files changed, 5 insertions, 0 deletions

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index be550474c..aa5849960 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -668,6 +668,11 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
            tmp.replace(pos, 8, "::");
         }
         out << tmp;
+      }else if( n.getKind()==kind::APPLY_TESTER ){
+        unsigned cindex = Datatype::indexOf(n.getOperator().toExpr());
+        const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr());
+        out << "is-";
+        toStream(out, Node::fromExpr(dt[cindex].getConstructor()), toDepth < 0 ? toDepth : toDepth - 1, types);
       }else{
         toStream(out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, types);
       }