diff --git a/regression/cbmc/printf1/main.c b/regression/cbmc/printf1/main.c
new file mode 100644
index 00000000000..b488946fd73
--- /dev/null
+++ b/regression/cbmc/printf1/main.c
@@ -0,0 +1,11 @@
+#include <stdio.h>
+#include <assert.h>
+
+int main()
+{
+  printf("PRINT d1 %d, %d\n", 123, -123);
+  printf("PRINT g1 %g, %g, %g, %g\n", 123.0, -123.0, 123.123, 0.123);
+  printf("PRINT e1 %e, %e, %e, %e\n", 123.0, -123.0, 123.123, 0.123);
+  printf("PRINT f1 %f, %f, %f, %f\n", 123.0, -123.0, 123.123, 0.123);
+  assert(0);
+}
diff --git a/regression/cbmc/printf1/test.desc b/regression/cbmc/printf1/test.desc
new file mode 100644
index 00000000000..b5c8583e4ff
--- /dev/null
+++ b/regression/cbmc/printf1/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+--trace
+^EXIT=10$
+^SIGNAL=0$
+^PRINT d1 123, -123$
+^PRINT g1 123, -123, 123\.123, 0\.123$
+^PRINT e1 1\.230000e\+2, -1\.230000e\+2, 1\.231230e\+2, 1\.230000e-1$
+^PRINT f1 123\.000000, -123\.000000, 123\.123000, 0\.123000$
+--
+^warning: ignoring
diff --git a/src/ansi-c/printf_formatter.cpp b/src/ansi-c/printf_formatter.cpp
index 59e3dbcc20f..31ddfa735f2 100644
--- a/src/ansi-c/printf_formatter.cpp
+++ b/src/ansi-c/printf_formatter.cpp
@@ -159,8 +159,18 @@ void printf_formattert::process_format(std::ostream &out)
     out << ch;
     break;
 
+  case 'e':
+  case 'E':
+    format_constant.style=format_spect::stylet::SCIENTIFIC;
+    if(next_operand==operands.end())
+      break;
+    out << format_constant(
+      make_type(*(next_operand++), double_type()));
+    break;
+
   case 'f':
   case 'F':
+    format_constant.style=format_spect::stylet::DECIMAL;
     if(next_operand==operands.end())
       break;
     out << format_constant(
@@ -169,6 +179,7 @@ void printf_formattert::process_format(std::ostream &out)
 
   case 'g':
   case 'G':
+    format_constant.style=format_spect::stylet::AUTOMATIC;
     if(format_constant.precision==0)
       format_constant.precision=1;
     if(next_operand==operands.end())
diff --git a/src/util/ieee_float.cpp b/src/util/ieee_float.cpp
index 52100b59242..73290f70654 100644
--- a/src/util/ieee_float.cpp
+++ b/src/util/ieee_float.cpp
@@ -161,25 +161,39 @@ std::string ieee_floatt::format(const format_spect &format_spec) const
 
   case format_spect::stylet::AUTOMATIC:
     {
+      // On Linux, the man page says:
       // "Style e is used if the exponent from its conversion
       //  is less than -4 or greater than or equal to the precision."
+      //
+      // On BSD, it's
+      // "The argument is printed in style f (F) or in style e (E)
+      // whichever gives full precision in minimum space."
 
       mp_integer _exponent, _fraction;
       extract_base10(_fraction, _exponent);
 
-      if(_exponent>=0)
+      mp_integer adjusted_exponent=base10_digits(_fraction)+_exponent;
+
+      if(adjusted_exponent>=format_spec.precision ||
+         adjusted_exponent<-4)
       {
-        if(base10_digits(_fraction)+_exponent>=format_spec.precision)
-          result+=to_string_scientific(format_spec.precision);
-        else
-          result+=to_string_decimal(format_spec.precision);
+        result+=to_string_scientific(format_spec.precision);
       }
-      else // _exponent<0
+      else
       {
-        if(true) // base10_digits(fraction)+_exponent<-4)
-          result+=to_string_scientific(format_spec.precision);
-        else
-          result+=to_string_decimal(format_spec.precision);
+        result+=to_string_decimal(format_spec.precision);
+
+        // Implementations tested also appear to suppress trailing zeros
+        // and trailing dots.
+
+        {
+          std::size_t trunc_pos=result.find_last_not_of('0');
+          if(trunc_pos!=std::string::npos)
+            result.resize(trunc_pos+1);
+        }
+
+        if(!result.empty() && result.back()=='.')
+          result.resize(result.size()-1);
       }
     }
     break;