diff --git a/regression/cbmc/Float24/main.c b/regression/cbmc/Float24/main.c
new file mode 100644
index 00000000000..0e12f24780a
--- /dev/null
+++ b/regression/cbmc/Float24/main.c
@@ -0,0 +1,6 @@
+int main()
+{
+  double d=5.1;
+  __CPROVER_assert(0, "");
+  return 0;
+}
diff --git a/regression/cbmc/Float24/test.desc b/regression/cbmc/Float24/test.desc
new file mode 100644
index 00000000000..6a7c97325db
--- /dev/null
+++ b/regression/cbmc/Float24/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--win32 --xml-ui
+^EXIT=10$
+^SIGNAL=0$
+VERIFICATION FAILED
+<full_lhs_value>5\.1</full_lhs_value>
+--
+^warning: ignoring
+<full_lhs_value>5\.1l</full_lhs_value>
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index eecc856a0f7..b889476a73f 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -1859,7 +1859,8 @@ std::string expr2ct::convert_constant(
       // ANSI-C: double is default; float/long-double require annotation
       if(src.type()==float_type())
         dest+='f';
-      else if(src.type()==long_double_type())
+      else if(src.type()==long_double_type() &&
+              double_type()!=long_double_type())
         dest+='l';
     }
     else if(dest.size()==4 &&