From 82f9ba130f855c1a7efb75264728a83cf0fce31a Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 13 Apr 2022 09:56:43 -0500
Subject: [PATCH] Fix type issue for FP constants in LFSC node converter
 (#8612)

Fixes type errors in debug builds.
---
 src/proof/lfsc/lfsc_node_converter.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/proof/lfsc/lfsc_node_converter.cpp b/src/proof/lfsc/lfsc_node_converter.cpp
index baf3b44ac..25ae48d92 100644
--- 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});
   }
-- 
2.30.2