From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 13 Apr 2022 14:56:43 +0000 (-0500)
Subject: Fix type issue for FP constants in LFSC node converter (#8612)
X-Git-Tag: cvc5-1.0.1~267
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=82f9ba130f855c1a7efb75264728a83cf0fce31a;p=cvc5.git

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 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});
   }