1 files changed, 10 insertions, 10 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 5d2ffb9db..7937e82f3 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -741,25 +741,25 @@ void CvcPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw
 
 }/* CvcPrinter::toStream(CommandStatus*) */
 
-void CvcPrinter::toStream(std::ostream& out, Model* m, const Command* c) const throw() {
-  theory::TheoryModel* tm = (theory::TheoryModel*)m;
+void CvcPrinter::toStream(std::ostream& out, Model& m, const Command* c) const throw() {
+  theory::TheoryModel& tm = (theory::TheoryModel&) m;
   if(dynamic_cast<const DeclareTypeCommand*>(c) != NULL) {
     TypeNode tn = TypeNode::fromType( ((const DeclareTypeCommand*)c)->getType() );
     if( tn.isSort() ){
       //print the cardinality
-      if( tm->d_rep_set.d_type_reps.find( tn )!=tm->d_rep_set.d_type_reps.end() ){
-        out << "; cardinality of " << tn << " is " << tm->d_rep_set.d_type_reps[tn].size() << std::endl;
+      if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
+        out << "; cardinality of " << tn << " is " << (*tm.d_rep_set.d_type_reps.find(tn)).second.size() << std::endl;
       }
     }
     out << c << std::endl;
     if( tn.isSort() ){
       //print the representatives
-      if( tm->d_rep_set.d_type_reps.find( tn )!=tm->d_rep_set.d_type_reps.end() ){
-        for( size_t i=0; i<tm->d_rep_set.d_type_reps[tn].size(); i++ ){
-          if( tm->d_rep_set.d_type_reps[tn][i].isVar() ){
-            out << tm->d_rep_set.d_type_reps[tn][i] << " : " << tn << ";" << std::endl;
+      if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
+        for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){
+          if( (*tm.d_rep_set.d_type_reps.find(tn)).second[i].isVar() ){
+            out << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << " : " << tn << ";" << std::endl;
           }else{
-            out << "% rep: " << tm->d_rep_set.d_type_reps[tn][i] << std::endl;
+            out << "% rep: " << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << std::endl;
           }
         }
       }
@@ -778,7 +778,7 @@ void CvcPrinter::toStream(std::ostream& out, Model* m, const Command* c) const t
     }else{
       out << tn;
     }
-    out << " = " << tm->getValue( n ) << ";" << std::endl;
+    out << " = " << tm.getValue( n ) << ";" << std::endl;
 
 /*
     //for table format (work in progress)