diff --git a/regression/cbmc-library/dprintf-01/main.c b/regression/cbmc-library/dprintf-01/main.c
new file mode 100644
index 00000000000..51758663848
--- /dev/null
+++ b/regression/cbmc-library/dprintf-01/main.c
@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <stdio.h>
+
+int main(int argc, char *argv[])
+{
+  dprintf(1, "some string %s: %d\n", argv[0], 42);
+  dprintf(1, "some other string\n");
+  return 0;
+}
diff --git a/regression/cbmc-library/dprintf-01/test.desc b/regression/cbmc-library/dprintf-01/test.desc
new file mode 100644
index 00000000000..96c9b4bcd7b
--- /dev/null
+++ b/regression/cbmc-library/dprintf-01/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --bounds-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-library/vdprintf-01/main.c b/regression/cbmc-library/vdprintf-01/main.c
new file mode 100644
index 00000000000..e64327c1a29
--- /dev/null
+++ b/regression/cbmc-library/vdprintf-01/main.c
@@ -0,0 +1,17 @@
+#include <stdarg.h>
+#include <stdio.h>
+
+int xdprintf(int fd, const char *format, ...)
+{
+  va_list list;
+  va_start(list, format);
+  int result = vdprintf(fd, format, list);
+  va_end(list);
+  return result;
+}
+
+int main()
+{
+  xdprintf(1, "%d\n", 42);
+  return 0;
+}
diff --git a/regression/cbmc-library/vdprintf-01/test.desc b/regression/cbmc-library/vdprintf-01/test.desc
new file mode 100644
index 00000000000..96c9b4bcd7b
--- /dev/null
+++ b/regression/cbmc-library/vdprintf-01/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --bounds-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/ansi-c/library/stdio.c b/src/ansi-c/library/stdio.c
index 483452d27e0..d3c49bce9d1 100644
--- a/src/ansi-c/library/stdio.c
+++ b/src/ansi-c/library/stdio.c
@@ -1560,6 +1560,55 @@ int asprintf(char **ptr, const char *fmt, ...)
   return result;
 }
 
+/* FUNCTION: dprintf */
+
+#ifndef __CPROVER_STDIO_H_INCLUDED
+#  include <stdio.h>
+#  define __CPROVER_STDIO_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_STDARG_H_INCLUDED
+#  include <stdarg.h>
+#  define __CPROVER_STDARG_H_INCLUDED
+#endif
+
+int dprintf(int fd, const char *restrict format, ...)
+{
+__CPROVER_HIDE:;
+  va_list list;
+  va_start(list, format);
+  int result = vdprintf(fd, format, list);
+  va_end(list);
+  return result;
+}
+
+/* FUNCTION: vdprintf */
+
+#ifndef __CPROVER_STDIO_H_INCLUDED
+#  include <stdio.h>
+#  define __CPROVER_STDIO_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_STDARG_H_INCLUDED
+#  include <stdarg.h>
+#  define __CPROVER_STDARG_H_INCLUDED
+#endif
+
+int __VERIFIER_nondet_int(void);
+
+int vdprintf(int fd, const char *restrict format, va_list arg)
+{
+__CPROVER_HIDE:;
+
+  int result = __VERIFIER_nondet_int();
+
+  (void)fd;
+  (void)*format;
+  (void)arg;
+
+  return result;
+}
+
 /* FUNCTION: vasprintf */
 
 #ifndef __CPROVER_STDIO_H_INCLUDED