Fix LFSC conversion for seq unit (#8353)

diff --git a/src/proof/lfsc/lfsc_node_converter.cpp b/src/proof/lfsc/lfsc_node_converter.cpp
index 3a9e26d559d02cba3deaf928073a5fb7486daeb6..506bb44406299eb27884b0722c94e7934e085ffd 100644 (file)
--- a/src/proof/lfsc/lfsc_node_converter.cpp
+++ b/src/proof/lfsc/lfsc_node_converter.cpp
@@ -303,7 +303,8 @@ Node LfscNodeConverter::postConvert(Node n)
     std::vector<Node> vecu;
     for (size_t i = 0, size = charVec.size(); i < size; i++)
     {
-      Node u = nm->mkNode(SEQ_UNIT, postConvert(charVec[size - (i + 1)]));
+      Node u = nm->mkSeqUnit(tn.getSequenceElementType(),
+                             postConvert(charVec[size - (i + 1)]));
       if (size == 1)
       {
         // singleton case