Fix type issue for FP constants in LFSC node converter (#8612)

Fixes type errors in debug builds.

diff --git a/src/proof/lfsc/lfsc_node_converter.cpp b/src/proof/lfsc/lfsc_node_converter.cpp
index baf3b44aca7e54b6733d9b95756eef9894e30dcf..25ae48d9213244280fc97d7a6dbb4b64d2a95f63 100644 (file)
--- a/src/proof/lfsc/lfsc_node_converter.cpp
+++ b/src/proof/lfsc/lfsc_node_converter.cpp
@@ -273,8 +273,8 @@ Node LfscNodeConverter::postConvert(Node n)
     Node sn = convert(nm->mkConst(s));
     Node en = convert(nm->mkConst(e));
     Node in = convert(nm->mkConst(i));
-    TypeNode btn = nm->booleanType();
-    TypeNode tnv = nm->mkFunctionType({btn, btn, btn}, tn);
+    TypeNode tnv =
+        nm->mkFunctionType({sn.getType(), en.getType(), in.getType()}, tn);
     Node bconstf = getSymbolInternal(k, tnv, "fp");
     return nm->mkNode(APPLY_UF, {bconstf, sn, en, in});
   }