diff --git a/share/libc/__fc_libc.h b/share/libc/__fc_libc.h
index 6e43667ac7d10ff995a1a2977499d078c211dbd6..70797ab496ba327e5d905f4b714b6f036b786d41 100644
--- a/share/libc/__fc_libc.h
+++ b/share/libc/__fc_libc.h
@@ -28,9 +28,11 @@
 #define _GNU_SOURCE 1
 
 #include "alloca.h"
+#include "argz.h"
 #include "arpa/inet.h"
 #include "assert.h"
 #include "byteswap.h"
+//#include "complex.h"
 #include "ctype.h"
 #include "dirent.h"
 #include "dlfcn.h"
@@ -93,6 +95,7 @@
 #include "sys/signal.h"
 #include "sys/socket.h"
 #include "sys/stat.h"
+#include "sys/statvfs.h"
 #include "sys/time.h"
 #include "sys/times.h"
 #include "sys/timex.h"
@@ -100,8 +103,10 @@
 #include "sys/uio.h"
 #include "sys/un.h"
 #include "sys/utsname.h"
+#include "sys/vfs.h"
 #include "sys/wait.h"
 #include "termios.h"
+//#include "tgmath.h"
 #include "time.h"
 #include "unistd.h"
 #include "utime.h"
diff --git a/tests/libc/check_full_libc.sh b/tests/libc/check_full_libc.sh
index ebfc06b481cff211a34b3a2988902444058bc48e..7725be701dad428d3090f5b7cb26ff92ad6e545e 100755
--- a/tests/libc/check_full_libc.sh
+++ b/tests/libc/check_full_libc.sh
@@ -1,17 +1,31 @@
-#!/bin/sh
+#!/bin/sh -eu
+
+errors=0
 
 cd share/libc
 
-for A in `ls *.h */*.h`;
-do
-    if ! grep -q $A ../../tests/libc/fc_libc.c ;
-    then echo "#include \"$A"\";
-    fi ;
-done;
+for A in *.h */*.h; do
+    if ! grep -q $A ../../tests/libc/fc_libc.c
+    then
+        echo "missing include in tests/libc/fc_libc.c: $A"
+        errors=$((errors+1))
+    fi
+    if ! grep -q $A __fc_libc.h && [ "${A#__fc_}" = "$A" ]
+    then
+        echo "missing include in share/libc/__fc_libc.h: $A"
+        errors=$((errors+1))
+    fi
+done
+
+for A in *.c */*.c; do
+    if ! grep -q $A __fc_runtime.c ../../tests/libc/fc_libc.c
+    then
+        echo "missing include in share/libc/__fc_runtime.c or tests/libc/fc_libc.c: $A"
+        errors=$((errors+1))
+    fi
+done
 
-for A in `ls *.c`;
-do
-    if ! grep -q $A __fc_runtime.c ../../tests/libc/fc_libc.c ;
-    then echo Not included implementation \'$A\';
-    fi ;
-done;
+if [ $errors -gt 0 ]; then
+    echo "found $errors error(s) in libc"
+    exit 1
+fi
diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c
index 51926233b9a8d16727ff13366ac42aca75a7b7ec..1345145e950c37a80e559c9426ab5a2ce0dc968e 100644
--- a/tests/libc/fc_libc.c
+++ b/tests/libc/fc_libc.c
@@ -52,6 +52,7 @@
 #include "__fc_define_intptr_t.h"
 #include "__fc_define_iovec.h"
 #include "__fc_define_key_t.h"
+#include "__fc_define_max_open_files.h"
 #include "__fc_define_mode_t.h"
 #include "__fc_define_nlink_t.h"
 #include "__fc_define_null.h"
@@ -75,8 +76,10 @@
 #include "__fc_define_wint_t.h"
 #include "__fc_gcc_builtins.h"
 #include "__fc_inet.h"
+#include "__fc_integer.h"
+//#include "__fc_libc.h" //keep this; used by check_full_libc.sh
 #include "__fc_machdep.h"
-//#include "__fc_machdep_linux_shared.h"
+//#include "__fc_machdep_linux_shared.h" //keep this; used by check_full_libc.sh
 #include "fcntl.h"
 #include "__fc_select.h"
 #include "__fc_string_axiomatic.h"
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 6278f20effa1ed041e3738067215c23f99a13f7b..a6771559129e315e277116165b1c711cf24cdf02 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -4,10 +4,10 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[eva] tests/libc/fc_libc.c:161: assertion got status valid.
-[eva] tests/libc/fc_libc.c:162: assertion got status valid.
-[eva] tests/libc/fc_libc.c:163: assertion got status valid.
 [eva] tests/libc/fc_libc.c:164: assertion got status valid.
+[eva] tests/libc/fc_libc.c:165: assertion got status valid.
+[eva] tests/libc/fc_libc.c:166: assertion got status valid.
+[eva] tests/libc/fc_libc.c:167: assertion got status valid.
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
@@ -212,6 +212,7 @@
 #include "__fc_builtin.h"
 #include "__fc_define_fd_set_t.h"
 #include "__fc_gcc_builtins.h"
+#include "__fc_integer.h"
 #include "__fc_select.h"
 #include "alloca.h"
 #include "argz.c"
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 6fb5f06d16b6e8ccc089918c6586812c43025be6..0bd9434fdceacd887dffcdb20ea051318bf58ca8 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -8033,6 +8033,9 @@ int __builtin_popcountl(unsigned long x);
  */
 int __builtin_popcountll(unsigned long long x);
 
+/*@ logic 𝔹 bit_test(ℤ x, ℤ pos) = (x & (1 << pos)) ≢ 0;
+
+*/
 /*@ requires valid_filename: valid_read_string(filename);
     assigns \result;
     assigns \result \from (indirect: *(filename + (0 ..))), (indirect: mode);
diff --git a/tests/libc/oracle/fc_libc.5.res.oracle b/tests/libc/oracle/fc_libc.5.res.oracle
deleted file mode 100644
index 7e6030e35546a1b40a346c2cb6b186cf1b6f488a..0000000000000000000000000000000000000000
--- a/tests/libc/oracle/fc_libc.5.res.oracle
+++ /dev/null
@@ -1,3 +0,0 @@
-#include "__fc_define_max_open_files.h"
-#include "__fc_integer.h"
-#include "__fc_libc.h"