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.

diff --git a/src/proof/lfsc/lfsc_node_converter.cpp b/src/proof/lfsc/lfsc_node_converter.cpp
index 8c4261f4c17cd29a2a417ae7c50528c774355b56..5eab07dd6063b229695ad73e42c40f6599845400 100644 (file)
--- 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