diff --git a/regression/cbmc/printf3/main.c b/regression/cbmc/printf3/main.c
new file mode 100644
index 000000000000..3afda07eca80
--- /dev/null
+++ b/regression/cbmc/printf3/main.c
@@ -0,0 +1,12 @@
+#include <assert.h>
+#include <stdio.h>
+
+int main()
+{
+  printf("%ld", 10);
+  printf("%llu", 11);
+  printf("%hhd", 12);
+  printf("%lf", 10.0);
+  printf("%Lf", 11.0);
+  assert(0);
+}
diff --git a/regression/cbmc/printf3/test.desc b/regression/cbmc/printf3/test.desc
new file mode 100644
index 000000000000..4ed8f11c7ad4
--- /dev/null
+++ b/regression/cbmc/printf3/test.desc
@@ -0,0 +1,12 @@
+CORE no-new-smt
+main.c
+--trace
+^10$
+^11$
+^12$
+^10.0+$
+^11.0+$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/src/goto-programs/printf_formatter.cpp b/src/goto-programs/printf_formatter.cpp
index e1207fdac589..afc598fbfa68 100644
--- a/src/goto-programs/printf_formatter.cpp
+++ b/src/goto-programs/printf_formatter.cpp
@@ -11,14 +11,15 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "printf_formatter.h"
 
-#include <sstream>
-
 #include <util/c_types.h>
+#include <util/expr_util.h>
 #include <util/format_constant.h>
 #include <util/pointer_expr.h>
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
 
+#include <sstream>
+
 const exprt printf_formattert::make_type(
   const exprt &src, const typet &dest)
 {
@@ -66,6 +67,8 @@ void printf_formattert::process_format(std::ostream &out)
   format_constant.min_width=0;
   format_constant.zero_padding=false;
 
+  std::string length_modifier;
+
   char ch=next();
 
   if(ch=='0') // leading zeros
@@ -94,6 +97,56 @@ void printf_formattert::process_format(std::ostream &out)
     }
   }
 
+  switch(ch)
+  {
+  case 'h':
+    ch = next();
+    if(ch == 'h')
+    {
+      length_modifier = "hh";
+      ch = next();
+    }
+    else
+    {
+      length_modifier = "h";
+    }
+    break;
+
+  case 'l':
+    ch = next();
+    if(ch == 'l')
+    {
+      length_modifier = "ll";
+      ch = next();
+    }
+    else
+    {
+      length_modifier = "l";
+    }
+    break;
+
+  case 'q':
+    ch = next();
+    length_modifier = "ll";
+    break;
+
+  case 'L':
+  case 'j':
+  case 'z':
+  case 't':
+    length_modifier = ch;
+    ch = next();
+    break;
+
+  case 'Z':
+    ch = next();
+    length_modifier = "z";
+    break;
+
+  default:
+    break;
+  }
+
   switch(ch)
   {
   case '%':
@@ -105,17 +158,23 @@ void printf_formattert::process_format(std::ostream &out)
     format_constant.style=format_spect::stylet::SCIENTIFIC;
     if(next_operand==operands.end())
       break;
-    out << format_constant(
-      make_type(*(next_operand++), double_type()));
+    if(length_modifier == "L")
+      out << format_constant(make_type(*(next_operand++), long_double_type()));
+    else
+      out << format_constant(make_type(*(next_operand++), double_type()));
     break;
 
+  case 'a': // TODO: hexadecimal output
+  case 'A': // TODO: hexadecimal output
   case 'f':
   case 'F':
     format_constant.style=format_spect::stylet::DECIMAL;
     if(next_operand==operands.end())
       break;
-    out << format_constant(
-      make_type(*(next_operand++), double_type()));
+    if(length_modifier == "L")
+      out << format_constant(make_type(*(next_operand++), long_double_type()));
+    else
+      out << format_constant(make_type(*(next_operand++), double_type()));
     break;
 
   case 'g':
@@ -125,10 +184,14 @@ void printf_formattert::process_format(std::ostream &out)
       format_constant.precision=1;
     if(next_operand==operands.end())
       break;
-    out << format_constant(
-      make_type(*(next_operand++), double_type()));
+    if(length_modifier == "L")
+      out << format_constant(make_type(*(next_operand++), long_double_type()));
+    else
+      out << format_constant(make_type(*(next_operand++), double_type()));
     break;
 
+  case 'S':
+    length_modifier = 'l';
   case 's':
     {
       if(next_operand==operands.end())
@@ -164,35 +227,87 @@ void printf_formattert::process_format(std::ostream &out)
     break;
 
   case 'd':
+  case 'i':
+  {
     if(next_operand==operands.end())
       break;
-    out << format_constant(
-      make_type(*(next_operand++), signed_int_type()));
+    typet conversion_type;
+    if(length_modifier == "hh")
+      conversion_type = signed_char_type();
+    else if(length_modifier == "h")
+      conversion_type = signed_short_int_type();
+    else if(length_modifier == "l")
+      conversion_type = signed_long_int_type();
+    else if(length_modifier == "ll")
+      conversion_type = signed_long_long_int_type();
+    else if(length_modifier == "j") // intmax_t
+      conversion_type = signed_long_long_int_type();
+    else if(length_modifier == "z")
+      conversion_type = signed_size_type();
+    else if(length_modifier == "t")
+      conversion_type = pointer_diff_type();
+    else
+      conversion_type = signed_int_type();
+    out << format_constant(make_type(*(next_operand++), conversion_type));
+  }
     break;
 
-  case 'D':
-    if(next_operand==operands.end())
-      break;
-    out << format_constant(
-      make_type(*(next_operand++), signed_long_int_type()));
+    case 'o': // TODO: octal output
+    case 'x': // TODO: hexadecimal output
+    case 'X': // TODO: hexadecimal output
+    case 'u':
+    {
+      if(next_operand == operands.end())
+        break;
+      typet conversion_type;
+      if(length_modifier == "hh")
+        conversion_type = unsigned_char_type();
+      else if(length_modifier == "h")
+        conversion_type = unsigned_short_int_type();
+      else if(length_modifier == "l")
+        conversion_type = unsigned_long_int_type();
+      else if(length_modifier == "ll")
+        conversion_type = unsigned_long_long_int_type();
+      else if(length_modifier == "j") // intmax_t
+        conversion_type = unsigned_long_long_int_type();
+      else if(length_modifier == "z")
+        conversion_type = size_type();
+      else if(length_modifier == "t")
+        conversion_type = pointer_diff_type();
+      else
+        conversion_type = unsigned_int_type();
+      out << format_constant(make_type(*(next_operand++), conversion_type));
+    }
     break;
 
-  case 'u':
-    if(next_operand==operands.end())
+    case 'C':
+      length_modifier = 'l';
+    case 'c':
+      if(next_operand == operands.end())
+        break;
+      if(length_modifier == "l")
+        out << format_constant(make_type(*(next_operand++), wchar_t_type()));
+      else
+        out << format_constant(
+          make_type(*(next_operand++), unsigned_char_type()));
       break;
-    out << format_constant(
-      make_type(*(next_operand++), unsigned_int_type()));
-    break;
 
-  case 'U':
-    if(next_operand==operands.end())
+    case 'p':
+      // TODO: hexadecimal output
+      out << format_constant(make_type(*(next_operand++), size_type()));
       break;
-    out << format_constant(
-      make_type(*(next_operand++), unsigned_long_int_type()));
-    break;
 
-  default:
-    out << '%' << ch;
+    case 'n':
+      if(next_operand == operands.end())
+        break;
+      // printf would store the number of characters written so far in the
+      // object pointed to by this operand. We do not implement this side-effect
+      // here, and just skip one operand.
+      ++next_operand;
+      break;
+
+    default:
+      out << '%' << ch;
   }
 }