diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp
index 21f6fc41f4a..545e9b0e59d 100644
--- a/src/ansi-c/ansi_c_internal_additions.cpp
+++ b/src/ansi-c/ansi_c_internal_additions.cpp
@@ -195,10 +195,20 @@ void ansi_c_internal_additions(std::string &code)
        config.ansi_c.arch=="x86_64" ||
        config.ansi_c.arch=="x32")
     {
-      if(config.ansi_c.mode==configt::ansi_ct::flavourt::APPLE)
+      if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG)
         code+="typedef double __float128;\n"; // clang doesn't do __float128
     }
 
+    if(
+      config.ansi_c.arch == "i386" || config.ansi_c.arch == "x86_64" ||
+      config.ansi_c.arch == "x32" || config.ansi_c.arch == "ia64")
+    {
+      // clang doesn't do __float80
+      // Note that __float80 is a typedef, and not a keyword.
+      if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG)
+        code += "typedef __CPROVER_Float64x __float80;\n";
+    }
+
     // On 64-bit systems, gcc has typedefs
     // __int128_t und __uint128_t -- but not on 32 bit!
     if(config.ansi_c.long_int_width>=64)
diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l
index 031d64365ab..af464a7bdb6 100644
--- a/src/ansi-c/scanner.l
+++ b/src/ansi-c/scanner.l
@@ -489,11 +489,8 @@ void ansi_c_scanner_init()
                     return make_identifier();
                 }
 
-"__float80"     { // clang doesn't have it
-                  if(PARSER.mode==configt::ansi_ct::flavourt::GCC)
-                  { loc(); return TOK_GCC_FLOAT80; }
-                  else
-                    return make_identifier();
+"__CPROVER__Float64x" {
+                  loc(); return TOK_GCC_FLOAT64X;
                 }
 
 "__float128"    { // clang doesn't have it
diff --git a/src/cpp/cpp_internal_additions.cpp b/src/cpp/cpp_internal_additions.cpp
index 9f733c6abab..a27927291df 100644
--- a/src/cpp/cpp_internal_additions.cpp
+++ b/src/cpp/cpp_internal_additions.cpp
@@ -126,10 +126,20 @@ void cpp_internal_additions(std::ostream &out)
       config.ansi_c.arch == "x32")
     {
       // clang doesn't do __float128
-      if(config.ansi_c.mode == configt::ansi_ct::flavourt::APPLE)
+      if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG)
         out << "typedef double __float128;" << '\n';
     }
 
+    if(
+      config.ansi_c.arch == "i386" || config.ansi_c.arch == "x86_64" ||
+      config.ansi_c.arch == "x32" || config.ansi_c.arch == "ia64")
+    {
+      // clang doesn't do __float80
+      // Note that __float80 is a typedef, and not a keyword.
+      if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG)
+        out << "typedef __CPROVER_Float64x __float80;" << '\n';
+    }
+
     // On 64-bit systems, gcc has typedefs
     // __int128_t und __uint128_t -- but not on 32 bit!
     if(config.ansi_c.long_int_width >= 64)