From 7ed586537b7767dee79a85e2754a12570328211c Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Tue, 11 Jan 2022 09:19:15 -0800
Subject: [PATCH] Fix `TypeNode::substitute()` for type constants (#7920)

Fixes cvc5/cvc5-projects#395. The
TypeNode::substitute() method did not account for type constants such
as the Boolean type and was trying to use a NodeBuilder to build such
constants instead. This commit fixes the issue by adding a special case
for types without children.
---
 src/expr/type_node.cpp         |  9 +++++++++
 test/api/cpp/CMakeLists.txt    |  1 +
 test/api/cpp/proj-issue395.cpp | 30 ++++++++++++++++++++++++++++++
 3 files changed, 40 insertions(+)
 create mode 100644 test/api/cpp/proj-issue395.cpp

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index b03e9bc45..de85dfb06 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -42,6 +42,15 @@ TypeNode TypeNode::substitute(
   if(i != cache.end()) {
     return (*i).second;
   }
+  else if (*this == type)
+  {
+    return replacement;
+  }
+
+  if (d_nv->getNumChildren() == 0)
+  {
+    return *this;
+  }
 
   // otherwise compute
   NodeBuilder nb(getKind());
diff --git a/test/api/cpp/CMakeLists.txt b/test/api/cpp/CMakeLists.txt
index 8b860ec1d..0c9bcc463 100644
--- a/test/api/cpp/CMakeLists.txt
+++ b/test/api/cpp/CMakeLists.txt
@@ -56,4 +56,5 @@ 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-issue395)
 cvc5_add_api_test(proj-issue399)
diff --git a/test/api/cpp/proj-issue395.cpp b/test/api/cpp/proj-issue395.cpp
new file mode 100644
index 000000000..17cac8cb1
--- /dev/null
+++ b/test/api/cpp/proj-issue395.cpp
@@ -0,0 +1,30 @@
+/******************************************************************************
+ * 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 #395
+ *
+ */
+
+#include <cassert>
+
+#include "api/cpp/cvc5.h"
+
+using namespace cvc5::api;
+
+int main(void)
+{
+  Solver slv;
+  Sort s1 = slv.getBooleanSort();
+  Sort s2 = slv.getIntegerSort();
+  Sort s5 = slv.mkFunctionSort({s2}, s1);
+  (void) s5.substitute({s1}, {s1});
+}
-- 
2.30.2