diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index 5e02a101e..d7ba25904 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -2976,13 +2976,11 @@ void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * ar
         prev_bit = bit;
     }
 
-    expr_ref one_div_exp2(m);
-    one_div_exp2 = m_arith_util.mk_div(one, exp2);
-    exp2 = m.mk_ite(exp_is_neg, one_div_exp2, exp2);
-    dbg_decouple("fpa2bv_to_real_exp2", exp2);
-
-    expr_ref res(m), two_exp2(m), minus_res(m), sgn_is_1(m);
+    expr_ref res(m), two_exp2(m), one_div_two_exp2(m), minus_res(m), sgn_is_1(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);
     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);
@@ -2990,7 +2988,7 @@ void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * ar
     dbg_decouple("fpa2bv_to_real_sig_times_exp2", res);
 
     TRACE(fpa2bv_to_real, tout << "rsig = " << mk_ismt2_pp(rsig, m) << std::endl;
-    tout << "exp2 = " << mk_ismt2_pp(exp2, m) << std::endl;);
+    tout << "two_exp2 = " << mk_ismt2_pp(two_exp2, m) << std::endl;);
 
     expr_ref unspec(m);
     mk_to_real_unspecified(f, num, args, unspec);
diff --git a/src/test/fpa.cpp b/src/test/fpa.cpp
index 217cb641b..632865cee 100644
--- a/src/test/fpa.cpp
+++ b/src/test/fpa.cpp
@@ -60,6 +60,28 @@ static void test_fp_to_real_denormal() {
         true);
 }
 
+// Regression test for soundness bug in to_fp (from real) with symbolic real interval.
+// When the rounding mode is RTZ and the real variable is constrained to an interval
+// that includes the exact rational value of a float, Z3 should return SAT.
+// This was broken because mk_to_real computed 2^(1/|exp|) instead of 1/(2^|exp|)
+// for floats with negative exponents, causing a conflict in the NRA solver.
+static void test_to_fp_from_real_interval() {
+    // The interval (-4127125/16777216, -16508499/67108864] contains -16508499/67108864
+    // which is the exact rational value of fp #b1 #b01111100 #b11110111110011001010011.
+    // to_fp(RTZ, r) for r in this closed interval must equal that float.
+    run_fp_test(
+        "(set-logic QF_FPLRA)\n"
+        "(declare-const x Float32)\n"
+        "(assert (= x (fp #b1 #b01111100 #b11110111110011001010011)))\n"
+        "(declare-const r Real)\n"
+        "(assert (and (> r (- (/ 4127125.0 16777216.0))) (<= r (- (/ 16508499.0 67108864.0)))))\n"
+        "(declare-const w Float32)\n"
+        "(assert (= w ((_ to_fp 8 24) RTZ r)))\n"
+        "(assert (= x w))\n"
+        "(check-sat)\n",
+        true);
+}
+
 static void test_recfun_defined_function_soundness() {
     run_fp_test(
         "(set-option :model_validate true)\n"
@@ -75,5 +97,6 @@ static void test_recfun_defined_function_soundness() {
 
 void tst_fpa() {
     test_fp_to_real_denormal();
+    test_to_fp_from_real_interval();
     test_recfun_defined_function_soundness();
 }