Fix issues with printing parametric datatypes in smt2 (#2213)

1 files changed, 9 insertions, 5 deletions

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 1f9c3fd2b..47124a589 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -324,10 +324,13 @@ SortType Parser::mkSort(const std::string& name, uint32_t flags) {
 }
 
 SortConstructorType Parser::mkSortConstructor(const std::string& name,
-                                              size_t arity) {
+                                              size_t arity,
+                                              uint32_t flags)
+{
   Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")"
                   << std::endl;
-  SortConstructorType type = d_exprManager->mkSortConstructor(name, arity);
+  SortConstructorType type =
+      d_exprManager->mkSortConstructor(name, arity, flags);
   defineType(name, vector<Type>(arity), type);
   return type;
 }
@@ -340,7 +343,8 @@ SortType Parser::mkUnresolvedType(const std::string& name) {
 
 SortConstructorType Parser::mkUnresolvedTypeConstructor(const std::string& name,
                                                         size_t arity) {
-  SortConstructorType unresolved = mkSortConstructor(name, arity);
+  SortConstructorType unresolved =
+      mkSortConstructor(name, arity, ExprManager::SORT_FLAG_PLACEHOLDER);
   d_unresolved.insert(unresolved);
   return unresolved;
 }
@@ -349,8 +353,8 @@ SortConstructorType Parser::mkUnresolvedTypeConstructor(
     const std::string& name, const std::vector<Type>& params) {
   Debug("parser") << "newSortConstructor(P)(" << name << ", " << params.size()
                   << ")" << std::endl;
-  SortConstructorType unresolved =
-      d_exprManager->mkSortConstructor(name, params.size());
+  SortConstructorType unresolved = d_exprManager->mkSortConstructor(
+      name, params.size(), ExprManager::SORT_FLAG_PLACEHOLDER);
   defineType(name, params, unresolved);
   Type t = getSort(name, params);
   d_unresolved.insert(unresolved);