diff options
Diffstat (limited to 'src/printer/smt2/smt2_printer.cpp')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 5 |
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); } |