diff options
Diffstat (limited to 'src/printer/smt2/smt2_printer.cpp')
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index b9b309d4a..56ad9c35a 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -446,6 +446,9 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::REGEXP_EMPTY: out << "re.nostr "; break; case kind::REGEXP_SIGMA: out << "re.allchar "; break; + case kind::CARDINALITY_CONSTRAINT: out << "fmf.card "; break; + case kind::CARDINALITY_VALUE: out << "fmf.card.val "; break; + // bv theory case kind::BITVECTOR_CONCAT: out << "concat "; forceBinary = true; break; case kind::BITVECTOR_AND: out << "bvand "; forceBinary = true; break; |