From 61da690d4a441f3c754ce25d64e5b8ff9d0080ff Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 3 May 2022 15:58:34 -0500
Subject: [PATCH] Fix LFSC node converter for 0-ary tuples (#8706)

Was missing 0-ary Tuple case for type-as-node.

Also removes a spurious check in the user-defined sorts case.

Fixes some issues in the nightlies.
---
 src/proof/lfsc/lfsc_node_converter.cpp | 46 ++++++++++++++------------
 1 file changed, 24 insertions(+), 22 deletions(-)

diff --git a/src/proof/lfsc/lfsc_node_converter.cpp b/src/proof/lfsc/lfsc_node_converter.cpp
index 8c4261f4c..5eab07dd6 100644
--- a/src/proof/lfsc/lfsc_node_converter.cpp
+++ b/src/proof/lfsc/lfsc_node_converter.cpp
@@ -575,35 +575,37 @@ TypeNode LfscNodeConverter::postConvertType(TypeNode tn)
       cur = nm->mkSortConstructor(ss.str(), nargs);
       cur = nm->mkSort(cur, convTypes);
     }
+    else
+    {
+      // no need to convert type for tuples of size 0,
+      // type as node is simple
+      tnn = getSymbolInternal(k, d_sortType, "Tuple");
+    }
   }
   else if (tn.getNumChildren() == 0)
   {
     Assert(!tn.isTuple());
     // an uninterpreted sort, or an uninstantiatied (maybe parametric) datatype
     d_declTypes.insert(tn);
-    if (tnn.isNull())
+    std::stringstream ss;
+    options::ioutils::applyOutputLang(ss, Language::LANG_SMTLIB_V2_6);
+    tn.toStream(ss);
+    if (tn.isUninterpretedSortConstructor())
     {
-      std::stringstream ss;
-      options::ioutils::applyOutputLang(ss, Language::LANG_SMTLIB_V2_6);
-      tn.toStream(ss);
-      if (tn.isUninterpretedSortConstructor())
-      {
-        std::string s = getNameForUserNameOfInternal(tn.getId(), ss.str());
-        tnn = getSymbolInternal(k, d_sortType, s, false);
-        cur =
-            nm->mkSortConstructor(s, tn.getUninterpretedSortConstructorArity());
-      }
-      else if (tn.isUninterpretedSort() || tn.isDatatype())
-      {
-        std::string s = getNameForUserNameOfInternal(tn.getId(), ss.str());
-        tnn = getSymbolInternal(k, d_sortType, s, false);
-        cur = nm->mkSort(s);
-      }
-      else
-      {
-        // all other builtin type constants, e.g. Int
-        tnn = getSymbolInternal(k, d_sortType, ss.str());
-      }
+      std::string s = getNameForUserNameOfInternal(tn.getId(), ss.str());
+      tnn = getSymbolInternal(k, d_sortType, s, false);
+      cur = nm->mkSortConstructor(s, tn.getUninterpretedSortConstructorArity());
+    }
+    else if (tn.isUninterpretedSort() || tn.isDatatype())
+    {
+      std::string s = getNameForUserNameOfInternal(tn.getId(), ss.str());
+      tnn = getSymbolInternal(k, d_sortType, s, false);
+      cur = nm->mkSort(s);
+    }
+    else
+    {
+      // all other builtin type constants, e.g. Int
+      tnn = getSymbolInternal(k, d_sortType, ss.str());
     }
   }
   else
-- 
2.30.2