diff --git a/tests/float/test_float3.ae b/tests/float/test_float3.ae
new file mode 100644
index 0000000000..3067a37b52
--- /dev/null
+++ b/tests/float/test_float3.ae
@@ -0,0 +1,5 @@
+logic x : real
+
+axiom ax : 1.0 <= x
+
+goal g : float(4, 4, NearestTiesToEven, 1.0) <= float(4, 4, NearestTiesToEven, x)
\ No newline at end of file
diff --git a/tests/float/test_float3.expected b/tests/float/test_float3.expected
new file mode 100644
index 0000000000..6f99ff0f44
--- /dev/null
+++ b/tests/float/test_float3.expected
@@ -0,0 +1,2 @@
+
+unsat