From 8a3f9efe5856fc07fbc99b9b606397a5079ddd78 Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Thu, 3 May 2018 21:48:19 -0700
Subject: [PATCH] Fix printing of multiple datatypes (#1872)

---
 src/printer/cvc/cvc_printer.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index f9cd7db83..64ebda07f 100644
--- 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;";
   }
-- 
2.30.2