From 4be7685978cc9050930fb4036c6bdf9e868722f4 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 1 Sep 2017 11:03:53 +0100
Subject: [PATCH] Do not add an "l" prefix to double constants when
 double==long double

---
 regression/cbmc/Float24/main.c    |  6 ++++++
 regression/cbmc/Float24/test.desc | 10 ++++++++++
 src/ansi-c/expr2c.cpp             |  3 ++-
 3 files changed, 18 insertions(+), 1 deletion(-)
 create mode 100644 regression/cbmc/Float24/main.c
 create mode 100644 regression/cbmc/Float24/test.desc

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 &&