diff --git a/regression/cbmc/Float-rounding/compile_time_rounding.c b/regression/cbmc/Float-rounding/compile_time_rounding.c
new file mode 100644
index 00000000000..42debe404ed
--- /dev/null
+++ b/regression/cbmc/Float-rounding/compile_time_rounding.c
@@ -0,0 +1,10 @@
+#include <assert.h>
+
+double THREE = 3;
+
+int main()
+{
+  // the rounding mode of the two '3' literals during
+  // the conversion to double should match
+  assert(THREE == 3);
+}
diff --git a/regression/cbmc/Float-rounding/compile_time_rounding.desc b/regression/cbmc/Float-rounding/compile_time_rounding.desc
new file mode 100644
index 00000000000..0a0acb29197
--- /dev/null
+++ b/regression/cbmc/Float-rounding/compile_time_rounding.desc
@@ -0,0 +1,11 @@
+KNOWNBUG
+compile_time_rounding.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+the rounding mode of the two '3' literals during
+the conversion to double should match