From e5e7cea7671c6b6d7c845985f65958a10552fb91 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Wed, 13 May 2026 00:12:06 +0000
Subject: [PATCH] Improve readability: split variable declaration in mk_to_real

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/56265d81-608a-4768-8c4d-30bd740d89fb

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/ast/fpa/fpa2bv_converter.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index d7ba25904..d2431174e 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -2976,11 +2976,12 @@ void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * ar
         prev_bit = bit;
     }
 
-    expr_ref res(m), two_exp2(m), one_div_two_exp2(m), minus_res(m), sgn_is_1(m);
+    expr_ref two_exp2(m), one_div_two_exp2(m);
     two_exp2 = m_arith_util.mk_power(two, exp2);
     one_div_two_exp2 = m_arith_util.mk_div(one, two_exp2);
     two_exp2 = m.mk_ite(exp_is_neg, one_div_two_exp2, two_exp2);
     dbg_decouple("fpa2bv_to_real_exp2", two_exp2);
+    expr_ref res(m), minus_res(m), sgn_is_1(m);
     res = m_arith_util.mk_mul(rsig, two_exp2);
     minus_res = m_arith_util.mk_uminus(res);
     sgn_is_1 = m.mk_eq(sgn, bv1);