From 8e0fce94790249ff7aff84ff4500bb96e2ebb9e9 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Tue, 1 Nov 2016 13:20:49 -0500
Subject: Working memory leak free version, changes interface to pointers.

---
 src/printer/cvc/cvc_printer.cpp | 18 ++++++++++--------
 1 file changed, 10 insertions(+), 8 deletions(-)

(limited to 'src/printer/cvc')

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 550f87081..11cf7dd11 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -163,7 +163,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       break;
 
     case kind::DATATYPE_TYPE: {
-      const Datatype& dt = n.getConst<Datatype>();
+      const Datatype& dt = (NodeManager::currentNM()->getDatatypeForIndex( n.getConst< DatatypeIndexConstant >().getIndex() ));
       if( dt.isTuple() ){
         out << '[';
         for (unsigned i = 0; i < dt[0].getNumArgs(); ++ i) {
@@ -333,15 +333,17 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       break;
 
     // DATATYPES
-    case kind::PARAMETRIC_DATATYPE:
-      out << n[0].getConst<Datatype>().getName() << '[';
-      for(unsigned i = 1; i < n.getNumChildren(); ++i) {
-        if(i > 1) {
-          out << ',';
+    case kind::PARAMETRIC_DATATYPE: {
+        const Datatype & dt = (NodeManager::currentNM()->getDatatypeForIndex( n[0].getConst< DatatypeIndexConstant >().getIndex() ));
+        out << dt.getName() << '[';
+        for(unsigned i = 1; i < n.getNumChildren(); ++i) {
+          if(i > 1) {
+            out << ',';
+          }
+          out << n[i];
         }
-        out << n[i];
+        out << ']';
       }
-      out << ']';
       return;
       break;
     case kind::APPLY_TYPE_ASCRIPTION: {
-- 
cgit v1.2.3