diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp
index c2c888885b..7aee01f024 100644
--- a/src/ast/rewriter/fpa_rewriter.cpp
+++ b/src/ast/rewriter/fpa_rewriter.cpp
@@ -474,6 +474,15 @@ br_status fpa_rewriter::mk_float_eq(expr * arg1, expr * arg2, expr_ref & result)
         return BR_DONE;
     }
 
+    if (m_util.is_numeral(arg1, v1) && !m_fm.is_nan(v1) && !m_fm.is_zero(v1)) {
+        result = m().mk_eq(arg2, arg1);
+        return BR_REWRITE3;
+    }
+    if (m_util.is_numeral(arg2, v2) && !m_fm.is_nan(v2) && !m_fm.is_zero(v2)) {
+        result = m().mk_eq(arg1, arg2);
+        return BR_REWRITE3;
+    }
+
     return BR_FAILED;
 }
 
diff --git a/src/test/fpa.cpp b/src/test/fpa.cpp
index 632865cee6..27c554f995 100644
--- a/src/test/fpa.cpp
+++ b/src/test/fpa.cpp
@@ -95,8 +95,20 @@ static void test_recfun_defined_function_soundness() {
         false);
 }
 
+static void test_to_fp_from_to_real_roundtrip() {
+    run_fp_test(
+        "(declare-fun a () Float32)\n"
+        "(declare-fun t () Float32)\n"
+        "(assert (fp.eq a ((_ to_fp 8 24) RNE 1.0)))\n"
+        "(assert (fp.eq t ((_ to_fp 8 24) RNE 0.8)))\n"
+        "(assert (fp.eq (fp.add RNE a t) ((_ to_fp 8 24) RNE (+ 1.0 (fp.to_real t)))))\n"
+        "(check-sat)\n",
+        true);
+}
+
 void tst_fpa() {
     test_fp_to_real_denormal();
     test_to_fp_from_real_interval();
     test_recfun_defined_function_soundness();
+    test_to_fp_from_to_real_roundtrip();
 }