diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index 5e02a101e..7e20d63fb 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -2976,13 +2976,10 @@ 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);
-    two_exp2 = m_arith_util.mk_power(two, exp2);
+    expr_ref res(m), two_exp2(m), signed_exp(m), minus_res(m), sgn_is_1(m);
+    signed_exp = m.mk_ite(exp_is_neg, m_arith_util.mk_uminus(exp2), exp2);
+    two_exp2 = m_arith_util.mk_power(two, signed_exp);
+    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);
diff --git a/src/test/fpa.cpp b/src/test/fpa.cpp
index 217cb641b..fe8aa0377 100644
--- a/src/test/fpa.cpp
+++ b/src/test/fpa.cpp
@@ -58,6 +58,17 @@ static void test_fp_to_real_denormal() {
         "(assert (> (fp.to_real (fp #b0 #b01 #b11111111111111111111111)) 1.0))\n"
         "(check-sat)\n",
         true);
+
+    // Test 5: regression for soundness bug in fp.to_real with QF_FPLRA.
+    // The rational is exactly representable by (fp #b0 #b00000000 #b01001101101110000010001),
+    // so this equality must be satisfiable.
+    run_fp_test(
+        "(set-logic QF_FPLRA)\n"
+        "(set-option :model_validate true)\n"
+        "(assert (= (fp.to_real (fp #b0 #b00000000 #b01001101101110000010001))\n"
+        "           (/ 2546705.0 713623846352979940529142984724747568191373312.0)))\n"
+        "(check-sat)\n",
+        true);
 }
 
 static void test_recfun_defined_function_soundness() {