diff options
Diffstat (limited to 'src/printer/smt2/smt2_printer.cpp')
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 657d288e7..14f46db84 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -385,6 +385,8 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, // arrays theory case kind::SELECT: case kind::STORE: + case kind::PARTIAL_SELECT_0: + case kind::PARTIAL_SELECT_1: case kind::ARRAY_TYPE: out << smtKindString(k) << " "; break; // string theory @@ -449,7 +451,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, 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; @@ -732,6 +734,8 @@ static string smtKindString(Kind k) throw() { case kind::SELECT: return "select"; case kind::STORE: return "store"; case kind::ARRAY_TYPE: return "Array"; + case kind::PARTIAL_SELECT_0: return "partial_select_0"; + case kind::PARTIAL_SELECT_1: return "partial_select_1"; // bv theory case kind::BITVECTOR_CONCAT: return "concat"; |