From f18f1bd8c6bcc6827893a2c25e67ca8cf0ddca20 Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Tue, 11 Jan 2022 06:29:49 -0800
Subject: [PATCH] Fix `TypeNode::substitute()` (#7916)

Fixes cvc5/cvc5-projects#397. Fixes
cvc5/cvc5-projects#399. After performing the
substitution on the child node, the result was not added as a child to
the node under construction, resulting in nodes with too few children.
This commit fixes that issue.
---
 src/expr/type_node.cpp         |  2 +-
 test/api/cpp/CMakeLists.txt    |  1 +
 test/api/cpp/proj-issue399.cpp | 39 ++++++++++++++++++++++++++++++++++
 3 files changed, 41 insertions(+), 1 deletion(-)
 create mode 100644 test/api/cpp/proj-issue399.cpp

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 8358facac..b03e9bc45 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -57,7 +57,7 @@ TypeNode TypeNode::substitute(
     }
     else
     {
-      (*j).substitute(type, replacement);
+      nb << (*j).substitute(type, replacement);
     }
   }
 
diff --git a/test/api/cpp/CMakeLists.txt b/test/api/cpp/CMakeLists.txt
index 929c5bef2..8b860ec1d 100644
--- a/test/api/cpp/CMakeLists.txt
+++ b/test/api/cpp/CMakeLists.txt
@@ -56,3 +56,4 @@ cvc5_add_api_test(proj-issue306)
 cvc5_add_api_test(proj-issue334)
 cvc5_add_api_test(proj-issue344)
 cvc5_add_api_test(proj-issue345)
+cvc5_add_api_test(proj-issue399)
diff --git a/test/api/cpp/proj-issue399.cpp b/test/api/cpp/proj-issue399.cpp
new file mode 100644
index 000000000..03ed55c3e
--- /dev/null
+++ b/test/api/cpp/proj-issue399.cpp
@@ -0,0 +1,39 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andres Noetzli
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Test for project issue #399
+ *
+ */
+
+#include <cassert>
+
+#include "api/cpp/cvc5.h"
+
+using namespace cvc5::api;
+
+int main(void)
+{
+  Solver slv;
+  Sort s1 = slv.mkUninterpretedSort("_u0");
+  Sort s2 = slv.getStringSort();
+  Sort _p2 = slv.mkParamSort("_p2");
+  Sort _p3 = slv.mkParamSort("_p3");
+  DatatypeDecl _dt1 = slv.mkDatatypeDecl("_dt1", {_p2, _p3});
+  DatatypeConstructorDecl _cons21 = slv.mkDatatypeConstructorDecl("_cons21");
+  _cons21.addSelector("_sel16", _p2);
+  _dt1.addConstructor(_cons21);
+  Sort s3 = slv.mkDatatypeSort(_dt1);
+  Sort s4 = slv.mkBagSort(s2);
+  Sort s5 = slv.mkArraySort(s1, s4);
+  Sort s9 = s3.instantiate({s4, s4});
+  (void)s5.substitute({s4}, {s9});
+}
-- 
2.30.2