From 8e7cd8e1381a23daa0b7680c70e6b2254acc1580 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Fri, 26 Jun 2026 17:11:34 +0000
Subject: [PATCH] Add alias-based FP.eq round-trip regression test

---
 src/test/fpa.cpp | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/src/test/fpa.cpp b/src/test/fpa.cpp
index 27c554f995..2fc9ce0cde 100644
--- a/src/test/fpa.cpp
+++ b/src/test/fpa.cpp
@@ -106,9 +106,25 @@ static void test_to_fp_from_to_real_roundtrip() {
         true);
 }
 
+static void test_to_fp_from_to_real_roundtrip_with_aliases() {
+    run_fp_test(
+        "(declare-fun a () Float32)\n"
+        "(declare-fun t () Float32)\n"
+        "(declare-fun one () Float32)\n"
+        "(declare-fun c08 () Float32)\n"
+        "(assert (= one ((_ to_fp 8 24) RNE 1.0)))\n"
+        "(assert (= c08 ((_ to_fp 8 24) RNE 0.8)))\n"
+        "(assert (fp.eq a one))\n"
+        "(assert (fp.eq t c08))\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();
+    test_to_fp_from_to_real_roundtrip_with_aliases();
 }