Fix printing of multiple datatypes (#1872)

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index f9cd7db839c7932c1e1ca81563d267633216b2e2..64ebda07fab79241a11d29b26c9fcb4dda4a99e3 100644 (file)
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -1457,6 +1457,7 @@ static void toStream(std::ostream& out,
           out << ')';
         }
       }
+      firstDatatype = false;
     }
     out << endl << "END;";
   }