diff --git a/regression/cbmc-library/fileno-01/main.c b/regression/cbmc-library/fileno-01/main.c
index a4d6d01dc37..c186de1b88d 100644
--- a/regression/cbmc-library/fileno-01/main.c
+++ b/regression/cbmc-library/fileno-01/main.c
@@ -3,7 +3,14 @@
 
 int main()
 {
-  fileno();
-  assert(0);
+  // requires initialization of stdin/stdout/stderr
+  // assert(fileno(stdin) == 0);
+  // assert(fileno(stdout) == 1);
+  // assert(fileno(stderr) == 2);
+
+  int fd;
+  FILE *some_file = fdopen(fd, "");
+  assert(fileno(some_file) >= -1);
+
   return 0;
 }
diff --git a/regression/cbmc-library/fileno-01/test.desc b/regression/cbmc-library/fileno-01/test.desc
index 9542d988e8d..96c9b4bcd7b 100644
--- a/regression/cbmc-library/fileno-01/test.desc
+++ b/regression/cbmc-library/fileno-01/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --pointer-check --bounds-check
 ^EXIT=0$
diff --git a/regression/cbmc-library/fprintf-01/main.c b/regression/cbmc-library/fprintf-01/main.c
index 264c8ae7b19..6eed023d694 100644
--- a/regression/cbmc-library/fprintf-01/main.c
+++ b/regression/cbmc-library/fprintf-01/main.c
@@ -1,9 +1,9 @@
 #include <assert.h>
 #include <stdio.h>
 
-int main()
+int main(int argc, char *argv[])
 {
-  fprintf();
-  assert(0);
+  fprintf(stdout, "some string %s: %d\n", argv[0], 42);
+  fprintf(stderr, "some other string\n");
   return 0;
 }
diff --git a/regression/cbmc-library/fprintf-01/test.desc b/regression/cbmc-library/fprintf-01/test.desc
index 9542d988e8d..96c9b4bcd7b 100644
--- a/regression/cbmc-library/fprintf-01/test.desc
+++ b/regression/cbmc-library/fprintf-01/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --pointer-check --bounds-check
 ^EXIT=0$
diff --git a/src/ansi-c/library/stdio.c b/src/ansi-c/library/stdio.c
index 12a387deb83..8caec8fb5c2 100644
--- a/src/ansi-c/library/stdio.c
+++ b/src/ansi-c/library/stdio.c
@@ -75,27 +75,27 @@ inline FILE *fopen(const char *filename, const char *mode)
   __CPROVER_HIDE:;
   (void)*filename;
   (void)*mode;
-  #ifdef __CPROVER_STRING_ABSTRACTION
+#ifdef __CPROVER_STRING_ABSTRACTION
   __CPROVER_assert(__CPROVER_is_zero_string(filename), "fopen zero-termination of 1st argument");
   __CPROVER_assert(__CPROVER_is_zero_string(mode), "fopen zero-termination of 2nd argument");
-  #endif
+#endif
 
   FILE *fopen_result;
 
   __CPROVER_bool fopen_error=__VERIFIER_nondet___CPROVER_bool();
 
-  #if !defined(__linux__) || defined(__GLIBC__)
+#if !defined(__linux__) || defined(__GLIBC__)
   fopen_result=fopen_error?NULL:malloc(sizeof(FILE));
-  #else
+#else
   // libraries need to expose the definition of FILE; this is the
   // case for musl
   fopen_result=fopen_error?NULL:malloc(sizeof(int));
-  #endif
+#endif
 
-  #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
+#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
   __CPROVER_set_must(fopen_result, "open");
   __CPROVER_cleanup(fopen_result, fclose_cleanup);
-  #endif
+#endif
 
   return fopen_result;
 }
@@ -112,11 +112,11 @@ inline FILE* freopen(const char *filename, const char *mode, FILE *f)
   __CPROVER_HIDE:;
   (void)*filename;
   (void)*mode;
-  #if !defined(__linux__) || defined(__GLIBC__)
+#if !defined(__linux__) || defined(__GLIBC__)
   (void)*f;
-  #else
+#else
   (void)*(char*)f;
-  #endif
+#endif
 
   return f;
 }
@@ -137,13 +137,13 @@ int __VERIFIER_nondet_int();
 
 inline int fclose(FILE *stream)
 {
-  __CPROVER_HIDE:;
-  #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
+__CPROVER_HIDE:;
+#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
   __CPROVER_assert(__CPROVER_get_must(stream, "open"),
                    "fclose file must be open");
   __CPROVER_clear_must(stream, "open");
   __CPROVER_set_must(stream, "closed");
-  #endif
+#endif
   int return_value=__VERIFIER_nondet_int();
   free(stream);
   return return_value;
@@ -166,18 +166,18 @@ inline FILE *fdopen(int handle, const char *mode)
   __CPROVER_HIDE:;
   (void)handle;
   (void)*mode;
-  #ifdef __CPROVER_STRING_ABSTRACTION
+#ifdef __CPROVER_STRING_ABSTRACTION
   __CPROVER_assert(__CPROVER_is_zero_string(mode),
     "fdopen zero-termination of 2nd argument");
-  #endif
+#endif
 
-  #if !defined(__linux__) || defined(__GLIBC__)
+#if !defined(__linux__) || defined(__GLIBC__)
   FILE *f=malloc(sizeof(FILE));
-  #else
+#else
   // libraries need to expose the definition of FILE; this is the
   // case for musl
   FILE *f=malloc(sizeof(int));
-  #endif
+#endif
 
   return f;
 }
@@ -205,10 +205,10 @@ inline FILE *_fdopen(int handle, const char *mode)
   __CPROVER_HIDE:;
   (void)handle;
   (void)*mode;
-  #ifdef __CPROVER_STRING_ABSTRACTION
+#ifdef __CPROVER_STRING_ABSTRACTION
   __CPROVER_assert(__CPROVER_is_zero_string(mode),
     "fdopen zero-termination of 2nd argument");
-  #endif
+#endif
 
   FILE *f=malloc(sizeof(FILE));
 
@@ -232,18 +232,21 @@ char *fgets(char *str, int size, FILE *stream)
   __CPROVER_bool error=__VERIFIER_nondet___CPROVER_bool();
 
   (void)size;
-  #if !defined(__linux__) || defined(__GLIBC__)
-  (void)*stream;
-  #else
-  (void)*(char*)stream;
-  #endif
+  if(stream != stdin)
+  {
+#if !defined(__linux__) || defined(__GLIBC__)
+    (void)*stream;
+#else
+    (void)*(char *)stream;
+#endif
+  }
 
-  #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
+#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
   __CPROVER_assert(__CPROVER_get_must(stream, "open"),
                    "fgets file must be open");
-  #endif
+#endif
 
-  #ifdef __CPROVER_STRING_ABSTRACTION
+#ifdef __CPROVER_STRING_ABSTRACTION
   int resulting_size;
   __CPROVER_assert(__CPROVER_buffer_size(str)>=size, "buffer-overflow in fgets");
   if(size>0)
@@ -252,7 +255,7 @@ char *fgets(char *str, int size, FILE *stream)
     __CPROVER_is_zero_string(str)=!error;
     __CPROVER_zero_string_length(str)=resulting_size;
   }
-  #else
+#else
   if(size>0)
   {
     int str_length=__VERIFIER_nondet_int();
@@ -265,7 +268,7 @@ char *fgets(char *str, int size, FILE *stream)
     if(!error)
       str[str_length]='\0';
   }
-  #endif
+#endif
 
   return error?0:str;
 }
@@ -290,16 +293,19 @@ inline size_t fread(
   size_t bytes=nread*size;
   __CPROVER_assume(nread<=nitems);
 
-  #if !defined(__linux__) || defined(__GLIBC__)
-  (void)*stream;
-  #else
-  (void)*(char*)stream;
-  #endif
+  if(stream != stdin)
+  {
+#if !defined(__linux__) || defined(__GLIBC__)
+    (void)*stream;
+#else
+    (void)*(char *)stream;
+#endif
+  }
 
-  #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
+#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
   __CPROVER_assert(__CPROVER_get_must(stream, "open"),
                    "fread file must be open");
-  #endif
+#endif
 
   for(size_t i=0; i<bytes; i++)
   {
@@ -325,16 +331,19 @@ inline int feof(FILE *stream)
   __CPROVER_HIDE:;
   int return_value=__VERIFIER_nondet_int();
 
-  #if !defined(__linux__) || defined(__GLIBC__)
-  (void)*stream;
-  #else
-  (void)*(char*)stream;
-  #endif
+  if(stream != stdin)
+  {
+#if !defined(__linux__) || defined(__GLIBC__)
+    (void)*stream;
+#else
+    (void)*(char *)stream;
+#endif
+  }
 
-  #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
+#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
   __CPROVER_assert(__CPROVER_get_must(stream, "open"),
                    "feof file must be open");
-  #endif
+#endif
 
   return return_value;
 }
@@ -354,16 +363,19 @@ inline int ferror(FILE *stream)
   __CPROVER_HIDE:;
   int return_value=__VERIFIER_nondet_int();
 
-  #if !defined(__linux__) || defined(__GLIBC__)
-  (void)*stream;
-  #else
-  (void)*(char*)stream;
-  #endif
+  if(stream != stdin)
+  {
+#if !defined(__linux__) || defined(__GLIBC__)
+    (void)*stream;
+#else
+    (void)*(char *)stream;
+#endif
+  }
 
-  #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
+#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
   __CPROVER_assert(__CPROVER_get_must(stream, "open"),
                    "feof file must be open");
-  #endif
+#endif
 
   return return_value;
 }
@@ -379,20 +391,27 @@ int __VERIFIER_nondet_int();
 
 inline int fileno(FILE *stream)
 {
-  // just return nondet
-  __CPROVER_HIDE:;
+__CPROVER_HIDE:;
+  if(stream == stdin)
+    return 0;
+  else if(stream == stdout)
+    return 1;
+  else if(stream == stderr)
+    return 2;
+
   int return_value=__VERIFIER_nondet_int();
+  __CPROVER_assume(return_value >= -1);
 
-  #if !defined(__linux__) || defined(__GLIBC__)
+#if !defined(__linux__) || defined(__GLIBC__)
   (void)*stream;
-  #else
+#else
   (void)*(char*)stream;
-  #endif
+#endif
 
-  #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
+#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
   __CPROVER_assert(__CPROVER_get_must(stream, "open"),
                    "fileno file must be open");
-  #endif
+#endif
 
   return return_value;
 }
@@ -411,21 +430,24 @@ inline int fputs(const char *s, FILE *stream)
   // just return nondet
   __CPROVER_HIDE:;
   int return_value=__VERIFIER_nondet_int();
-  #ifdef __CPROVER_STRING_ABSTRACTION
+#ifdef __CPROVER_STRING_ABSTRACTION
   __CPROVER_assert(__CPROVER_is_zero_string(s), "fputs zero-termination of 1st argument");
-  #endif
+#endif
   (void)*s;
 
-  #if !defined(__linux__) || defined(__GLIBC__)
-  (void)*stream;
-  #else
-  (void)*(char*)stream;
-  #endif
+  if(stream != stdout && stream != stderr)
+  {
+#if !defined(__linux__) || defined(__GLIBC__)
+    (void)*stream;
+#else
+    (void)*(char *)stream;
+#endif
+  }
 
-  #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
+#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
   __CPROVER_assert(__CPROVER_get_must(stream, "open"),
                    "fputs file must be open");
-  #endif
+#endif
 
   return return_value;
 }
@@ -446,11 +468,11 @@ inline int fflush(FILE *stream)
   int return_value=__VERIFIER_nondet_int();
   (void)stream;
 
-  #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
+#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
   if(stream)
     __CPROVER_assert(__CPROVER_get_must(stream, "open"),
                      "fflush file must be open");
-  #endif
+#endif
 
   return return_value;
 }
@@ -470,16 +492,19 @@ inline int fpurge(FILE *stream)
   __CPROVER_HIDE:;
   int return_value=__VERIFIER_nondet_int();
 
-  #if !defined(__linux__) || defined(__GLIBC__)
-  (void)*stream;
-  #else
-  (void)*(char*)stream;
-  #endif
+  if(stream != stdin && stream != stdout && stream != stderr)
+  {
+#if !defined(__linux__) || defined(__GLIBC__)
+    (void)*stream;
+#else
+    (void)*(char *)stream;
+#endif
+  }
 
-  #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
+#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
   __CPROVER_assert(__CPROVER_get_must(stream, "open"),
                    "fpurge file must be open");
-  #endif
+#endif
 
   return return_value;
 }
@@ -497,20 +522,25 @@ inline int fgetc(FILE *stream)
 {
   __CPROVER_HIDE:;
   int return_value=__VERIFIER_nondet_int();
-  #if !defined(__linux__) || defined(__GLIBC__)
-  (void)*stream;
-  #else
-  (void)*(char*)stream;
-  #endif
+
+  if(stream != stdin)
+  {
+#if !defined(__linux__) || defined(__GLIBC__)
+    (void)*stream;
+#else
+    (void)*(char *)stream;
+#endif
+  }
+
   // it's a byte or EOF (-1)
   __CPROVER_assume(return_value>=-1 && return_value<=255);
 
   __CPROVER_input("fgetc", return_value);
 
-  #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
+#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
   __CPROVER_assert(__CPROVER_get_must(stream, "open"),
                    "fgetc file must be open");
-  #endif
+#endif
 
   return return_value;
 }
@@ -529,16 +559,19 @@ inline int getc(FILE *stream)
   __CPROVER_HIDE:;
   int return_value=__VERIFIER_nondet_int();
 
-  #if !defined(__linux__) || defined(__GLIBC__)
-  (void)*stream;
-  #else
-  (void)*(char*)stream;
-  #endif
+  if(stream != stdin)
+  {
+#if !defined(__linux__) || defined(__GLIBC__)
+    (void)*stream;
+#else
+    (void)*(char *)stream;
+#endif
+  }
 
-  #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
+#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
   __CPROVER_assert(__CPROVER_get_must(stream, "open"),
                    "getc file must be open");
-  #endif
+#endif
 
   // It's a byte or EOF, which we fix to -1.
   __CPROVER_assume(return_value>=-1 && return_value<=255);
@@ -581,16 +614,19 @@ inline int getw(FILE *stream)
   __CPROVER_HIDE:;
   int return_value=__VERIFIER_nondet_int();
 
-  #if !defined(__linux__) || defined(__GLIBC__)
-  (void)*stream;
-  #else
-  (void)*(char*)stream;
-  #endif
+  if(stream != stdin)
+  {
+#if !defined(__linux__) || defined(__GLIBC__)
+    (void)*stream;
+#else
+    (void)*(char *)stream;
+#endif
+  }
 
-  #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
+#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
   __CPROVER_assert(__CPROVER_get_must(stream, "open"),
                    "getw file must be open");
-  #endif
+#endif
 
   __CPROVER_input("getw", return_value);
 
@@ -612,18 +648,18 @@ inline int fseek(FILE *stream, long offset, int whence)
   __CPROVER_HIDE:;
   int return_value=__VERIFIER_nondet_int();
 
-  #if !defined(__linux__) || defined(__GLIBC__)
+#if !defined(__linux__) || defined(__GLIBC__)
   (void)*stream;
-  #else
+#else
   (void)*(char*)stream;
-  #endif
+#endif
   (void)offset;
   (void)whence;
 
-  #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
+#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
   __CPROVER_assert(__CPROVER_get_must(stream, "open"),
                    "fseek file must be open");
-  #endif
+#endif
 
   return return_value;
 }
@@ -642,16 +678,16 @@ inline long ftell(FILE *stream)
   __CPROVER_HIDE:;
   long return_value=__VERIFIER_nondet_long();
 
-  #if !defined(__linux__) || defined(__GLIBC__)
+#if !defined(__linux__) || defined(__GLIBC__)
   (void)*stream;
-  #else
+#else
   (void)*(char*)stream;
-  #endif
+#endif
 
-  #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
+#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
   __CPROVER_assert(__CPROVER_get_must(stream, "open"),
                    "ftell file must be open");
-  #endif
+#endif
 
   return return_value;
 }
@@ -665,18 +701,18 @@ inline long ftell(FILE *stream)
 
 void rewind(FILE *stream)
 {
-  __CPROVER_HIDE:
+__CPROVER_HIDE:
 
-  #if !defined(__linux__) || defined(__GLIBC__)
+#if !defined(__linux__) || defined(__GLIBC__)
   (void)*stream;
-  #else
+#else
   (void)*(char*)stream;
-  #endif
+#endif
 
-  #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
+#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
   __CPROVER_assert(__CPROVER_get_must(stream, "open"),
                    "rewind file must be open");
-  #endif
+#endif
 }
 
 /* FUNCTION: fwrite */
@@ -698,16 +734,19 @@ size_t fwrite(
   (void)*(char*)ptr;
   (void)size;
 
-  #if !defined(__linux__) || defined(__GLIBC__)
-  (void)*stream;
-  #else
-  (void)*(char*)stream;
-  #endif
+  if(stream != stdout && stream != stderr)
+  {
+#if !defined(__linux__) || defined(__GLIBC__)
+    (void)*stream;
+#else
+    (void)*(char *)stream;
+#endif
+  }
 
-  #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
+#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
   __CPROVER_assert(__CPROVER_get_must(stream, "open"),
                    "fwrite file must be open");
-  #endif
+#endif
 
   size_t nwrite=__VERIFIER_nondet_size_t();
   __CPROVER_assume(nwrite<=nitems);
@@ -751,7 +790,7 @@ void perror(const char *s)
 
 inline int fscanf(FILE *restrict stream, const char *restrict format, ...)
 {
-  __CPOVER_HIDE:;
+__CPROVER_HIDE:;
   va_list list;
   va_start(list, format);
   int result=vfscanf(stream, format, list);
@@ -773,7 +812,7 @@ inline int fscanf(FILE *restrict stream, const char *restrict format, ...)
 
 inline int scanf(const char *restrict format, ...)
 {
-  __CPOVER_HIDE:;
+__CPROVER_HIDE:;
   va_list list;
   va_start(list, format);
   int result=vfscanf(stdin, format, list);
@@ -795,7 +834,7 @@ inline int scanf(const char *restrict format, ...)
 
 inline int sscanf(const char *restrict s, const char *restrict format, ...)
 {
-  __CPOVER_HIDE:;
+__CPROVER_HIDE:;
   va_list list;
   va_start(list, format);
   int result=vsscanf(s, format, list);
@@ -821,18 +860,23 @@ inline int vfscanf(FILE *restrict stream, const char *restrict format, va_list a
 {
   __CPROVER_HIDE:;
   int result=__VERIFIER_nondet_int();
-  #if !defined(__linux__) || defined(__GLIBC__)
-  (void)*stream;
-  #else
-  (void)*(char*)stream;
-  #endif
+
+  if(stream != stdin)
+  {
+#if !defined(__linux__) || defined(__GLIBC__)
+    (void)*stream;
+#else
+    (void)*(char *)stream;
+#endif
+  }
+
   (void)*format;
   (void)arg;
 
-  #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
+#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
   __CPROVER_assert(__CPROVER_get_must(stream, "open"),
                    "vfscanf file must be open");
-  #endif
+#endif
 
   return result;
 }
@@ -921,18 +965,22 @@ inline int vfprintf(FILE *stream, const char *restrict format, va_list arg)
 
   int result=__VERIFIER_nondet_int();
 
-  #if !defined(__linux__) || defined(__GLIBC__)
-  (void)*stream;
-  #else
-  (void)*(char*)stream;
-  #endif
+  if(stream != stdout && stream != stderr)
+  {
+#if !defined(__linux__) || defined(__GLIBC__)
+    (void)*stream;
+#else
+    (void)*(char *)stream;
+#endif
+  }
+
   (void)*format;
   (void)arg;
 
-  #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
+#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
   __CPROVER_assert(__CPROVER_get_must(stream, "open"),
                    "vfprintf file must be open");
-  #endif
+#endif
 
   return result;
 }