Use the correct casting kind in the CVC5 formula creator function decl
map
@@ -460,8 +460,8 @@ public class CVC5FormulaCreator extends FormulaCreator<Term, Sort, Solver, Term>
.put(Kind.FLOATINGPOINT_TO_SBV, FunctionDeclarationKind.FP_CASTTO_SBV)
.put(Kind.FLOATINGPOINT_TO_UBV, FunctionDeclarationKind.FP_CASTTO_UBV)
.put(Kind.FLOATINGPOINT_TO_FP_FROM_FP, FunctionDeclarationKind.FP_CASTTO_FP)
- .put(Kind.FLOATINGPOINT_TO_SBV, FunctionDeclarationKind.BV_SCASTTO_FP)
- .put(Kind.FLOATINGPOINT_TO_UBV, FunctionDeclarationKind.BV_UCASTTO_FP)
+ .put(Kind.FLOATINGPOINT_TO_FP_FROM_SBV, FunctionDeclarationKind.BV_SCASTTO_FP)
+ .put(Kind.FLOATINGPOINT_TO_FP_FROM_UBV, FunctionDeclarationKind.BV_UCASTTO_FP)
.put(Kind.FLOATINGPOINT_IS_NAN, FunctionDeclarationKind.FP_IS_NAN)
.put(Kind.FLOATINGPOINT_IS_NEG, FunctionDeclarationKind.FP_IS_NEGATIVE)
.put(Kind.FLOATINGPOINT_IS_INF, FunctionDeclarationKind.FP_IS_INF)
