From aa9aa46b77f048f2865c29e40ed946371fd115ef Mon Sep 17 00:00:00 2001 From: Guy Date: Wed, 23 Mar 2016 12:07:59 -0700 Subject: squash-merge from proof branch --- src/printer/smt2/smt2_printer.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'src/printer/smt2') 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"; -- cgit v1.2.3