diff --git a/CHANGELOG b/CHANGELOG
index 9a884ca05e7..2022bb01308 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -4,6 +4,9 @@
   generate bodies for functions that don't have a body
   in the goto code. This supercedes the functionality
   of --undefined-function-is-assume-false
+* The --fixedbv command-line option has been removed
+  (it was marked deprecated in January 2017)
+
 
 5.8
 ===
diff --git a/regression/cbmc/Fixedbv4/main.c b/regression/cbmc/Fixedbv4/main.c
index c04fa2bfc21..d8079138627 100644
--- a/regression/cbmc/Fixedbv4/main.c
+++ b/regression/cbmc/Fixedbv4/main.c
@@ -1,61 +1,65 @@
+#include <assert.h>
+
+typedef __CPROVER_fixedbv[32][16] fbvt;
+
 int main()
 {
-  double f;
+  fbvt f;
 
   // addition
   assert(100.0+10==110);
   assert(0+f==f);
   assert(f+0==f);
   assert(100+0.5==100.5);
-  assert(0.0+0.0+f==f);
+  assert((fbvt)0.0+(fbvt)0.0+f==f);
 
   // subtraction
-  assert(100.0-10==90);
+  assert((fbvt)100.0-10==90);
   assert(0-f==-f);
   assert(f-0==f);
-  assert(100-0.5==99.5);
-  assert(0.0-0.0-f==-f);
+  assert((fbvt)100-(fbvt)0.5==(fbvt)99.5);
+  assert((fbvt)0.0-(fbvt)0.0-f==-f);
 
   // unary minus
-  assert(-(-100.0)==100);
-  assert(-(1-2.0)==1);
+  assert(-(fbvt)(-100.0)==100);
+  assert(-(1-(fbvt)2.0)==1);
   assert(-(-f)==f);
 
   // multiplication
-  assert(100.0*10==1000);
+  assert((fbvt)100.0*10==1000);
   assert(0*f==0);
   assert(f*0==0);
-  assert(100*0.5==50);
+  assert((fbvt)100*(fbvt)0.5==50);
   assert(f*1==f);
   assert(1*f==f);
-  assert(1.0*1.0*f==f);
+  assert((fbvt)1.0*(fbvt)1.0*f==f);
 
   // division
-  assert(100.0/1.0==100);
-  assert(100.1/1.0==100.1);
-  assert(100.0/2.0==50);
-  assert(100.0/0.5==200);
-  assert(0/1.0==0);
-  assert(f/1.0==f);
+  assert((fbvt)100.0/(fbvt)1.0==100);
+  assert((fbvt)100.1/(fbvt)1.0==(fbvt)100.1);
+  assert((fbvt)100.0/(fbvt)2.0==50);
+  assert((fbvt)100.0/(fbvt)0.5==200);
+  assert(0/(fbvt)1.0==0);
+  assert(f/(fbvt)1.0==f);
 
   // conversion
   assert(((double)(float)100)==100.0);
   assert(((unsigned int)100.0)==100.0);
   assert(100.0);
   assert(!0.0);
-  assert((int)0.5==0);
-  assert((int)0.49==0);
-  assert((int)-1.5==-1);
-  assert((int)-10.49==-10);
+  assert((int)(fbvt)0.5==0);
+  assert((int)(fbvt)0.49==0);
+  assert((int)(fbvt)-1.5==-1);
+  assert((int)(fbvt)-10.49==-10);
 
   // relations
-  assert(1.0<2.5);
-  assert(1.0<=2.5);
-  assert(1.01<=1.01);
-  assert(2.5>1.0);
-  assert(2.5>=1.0);
-  assert(1.01>=1.01);
-  assert(!(1.0>=2.5));
-  assert(!(1.0>2.5));
-  assert(1.0!=2.5);
+  assert((fbvt)1.0<(fbvt)2.5);
+  assert((fbvt)1.0<=(fbvt)2.5);
+  assert((fbvt)1.01<=(fbvt)1.01);
+  assert((fbvt)2.5>(fbvt)1.0);
+  assert((fbvt)2.5>=(fbvt)1.0);
+  assert((fbvt)1.01>=(fbvt)1.01);
+  assert(!((fbvt)1.0>=(fbvt)2.5));
+  assert(!((fbvt)1.0>(fbvt)2.5));
+  assert((fbvt)1.0!=(fbvt)2.5);
 }
diff --git a/regression/cbmc/Fixedbv4/test.desc b/regression/cbmc/Fixedbv4/test.desc
index a43bbd7df65..65535fe6331 100644
--- a/regression/cbmc/Fixedbv4/test.desc
+++ b/regression/cbmc/Fixedbv4/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---fixedbv
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc/Fixedbv6/main.c b/regression/cbmc/Fixedbv6/main.c
index f72d72c6975..ebbad13d9c5 100644
--- a/regression/cbmc/Fixedbv6/main.c
+++ b/regression/cbmc/Fixedbv6/main.c
@@ -1,27 +1,29 @@
+typedef __CPROVER_fixedbv[32][16] fbvt;
+
 int main()
 {
   // constants
-  assert(1.0!=2.0);
-  assert(1.0==1.0);
-  assert(1.0<2.0);
-  assert(!(-1.0<-2.0));
-  assert(2.0>1.0);
-  assert(!(-2.0>-1.0));
-  assert(!(2.0<2.0));
-  assert(!(-2.0<-2.0));
-  assert(!(2.0>2.0));
-  assert(!(-2.0>-2.0));
-  assert(2.0<=2.0);
-  assert(-2.0<=-2.0);
-  assert(2.0>=2.0);
-  assert(-2.0>=-2.0);
-  assert(1.0<=2.0);
-  assert(!(-1.0<=-2.0));
-  assert(2.0>=1.0);
-  assert(!(-2.0>=-1.0));
+  assert((fbvt)1.0!=(fbvt)2.0);
+  assert((fbvt)1.0==(fbvt)1.0);
+  assert((fbvt)1.0<(fbvt)2.0);
+  assert(!((fbvt)-1.0<(fbvt)-2.0));
+  assert((fbvt)2.0>(fbvt)1.0);
+  assert(!((fbvt)-2.0>(fbvt)-1.0));
+  assert(!((fbvt)2.0<(fbvt)2.0));
+  assert(!((fbvt)-2.0<(fbvt)-2.0));
+  assert(!((fbvt)2.0>(fbvt)2.0));
+  assert(!((fbvt)-2.0>(fbvt)-2.0));
+  assert((fbvt)2.0<=(fbvt)2.0);
+  assert((fbvt)-2.0<=(fbvt)-2.0);
+  assert((fbvt)2.0>=(fbvt)2.0);
+  assert((fbvt)-2.0>=(fbvt)-2.0);
+  assert((fbvt)1.0<=(fbvt)2.0);
+  assert(!((fbvt)-1.0<=(fbvt)-2.0));
+  assert((fbvt)2.0>=(fbvt)1.0);
+  assert(!((fbvt)-2.0>=(fbvt)-1.0));
 
   // variables
-  float a, b, _a=a, _b=b;
+  fbvt a, b, _a=a, _b=b;
   __CPROVER_assume(a==1 && b==2);
 
   assert(a!=b);
diff --git a/regression/cbmc/Fixedbv6/test.desc b/regression/cbmc/Fixedbv6/test.desc
index 991a8916c67..9efefbc7362 100644
--- a/regression/cbmc/Fixedbv6/test.desc
+++ b/regression/cbmc/Fixedbv6/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---fixedbv
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc/Fixedbv7/main.c b/regression/cbmc/Fixedbv7/main.c
index c04fa2bfc21..dde9a4c858d 100644
--- a/regression/cbmc/Fixedbv7/main.c
+++ b/regression/cbmc/Fixedbv7/main.c
@@ -1,61 +1,65 @@
+#include <assert.h>
+
+typedef __CPROVER_fixedbv[32][16] fbvt;
+
 int main()
 {
-  double f;
+  fbvt f;
 
   // addition
-  assert(100.0+10==110);
+  assert((fbvt)100.0+10==110);
   assert(0+f==f);
   assert(f+0==f);
-  assert(100+0.5==100.5);
-  assert(0.0+0.0+f==f);
+  assert(100+(fbvt)0.5==(fbvt)100.5);
+  assert((fbvt)0.0+(fbvt)0.0+f==f);
 
   // subtraction
-  assert(100.0-10==90);
+  assert((fbvt)100.0-10==90);
   assert(0-f==-f);
   assert(f-0==f);
-  assert(100-0.5==99.5);
-  assert(0.0-0.0-f==-f);
+  assert(100-(fbvt)0.5==(fbvt)99.5);
+  assert((fbvt)0.0-(fbvt)0.0-f==-f);
 
   // unary minus
-  assert(-(-100.0)==100);
-  assert(-(1-2.0)==1);
+  assert(-(fbvt)(-100.0)==100);
+  assert(-(1-(fbvt)2.0)==1);
   assert(-(-f)==f);
 
   // multiplication
-  assert(100.0*10==1000);
+  assert((fbvt)100.0*10==1000);
   assert(0*f==0);
   assert(f*0==0);
-  assert(100*0.5==50);
+  assert(100*(fbvt)0.5==50);
   assert(f*1==f);
   assert(1*f==f);
-  assert(1.0*1.0*f==f);
+  assert((fbvt)1.0*(fbvt)1.0*f==f);
 
   // division
-  assert(100.0/1.0==100);
-  assert(100.1/1.0==100.1);
-  assert(100.0/2.0==50);
-  assert(100.0/0.5==200);
-  assert(0/1.0==0);
-  assert(f/1.0==f);
+  assert((fbvt)100.0/(fbvt)1.0==100);
+  assert((fbvt)100.1/(fbvt)1.0==(fbvt)100.1);
+  assert((fbvt)100.0/(fbvt)2.0==50);
+  assert((fbvt)100.0/(fbvt)0.5==200);
+  assert(0/(fbvt)1.0==0);
+  assert(f/(fbvt)1.0==f);
 
   // conversion
-  assert(((double)(float)100)==100.0);
-  assert(((unsigned int)100.0)==100.0);
+  assert(((__CPROVER_fixedbv[40][16])(fbvt)100)==(__CPROVER_fixedbv[40][16])100.0);
+  assert(((unsigned int)(fbvt)100.0)==100.0);
   assert(100.0);
   assert(!0.0);
-  assert((int)0.5==0);
-  assert((int)0.49==0);
-  assert((int)-1.5==-1);
-  assert((int)-10.49==-10);
+  assert((int)(fbvt)0.5==0);
+  assert((int)(fbvt)0.49==0);
+  assert((int)(fbvt)-1.5==-1);
+  assert((int)(fbvt)-10.49==-10);
 
   // relations
-  assert(1.0<2.5);
-  assert(1.0<=2.5);
-  assert(1.01<=1.01);
-  assert(2.5>1.0);
-  assert(2.5>=1.0);
-  assert(1.01>=1.01);
-  assert(!(1.0>=2.5));
-  assert(!(1.0>2.5));
-  assert(1.0!=2.5);
+  assert((fbvt)1.0<(fbvt)2.5);
+  assert((fbvt)1.0<=(fbvt)2.5);
+  assert((fbvt)1.01<=(fbvt)1.01);
+  assert((fbvt)2.5>(fbvt)1.0);
+  assert((fbvt)2.5>=(fbvt)1.0);
+  assert((fbvt)1.01>=(fbvt)1.01);
+  assert(!((fbvt)1.0>=(fbvt)2.5));
+  assert(!((fbvt)1.0>(fbvt)2.5));
+  assert((fbvt)1.0!=(fbvt)2.5);
 }
diff --git a/regression/cbmc/Fixedbv7/test.desc b/regression/cbmc/Fixedbv7/test.desc
index 5b018497756..b95c9e3cc2a 100644
--- a/regression/cbmc/Fixedbv7/test.desc
+++ b/regression/cbmc/Fixedbv7/test.desc
@@ -1,8 +1,11 @@
-CORE
+KNOWNBUG
 main.c
---fixedbv --no-simplify
+--no-simplify
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+--
+To make this work, conversion from floating-point numbers to fixed-point
+numbers is required in solvers/flattening/boolbv_typecast.cpp. Issue #2158.
\ No newline at end of file
diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp
index 47ef1c503f5..d488b31f14f 100644
--- a/src/ansi-c/ansi_c_internal_additions.cpp
+++ b/src/ansi-c/ansi_c_internal_additions.cpp
@@ -243,7 +243,6 @@ void ansi_c_architecture_strings(std::string &code)
   code+=architecture_string(config.ansi_c.wchar_t_width, "wchar_t_width");
   code+=architecture_string(config.ansi_c.char_is_unsigned, "char_is_unsigned");
   code+=architecture_string(config.ansi_c.wchar_t_is_unsigned, "wchar_t_is_unsigned"); // NOLINT(whitespace/line_length)
-  code+=architecture_string(config.ansi_c.use_fixed_for_float, "fixed_for_float"); // NOLINT(whitespace/line_length)
   code+=architecture_string(config.ansi_c.alignment, "alignment");
   code+=architecture_string(config.ansi_c.memory_operand_size, "memory_operand_size"); // NOLINT(whitespace/line_length)
   code+=architecture_string(static_cast<int>(config.ansi_c.endianness), "endianness"); // NOLINT(whitespace/line_length)
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index 305a38e008f..215f05d39bd 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -219,15 +219,6 @@ std::string expr2ct::convert_rec(
   {
     const std::size_t width=to_fixedbv_type(src).get_width();
 
-    if(config.ansi_c.use_fixed_for_float)
-    {
-      if(width==config.ansi_c.single_width)
-        return q+"float"+d;
-      if(width==config.ansi_c.double_width)
-        return q+"double"+d;
-      if(width==config.ansi_c.long_double_width)
-        return q+"long double"+d;
-    }
     const std::size_t fraction_bits=to_fixedbv_type(src).get_fraction_bits();
     return
       q+"__CPROVER_fixedbv["+std::to_string(width)+"]["+
diff --git a/src/ansi-c/gcc_types.cpp b/src/ansi-c/gcc_types.cpp
index 5ac8a9b4220..cebc072e5fc 100644
--- a/src/ansi-c/gcc_types.cpp
+++ b/src/ansi-c/gcc_types.cpp
@@ -13,145 +13,64 @@ Author: Daniel Kroening, kroening@kroening.com
 
 bitvector_typet gcc_float16_type()
 {
-  if(config.ansi_c.use_fixed_for_float)
-  {
-    fixedbv_typet result;
-    result.set_width(16);
-    result.set_integer_bits(16/2);
-    result.set(ID_C_c_type, ID_gcc_float16);
-    return result;
-  }
-  else
-  {
-    floatbv_typet result=
-      ieee_float_spect::half_precision().to_type();
-    result.set(ID_C_c_type, ID_gcc_float16);
-    return result;
-  }
+  floatbv_typet result=
+    ieee_float_spect::half_precision().to_type();
+  result.set(ID_C_c_type, ID_gcc_float16);
+  return result;
 }
 
 bitvector_typet gcc_float32_type()
 {
   // not same as float!
-
-  if(config.ansi_c.use_fixed_for_float)
-  {
-    fixedbv_typet result;
-    result.set_width(config.ansi_c.single_width);
-    result.set_integer_bits(config.ansi_c.single_width/2);
-    result.set(ID_C_c_type, ID_gcc_float32);
-    return result;
-  }
-  else
-  {
-    floatbv_typet result=
-      ieee_float_spect::single_precision().to_type();
-    result.set(ID_C_c_type, ID_gcc_float32);
-    return result;
-  }
+  floatbv_typet result=
+    ieee_float_spect::single_precision().to_type();
+  result.set(ID_C_c_type, ID_gcc_float32);
+  return result;
 }
 
 bitvector_typet gcc_float32x_type()
 {
   // not same as float!
-
-  if(config.ansi_c.use_fixed_for_float)
-  {
-    fixedbv_typet result;
-    result.set_width(config.ansi_c.single_width);
-    result.set_integer_bits(config.ansi_c.single_width/2);
-    result.set(ID_C_c_type, ID_gcc_float32x);
-    return result;
-  }
-  else
-  {
-    floatbv_typet result=
-      ieee_float_spect::single_precision().to_type();
-    result.set(ID_C_c_type, ID_gcc_float32x);
-    return result;
-  }
+  floatbv_typet result=
+    ieee_float_spect::single_precision().to_type();
+  result.set(ID_C_c_type, ID_gcc_float32x);
+  return result;
 }
 
 bitvector_typet gcc_float64_type()
 {
   // not same as double!
-  if(config.ansi_c.use_fixed_for_float)
-  {
-    fixedbv_typet result;
-    result.set_width(config.ansi_c.double_width);
-    result.set_integer_bits(config.ansi_c.double_width/2);
-    result.set(ID_C_c_type, ID_gcc_float64);
-    return result;
-  }
-  else
-  {
-    floatbv_typet result=
-      ieee_float_spect::double_precision().to_type();
-    result.set(ID_C_c_type, ID_gcc_float64);
-    return result;
-  }
+  floatbv_typet result=
+    ieee_float_spect::double_precision().to_type();
+  result.set(ID_C_c_type, ID_gcc_float64);
+  return result;
 }
 
 bitvector_typet gcc_float64x_type()
 {
   // not same as double!
-  if(config.ansi_c.use_fixed_for_float)
-  {
-    fixedbv_typet result;
-    result.set_width(config.ansi_c.double_width);
-    result.set_integer_bits(config.ansi_c.double_width/2);
-    result.set(ID_C_c_type, ID_gcc_float64x);
-    return result;
-  }
-  else
-  {
-    floatbv_typet result=
-      ieee_float_spect::double_precision().to_type();
-    result.set(ID_C_c_type, ID_gcc_float64x);
-    return result;
-  }
+  floatbv_typet result=
+    ieee_float_spect::double_precision().to_type();
+  result.set(ID_C_c_type, ID_gcc_float64x);
+  return result;
 }
 
 bitvector_typet gcc_float128_type()
 {
   // not same as long double!
-
-  if(config.ansi_c.use_fixed_for_float)
-  {
-    fixedbv_typet result;
-    result.set_width(128);
-    result.set_integer_bits(128/2);
-    result.set(ID_C_c_type, ID_gcc_float128);
-    return result;
-  }
-  else
-  {
-    floatbv_typet result=
-      ieee_float_spect::quadruple_precision().to_type();
-    result.set(ID_C_c_type, ID_gcc_float128);
-    return result;
-  }
+  floatbv_typet result=
+    ieee_float_spect::quadruple_precision().to_type();
+  result.set(ID_C_c_type, ID_gcc_float128);
+  return result;
 }
 
 bitvector_typet gcc_float128x_type()
 {
   // not same as long double!
-
-  if(config.ansi_c.use_fixed_for_float)
-  {
-    fixedbv_typet result;
-    result.set_width(128);
-    result.set_integer_bits(128/2);
-    result.set(ID_C_c_type, ID_gcc_float128x);
-    return result;
-  }
-  else
-  {
-    floatbv_typet result=
-      ieee_float_spect::quadruple_precision().to_type();
-    result.set(ID_C_c_type, ID_gcc_float128x);
-    return result;
-  }
+  floatbv_typet result=
+    ieee_float_spect::quadruple_precision().to_type();
+  result.set(ID_C_c_type, ID_gcc_float128x);
+  return result;
 }
 
 unsignedbv_typet gcc_unsigned_int128_type()
diff --git a/src/ansi-c/literals/convert_float_literal.cpp b/src/ansi-c/literals/convert_float_literal.cpp
index 19a9467b3cc..a7e817c82f5 100644
--- a/src/ansi-c/literals/convert_float_literal.cpp
+++ b/src/ansi-c/literals/convert_float_literal.cpp
@@ -74,60 +74,18 @@ exprt convert_float_literal(const std::string &src)
     // but these aren't handled anywhere
   }
 
-  if(config.ansi_c.use_fixed_for_float)
-  {
-    unsigned width=result.type().get_int(ID_width);
-    unsigned fraction_bits;
-    const irep_idt integer_bits=result.type().get(ID_integer_bits);
-
-    assert(width!=0);
+  ieee_floatt a(to_floatbv_type(result.type()));
 
-    if(integer_bits==irep_idt())
-      fraction_bits=width/2; // default
-    else
-      fraction_bits=width-std::stoi(id2string(integer_bits));
-
-    mp_integer factor=mp_integer(1)<<fraction_bits;
-    mp_integer value=parsed_float.significand*factor;
-
-    if(value!=0)
-    {
-      if(parsed_float.exponent<0)
-        value/=power(parsed_float.exponent_base, -parsed_float.exponent);
-      else
-      {
-        value*=power(parsed_float.exponent_base, parsed_float.exponent);
-
-        if(value>=power(2, width-1))
-        {
-          // saturate: use "biggest value"
-          value=power(2, width-1)-1;
-        }
-        else if(value<=-power(2, width-1)-1)
-        {
-          // saturate: use "smallest value"
-          value=-power(2, width-1);
-        }
-      }
-    }
-
-    result.set(ID_value, integer2binary(value, width));
-  }
+  if(parsed_float.exponent_base==10)
+    a.from_base10(parsed_float.significand, parsed_float.exponent);
+  else if(parsed_float.exponent_base==2) // hex
+    a.build(parsed_float.significand, parsed_float.exponent);
   else
-  {
-    ieee_floatt a(to_floatbv_type(result.type()));
-
-    if(parsed_float.exponent_base==10)
-      a.from_base10(parsed_float.significand, parsed_float.exponent);
-    else if(parsed_float.exponent_base==2) // hex
-      a.build(parsed_float.significand, parsed_float.exponent);
-    else
-      assert(false);
+    UNREACHABLE;
 
-    result.set(
-      ID_value,
-      integer2binary(a.pack(), a.spec.width()));
-  }
+  result.set(
+    ID_value,
+    integer2binary(a.pack(), a.spec.width()));
 
   if(parsed_float.is_imaginary)
   {
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
index b50c5160ba3..f2efce4557d 100644
--- a/src/cbmc/cbmc_parse_options.h
+++ b/src/cbmc/cbmc_parse_options.h
@@ -74,7 +74,7 @@ class optionst;
   OPT_FLUSH \
   "(localize-faults)(localize-faults-method):" \
   OPT_GOTO_TRACE \
-  "(claim):(show-claims)(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
+  "(claim):(show-claims)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
 // clang-format on
 
 class cbmc_parse_optionst:
diff --git a/src/util/c_types.cpp b/src/util/c_types.cpp
index 78d0ad08238..c0cd6cc37a8 100644
--- a/src/util/c_types.cpp
+++ b/src/util/c_types.cpp
@@ -184,78 +184,45 @@ unsignedbv_typet char32_t_type()
 
 bitvector_typet float_type()
 {
-  if(config.ansi_c.use_fixed_for_float)
-  {
-    fixedbv_typet result;
-    result.set_width(config.ansi_c.single_width);
-    result.set_integer_bits(config.ansi_c.single_width/2);
-    result.set(ID_C_c_type, ID_float);
-    return result;
-  }
-  else
-  {
-    floatbv_typet result=
-      ieee_float_spect::single_precision().to_type();
-    result.set(ID_C_c_type, ID_float);
-    return result;
-  }
+  floatbv_typet result=
+    ieee_float_spect::single_precision().to_type();
+  result.set(ID_C_c_type, ID_float);
+  return result;
 }
 
 bitvector_typet double_type()
 {
-  if(config.ansi_c.use_fixed_for_float)
-  {
-    fixedbv_typet result;
-    result.set_width(config.ansi_c.double_width);
-    result.set_integer_bits(config.ansi_c.double_width/2);
-    result.set(ID_C_c_type, ID_double);
-    return result;
-  }
-  else
-  {
-    floatbv_typet result=
-      ieee_float_spect::double_precision().to_type();
-    result.set(ID_C_c_type, ID_double);
-    return result;
-  }
+  floatbv_typet result=
+    ieee_float_spect::double_precision().to_type();
+  result.set(ID_C_c_type, ID_double);
+  return result;
 }
 
 bitvector_typet long_double_type()
 {
-  if(config.ansi_c.use_fixed_for_float)
+  floatbv_typet result;
+  if(config.ansi_c.long_double_width==128)
+    result=ieee_float_spect::quadruple_precision().to_type();
+  else if(config.ansi_c.long_double_width==64)
+    result=ieee_float_spect::double_precision().to_type();
+  else if(config.ansi_c.long_double_width==80)
   {
-    fixedbv_typet result;
-    result.set_width(config.ansi_c.long_double_width);
-    result.set_integer_bits(config.ansi_c.long_double_width/2);
-    result.set(ID_C_c_type, ID_long_double);
-    return result;
+    // x86 extended precision has 80 bits in total, and
+    // deviating from IEEE, does not use a hidden bit.
+    // We use the closest we have got, but the below isn't accurate.
+    result=ieee_float_spect(63, 15).to_type();
   }
-  else
+  else if(config.ansi_c.long_double_width==96)
   {
-    floatbv_typet result;
-    if(config.ansi_c.long_double_width==128)
-      result=ieee_float_spect::quadruple_precision().to_type();
-    else if(config.ansi_c.long_double_width==64)
-      result=ieee_float_spect::double_precision().to_type();
-    else if(config.ansi_c.long_double_width==80)
-    {
-      // x86 extended precision has 80 bits in total, and
-      // deviating from IEEE, does not use a hidden bit.
-      // We use the closest we have got, but the below isn't accurate.
-      result=ieee_float_spect(63, 15).to_type();
-    }
-    else if(config.ansi_c.long_double_width==96)
-    {
-      result=ieee_float_spect(80, 15).to_type();
-      // not quite right. The extra bits beyond 80 are usually padded.
-    }
-    else
-      INVARIANT(false, "width of long double");
-
-    result.set(ID_C_c_type, ID_long_double);
-
-    return result;
+    result=ieee_float_spect(80, 15).to_type();
+    // not quite right. The extra bits beyond 80 are usually padded.
   }
+  else
+    INVARIANT(false, "width of long double");
+
+  result.set(ID_C_c_type, ID_long_double);
+
+  return result;
 }
 
 signedbv_typet pointer_diff_type()
diff --git a/src/util/config.cpp b/src/util/config.cpp
index 15680a6c448..c0d68d9cd05 100644
--- a/src/util/config.cpp
+++ b/src/util/config.cpp
@@ -739,7 +739,6 @@ bool configt::set(const cmdlinet &cmdline)
   ansi_c.single_precision_constant=false;
   ansi_c.for_has_scope=true; // C99 or later
   ansi_c.c_standard=ansi_ct::default_c_standard();
-  ansi_c.use_fixed_for_float=false;
   ansi_c.endianness=ansi_ct::endiannesst::NO_ENDIANNESS;
   ansi_c.os=ansi_ct::ost::NO_OS;
   ansi_c.arch="none";
@@ -791,12 +790,6 @@ bool configt::set(const cmdlinet &cmdline)
   if(cmdline.isset("include"))
     ansi_c.include_files=cmdline.get_values("include");
 
-  if(cmdline.isset("floatbv"))
-    ansi_c.use_fixed_for_float=false;
-
-  if(cmdline.isset("fixedbv"))
-    ansi_c.use_fixed_for_float=true;
-
   // the default architecture is the one we run on
   irep_idt this_arch=this_architecture();
   irep_idt arch=this_arch;
@@ -1142,7 +1135,6 @@ void configt::set_from_symbol_table(
 
   ansi_c.char_is_unsigned=unsigned_from_ns(ns, "char_is_unsigned")!=0;
   ansi_c.wchar_t_is_unsigned=unsigned_from_ns(ns, "wchar_t_is_unsigned")!=0;
-  ansi_c.use_fixed_for_float=unsigned_from_ns(ns, "fixed_for_float")!=0;
   // for_has_scope, single_precision_constant, rounding_mode not
   // stored in namespace
 
diff --git a/src/util/config.h b/src/util/config.h
index 8031b872d3e..57cf613956f 100644
--- a/src/util/config.h
+++ b/src/util/config.h
@@ -41,7 +41,6 @@ class configt
 
     // various language options
     bool char_is_unsigned, wchar_t_is_unsigned;
-    bool use_fixed_for_float;
     bool for_has_scope;
     bool single_precision_constant;
     enum class c_standardt { C89, C99, C11 } c_standard;
diff --git a/src/util/fixedbv.cpp b/src/util/fixedbv.cpp
index 4ea2a166129..0ca5d394212 100644
--- a/src/util/fixedbv.cpp
+++ b/src/util/fixedbv.cpp
@@ -79,6 +79,11 @@ void fixedbvt::round(const fixedbv_spect &dest_spec)
 
     result=div;
   }
+  else // new_faction_bits==old_fraction_vits
+  {
+    // no change!
+    result=v;
+  }
 
   v=result;
   spec=dest_spec;