From 477b90228e57d619cd848c19feee646109c4a2c9 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt>
Date: Sun, 20 Nov 2022 19:19:12 +0000
Subject: [PATCH] fix #6460: crash in mk_to_ieee_bv_i
---
src/ast/fpa/fpa2bv_converter.cpp | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index 21c71c8a9..c456da29b 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -3288,7 +3288,7 @@ void fpa2bv_converter::mk_to_ieee_bv_unspecified(func_decl * f, unsigned num, ex
void fpa2bv_converter::mk_to_ieee_bv_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result)
{
func_decl_ref fu(m.mk_func_decl(f->get_family_id(), OP_FPA_TO_IEEE_BV, 0, nullptr, num, args), m);
- mk_to_bv(fu, num, args, true, result);
+ mk_to_ieee_bv(fu, num, args, result);
}
void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args, bool is_signed, expr_ref & result) {