More array constants and parsing: better error messages, extend to CVC presentation language.

1 files changed, 7 insertions, 0 deletions

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 9b3e83578..2d89d3aff 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -168,6 +168,13 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       break;
     }
 
+    case kind::STORE_ALL: {
+      const ArrayStoreAll& asa = n.getConst<ArrayStoreAll>();
+      out << "ARRAY(" << asa.getType().getIndexType() << " OF "
+          << asa.getType().getConstituentType() << ") : " << asa.getExpr();
+      break;
+    }
+
     default:
       // fall back on whatever operator<< does on underlying type; we
       // might luck out and print something reasonable