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

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index b7e1520b78b96063d8ad0da5af89e227750dbbad..4f0d4b6644eb7a6180261967129dcf5ab49eb75b 100644 (file)
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -398,8 +398,13 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
         }
       }
       break;
-    case kind::APPLY_TESTER:
-      toStream(op, n.getOperator(), depth, types, false);
+    case kind::APPLY_TESTER: {
+      Assert( !n.getType().isTuple() && !n.getType().isRecord() );
+      op << "is_";
+      unsigned cindex = Datatype::indexOf(n.getOperator().toExpr());
+      const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr());
+      toStream(op, Node::fromExpr(dt[cindex].getConstructor()), depth, types, false);
+    }
       break;
     case kind::CONSTRUCTOR_TYPE:
     case kind::SELECTOR_TYPE:

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index be550474c7138c6dd72122879b7d4bcdb525114e..aa5849960718400d32dfe92f98fed154993d9a91 100644 (file)
--- 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);
       }