From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 21 Mar 2022 20:27:36 +0000 (-0500)
Subject: Fix LFSC conversion for seq unit (#8353)
X-Git-Tag: cvc5-1.0.0~220
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b0658f29d01deb66de208e0520046024e3892f02;p=cvc5.git

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 3a9e26d55..506bb4440 100644
--- 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