diff --git a/share/libc/unistd.h b/share/libc/unistd.h
index 46162fb22a34e7cd7212a610fd3b1fbae47bce53..9ee67070df73b4a30d6884ac5c8f021896bac633 100644
--- a/share/libc/unistd.h
+++ b/share/libc/unistd.h
@@ -960,7 +960,19 @@ extern int          isatty(int fd);
 extern int          lchown(const char *, uid_t, gid_t);
 extern int          link(const char *, const char *);
 extern int          lockf(int, int, off_t);
-extern off_t        lseek(int, off_t, int);
+
+/*@ //missing: may assign to errno: EBADF, EINVAL, EOVERFLOW, ESPIPE, ENXIO (Linux);
+  requires valid_fd: 0 <= fd < __FC_MAX_OPEN_FILES;
+  requires valid_whence: whence == SEEK_SET || whence == SEEK_CUR ||
+                         whence == SEEK_END;
+  assigns \result \from indirect:fd, indirect:__fc_fds[fd], indirect:offset,
+                        indirect:whence;
+  assigns __fc_fds[fd] \from indirect:fd, __fc_fds[fd], indirect:offset,
+                             indirect:whence;
+  ensures result_error_or_offset: \result == -1 || 0 <= \result;
+ */
+extern off_t        lseek(int fd, off_t offset, int whence);
+
 extern int          nice(int);
 
 /*@ // missing: may assign to errno: EACCES, EINVAL, ELOOP, ENOENT, ENOTDIR
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 37633dcd6d3636bb942328b54e18c508e16907b6..6e3d1931e3a29df6f54f71de3d15181b471bbc54 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -40,7 +40,7 @@
    unsetenv (0 call); wcscat (0 call); wcscpy (0 call); wcslen (2 calls);
    wcsncat (0 call); wcsncpy (0 call); wmemcpy (0 call); wmemset (0 call); 
   
-  Undefined functions (381)
+  Undefined functions (382)
   =========================
    FD_CLR (0 call); FD_ISSET (0 call); FD_SET (0 call); FD_ZERO (0 call);
    Frama_C_int_interval (0 call); Frama_C_long_interval (0 call);
@@ -109,13 +109,13 @@
    localtime (0 call); log (0 call); log10 (0 call); log10f (0 call);
    log10l (0 call); log2 (0 call); log2f (0 call); log2l (0 call);
    logf (0 call); logl (0 call); longjmp (0 call); lrand48 (0 call);
-   malloc (7 calls); mblen (0 call); mbstowcs (0 call); mbtowc (0 call);
-   mkdir (0 call); mkstemp (0 call); mktime (0 call); mrand48 (0 call);
-   nan (0 call); nanf (0 call); nanl (0 call); nanosleep (0 call);
-   nrand48 (0 call); ntohl (0 call); ntohs (0 call); open (0 call);
-   openat (0 call); opendir (0 call); openlog (0 call); pathconf (0 call);
-   pclose (0 call); perror (0 call); pipe (0 call); poll (0 call);
-   popen (0 call); pow (0 call); powf (0 call);
+   lseek (0 call); malloc (7 calls); mblen (0 call); mbstowcs (0 call);
+   mbtowc (0 call); mkdir (0 call); mkstemp (0 call); mktime (0 call);
+   mrand48 (0 call); nan (0 call); nanf (0 call); nanl (0 call);
+   nanosleep (0 call); nrand48 (0 call); ntohl (0 call); ntohs (0 call);
+   open (0 call); openat (0 call); opendir (0 call); openlog (0 call);
+   pathconf (0 call); pclose (0 call); perror (0 call); pipe (0 call);
+   poll (0 call); popen (0 call); pow (0 call); powf (0 call);
    pthread_cond_broadcast (0 call); pthread_cond_destroy (0 call);
    pthread_cond_init (0 call); pthread_cond_wait (0 call);
    pthread_create (0 call); pthread_join (0 call);
@@ -178,7 +178,7 @@
   Goto = 89
   Assignment = 438
   Exit point = 82
-  Function = 463
+  Function = 464
   Function call = 89
   Pointer dereferencing = 158
   Cyclomatic complexity = 286
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 062a50bfd139232b9eb40071fd09447bdb2a61a9..107f92c67f3f62604ce53ca25bf5a5672e0c65be 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -7499,6 +7499,19 @@ extern uid_t getuid(void);
  */
 extern int isatty(int fd);
 
+/*@ requires valid_fd: 0 ≤ fd < 1024;
+    requires valid_whence: whence ≡ 0 ∨ whence ≡ 1 ∨ whence ≡ 2;
+    ensures result_error_or_offset: \result ≡ -1 ∨ 0 ≤ \result;
+    assigns \result, __fc_fds[fd];
+    assigns \result
+      \from (indirect: fd), (indirect: __fc_fds[fd]), (indirect: offset),
+            (indirect: whence);
+    assigns __fc_fds[fd]
+      \from (indirect: fd), __fc_fds[fd], (indirect: offset),
+            (indirect: whence);
+ */
+extern off_t lseek(int fd, off_t offset, int whence);
+
 /*@ requires valid_path: valid_read_string(path);
     assigns \result;
     assigns \result \from (indirect: *(path + (0 ..))), (indirect: name);
diff --git a/tests/libc/oracle/unistd_h.0.res.oracle b/tests/libc/oracle/unistd_h.0.res.oracle
index 13fef3820e2033fcea8eefc8f370b31d944338a5..5b653c8e60e1ae17db8af7beee6cf8ab0a0e9195 100644
--- a/tests/libc/oracle/unistd_h.0.res.oracle
+++ b/tests/libc/oracle/unistd_h.0.res.oracle
@@ -81,442 +81,453 @@
   Called from tests/libc/unistd_h.c:22.
 [eva] Done for function dup
 [eva] tests/libc/unistd_h.c:23: assertion got status valid.
+[eva] computing for function lseek <- main.
+  Called from tests/libc/unistd_h.c:27.
+[eva] using specification for function lseek
+[eva] tests/libc/unistd_h.c:27: 
+  function lseek: precondition 'valid_fd' got status valid.
+[eva] tests/libc/unistd_h.c:27: 
+  function lseek: precondition 'valid_whence' got status valid.
+[eva] Done for function lseek
+[eva] computing for function lseek <- main.
+  Called from tests/libc/unistd_h.c:27.
+[eva] Done for function lseek
 [eva] computing for function dup2 <- main.
-  Called from tests/libc/unistd_h.c:26.
+  Called from tests/libc/unistd_h.c:30.
 [eva] using specification for function dup2
-[eva] tests/libc/unistd_h.c:26: 
+[eva] tests/libc/unistd_h.c:30: 
   function dup2: precondition 'valid_fildes' got status valid.
-[eva] tests/libc/unistd_h.c:26: 
+[eva] tests/libc/unistd_h.c:30: 
   function dup2: precondition 'valid_fildes2' got status valid.
 [eva] Done for function dup2
 [eva] computing for function dup2 <- main.
-  Called from tests/libc/unistd_h.c:26.
+  Called from tests/libc/unistd_h.c:30.
 [eva] Done for function dup2
 [eva] computing for function dup2 <- main.
-  Called from tests/libc/unistd_h.c:28.
-[eva] tests/libc/unistd_h.c:28: 
+  Called from tests/libc/unistd_h.c:32.
+[eva] tests/libc/unistd_h.c:32: 
   function dup2: precondition 'valid_fildes' got status valid.
-[eva:alarm] tests/libc/unistd_h.c:28: Warning: 
+[eva:alarm] tests/libc/unistd_h.c:32: Warning: 
   function dup2: precondition 'valid_fildes2' got status invalid.
 [eva] Done for function dup2
 [eva] computing for function dup2 <- main.
-  Called from tests/libc/unistd_h.c:28.
+  Called from tests/libc/unistd_h.c:32.
 [eva] Done for function dup2
 [eva] computing for function dup2 <- main.
-  Called from tests/libc/unistd_h.c:28.
+  Called from tests/libc/unistd_h.c:32.
 [eva] Done for function dup2
 [eva] computing for function dup2 <- main.
-  Called from tests/libc/unistd_h.c:28.
+  Called from tests/libc/unistd_h.c:32.
 [eva] Done for function dup2
 [eva] computing for function fork <- main.
-  Called from tests/libc/unistd_h.c:32.
+  Called from tests/libc/unistd_h.c:36.
 [eva] using specification for function fork
 [eva] Done for function fork
 [eva] computing for function fork <- main.
-  Called from tests/libc/unistd_h.c:32.
+  Called from tests/libc/unistd_h.c:36.
 [eva] Done for function fork
 [eva] computing for function fork <- main.
-  Called from tests/libc/unistd_h.c:32.
+  Called from tests/libc/unistd_h.c:36.
 [eva] Done for function fork
 [eva] computing for function fork <- main.
-  Called from tests/libc/unistd_h.c:32.
+  Called from tests/libc/unistd_h.c:36.
 [eva] Done for function fork
-[eva] tests/libc/unistd_h.c:33: assertion got status valid.
+[eva] tests/libc/unistd_h.c:37: assertion got status valid.
 [eva] computing for function setsid <- main.
-  Called from tests/libc/unistd_h.c:35.
+  Called from tests/libc/unistd_h.c:39.
 [eva] using specification for function setsid
 [eva] Done for function setsid
 [eva] computing for function setsid <- main.
-  Called from tests/libc/unistd_h.c:35.
+  Called from tests/libc/unistd_h.c:39.
 [eva] Done for function setsid
 [eva] computing for function setsid <- main.
-  Called from tests/libc/unistd_h.c:35.
+  Called from tests/libc/unistd_h.c:39.
 [eva] Done for function setsid
 [eva] computing for function setsid <- main.
-  Called from tests/libc/unistd_h.c:35.
+  Called from tests/libc/unistd_h.c:39.
 [eva] Done for function setsid
 [eva] computing for function setsid <- main.
-  Called from tests/libc/unistd_h.c:35.
+  Called from tests/libc/unistd_h.c:39.
 [eva] Done for function setsid
 [eva] computing for function setsid <- main.
-  Called from tests/libc/unistd_h.c:35.
+  Called from tests/libc/unistd_h.c:39.
 [eva] Done for function setsid
 [eva] computing for function setsid <- main.
-  Called from tests/libc/unistd_h.c:35.
+  Called from tests/libc/unistd_h.c:39.
 [eva] Done for function setsid
 [eva] computing for function setsid <- main.
-  Called from tests/libc/unistd_h.c:35.
+  Called from tests/libc/unistd_h.c:39.
 [eva] Done for function setsid
 [eva] computing for function setsid <- main.
-  Called from tests/libc/unistd_h.c:35.
+  Called from tests/libc/unistd_h.c:39.
 [eva] Done for function setsid
 [eva] computing for function setsid <- main.
-  Called from tests/libc/unistd_h.c:35.
+  Called from tests/libc/unistd_h.c:39.
 [eva] Done for function setsid
 [eva] computing for function setsid <- main.
-  Called from tests/libc/unistd_h.c:35.
+  Called from tests/libc/unistd_h.c:39.
 [eva] Done for function setsid
 [eva] computing for function setsid <- main.
-  Called from tests/libc/unistd_h.c:35.
+  Called from tests/libc/unistd_h.c:39.
 [eva] Done for function setsid
 [eva] computing for function sync <- main.
-  Called from tests/libc/unistd_h.c:37.
+  Called from tests/libc/unistd_h.c:41.
 [eva] using specification for function sync
 [eva] Done for function sync
 [eva] computing for function sysconf <- main.
-  Called from tests/libc/unistd_h.c:39.
+  Called from tests/libc/unistd_h.c:43.
 [eva] using specification for function sysconf
 [eva] Done for function sysconf
 [eva] computing for function getcwd <- main.
-  Called from tests/libc/unistd_h.c:42.
+  Called from tests/libc/unistd_h.c:46.
 [eva] using specification for function getcwd
-[eva] tests/libc/unistd_h.c:42: 
+[eva] tests/libc/unistd_h.c:46: 
   function getcwd: precondition 'valid_buf' got status valid.
 [eva] Done for function getcwd
-[eva] tests/libc/unistd_h.c:44: assertion got status valid.
-[eva:alarm] tests/libc/unistd_h.c:45: Warning: assertion got status unknown.
+[eva] tests/libc/unistd_h.c:48: assertion got status valid.
+[eva:alarm] tests/libc/unistd_h.c:49: Warning: assertion got status unknown.
 [eva] computing for function pathconf <- main.
-  Called from tests/libc/unistd_h.c:48.
+  Called from tests/libc/unistd_h.c:52.
 [eva] using specification for function pathconf
-[eva] tests/libc/unistd_h.c:48: 
+[eva] tests/libc/unistd_h.c:52: 
   function pathconf: precondition 'valid_path' got status valid.
 [eva] Done for function pathconf
 [eva] computing for function pathconf <- main.
-  Called from tests/libc/unistd_h.c:48.
+  Called from tests/libc/unistd_h.c:52.
 [eva] Done for function pathconf
 [eva] computing for function getresuid <- main.
-  Called from tests/libc/unistd_h.c:51.
+  Called from tests/libc/unistd_h.c:55.
 [eva] using specification for function getresuid
-[eva] tests/libc/unistd_h.c:51: 
+[eva] tests/libc/unistd_h.c:55: 
   function getresuid: precondition 'valid_ruid' got status valid.
-[eva] tests/libc/unistd_h.c:51: 
+[eva] tests/libc/unistd_h.c:55: 
   function getresuid: precondition 'valid_euid' got status valid.
-[eva] tests/libc/unistd_h.c:51: 
+[eva] tests/libc/unistd_h.c:55: 
   function getresuid: precondition 'valid_suid' got status valid.
 [eva] Done for function getresuid
 [eva] computing for function getresuid <- main.
-  Called from tests/libc/unistd_h.c:51.
+  Called from tests/libc/unistd_h.c:55.
 [eva] Done for function getresuid
 [eva] computing for function setresuid <- main.
-  Called from tests/libc/unistd_h.c:53.
+  Called from tests/libc/unistd_h.c:57.
 [eva] using specification for function setresuid
 [eva] Done for function setresuid
 [eva] computing for function setresuid <- main.
-  Called from tests/libc/unistd_h.c:53.
+  Called from tests/libc/unistd_h.c:57.
 [eva] Done for function setresuid
-[eva] tests/libc/unistd_h.c:54: assertion got status valid.
+[eva] tests/libc/unistd_h.c:58: assertion got status valid.
 [eva] computing for function getresgid <- main.
-  Called from tests/libc/unistd_h.c:57.
+  Called from tests/libc/unistd_h.c:61.
 [eva] using specification for function getresgid
-[eva] tests/libc/unistd_h.c:57: 
+[eva] tests/libc/unistd_h.c:61: 
   function getresgid: precondition 'valid_rgid' got status valid.
-[eva] tests/libc/unistd_h.c:57: 
+[eva] tests/libc/unistd_h.c:61: 
   function getresgid: precondition 'valid_egid' got status valid.
-[eva] tests/libc/unistd_h.c:57: 
+[eva] tests/libc/unistd_h.c:61: 
   function getresgid: precondition 'valid_sgid' got status valid.
 [eva] Done for function getresgid
 [eva] computing for function getresgid <- main.
-  Called from tests/libc/unistd_h.c:57.
+  Called from tests/libc/unistd_h.c:61.
 [eva] Done for function getresgid
 [eva] computing for function getresgid <- main.
-  Called from tests/libc/unistd_h.c:57.
+  Called from tests/libc/unistd_h.c:61.
 [eva] Done for function getresgid
 [eva] computing for function getresgid <- main.
-  Called from tests/libc/unistd_h.c:57.
+  Called from tests/libc/unistd_h.c:61.
 [eva] Done for function getresgid
 [eva] computing for function setresgid <- main.
-  Called from tests/libc/unistd_h.c:59.
+  Called from tests/libc/unistd_h.c:63.
 [eva] using specification for function setresgid
 [eva] Done for function setresgid
 [eva] computing for function setresgid <- main.
-  Called from tests/libc/unistd_h.c:59.
+  Called from tests/libc/unistd_h.c:63.
 [eva] Done for function setresgid
-[eva] tests/libc/unistd_h.c:60: assertion got status valid.
+[eva] tests/libc/unistd_h.c:64: assertion got status valid.
 [eva] computing for function getpid <- main.
-  Called from tests/libc/unistd_h.c:62.
+  Called from tests/libc/unistd_h.c:66.
 [eva] using specification for function getpid
 [eva] Done for function getpid
 [eva] computing for function getpid <- main.
-  Called from tests/libc/unistd_h.c:62.
+  Called from tests/libc/unistd_h.c:66.
 [eva] Done for function getpid
 [eva] computing for function getpid <- main.
-  Called from tests/libc/unistd_h.c:62.
+  Called from tests/libc/unistd_h.c:66.
 [eva] Done for function getpid
 [eva] computing for function getpid <- main.
-  Called from tests/libc/unistd_h.c:62.
+  Called from tests/libc/unistd_h.c:66.
 [eva] Done for function getpid
 [eva] computing for function getppid <- main.
-  Called from tests/libc/unistd_h.c:63.
+  Called from tests/libc/unistd_h.c:67.
 [eva] using specification for function getppid
 [eva] Done for function getppid
 [eva] computing for function getppid <- main.
-  Called from tests/libc/unistd_h.c:63.
+  Called from tests/libc/unistd_h.c:67.
 [eva] Done for function getppid
 [eva] computing for function getppid <- main.
-  Called from tests/libc/unistd_h.c:63.
+  Called from tests/libc/unistd_h.c:67.
 [eva] Done for function getppid
 [eva] computing for function getppid <- main.
-  Called from tests/libc/unistd_h.c:63.
+  Called from tests/libc/unistd_h.c:67.
 [eva] Done for function getppid
 [eva] computing for function getsid <- main.
-  Called from tests/libc/unistd_h.c:64.
+  Called from tests/libc/unistd_h.c:68.
 [eva] using specification for function getsid
 [eva] Done for function getsid
 [eva] computing for function getsid <- main.
-  Called from tests/libc/unistd_h.c:64.
+  Called from tests/libc/unistd_h.c:68.
 [eva] Done for function getsid
 [eva] computing for function getsid <- main.
-  Called from tests/libc/unistd_h.c:64.
+  Called from tests/libc/unistd_h.c:68.
 [eva] Done for function getsid
 [eva] computing for function getsid <- main.
-  Called from tests/libc/unistd_h.c:64.
+  Called from tests/libc/unistd_h.c:68.
 [eva] Done for function getsid
 [eva] computing for function getuid <- main.
-  Called from tests/libc/unistd_h.c:65.
+  Called from tests/libc/unistd_h.c:69.
 [eva] using specification for function getuid
 [eva] Done for function getuid
 [eva] computing for function getuid <- main.
-  Called from tests/libc/unistd_h.c:65.
+  Called from tests/libc/unistd_h.c:69.
 [eva] Done for function getuid
 [eva] computing for function getuid <- main.
-  Called from tests/libc/unistd_h.c:65.
+  Called from tests/libc/unistd_h.c:69.
 [eva] Done for function getuid
 [eva] computing for function getuid <- main.
-  Called from tests/libc/unistd_h.c:65.
+  Called from tests/libc/unistd_h.c:69.
 [eva] Done for function getuid
 [eva] computing for function getgid <- main.
-  Called from tests/libc/unistd_h.c:66.
+  Called from tests/libc/unistd_h.c:70.
 [eva] using specification for function getgid
 [eva] Done for function getgid
 [eva] computing for function getgid <- main.
-  Called from tests/libc/unistd_h.c:66.
+  Called from tests/libc/unistd_h.c:70.
 [eva] Done for function getgid
 [eva] computing for function getgid <- main.
-  Called from tests/libc/unistd_h.c:66.
+  Called from tests/libc/unistd_h.c:70.
 [eva] Done for function getgid
 [eva] computing for function getgid <- main.
-  Called from tests/libc/unistd_h.c:66.
+  Called from tests/libc/unistd_h.c:70.
 [eva] Done for function getgid
 [eva] computing for function geteuid <- main.
-  Called from tests/libc/unistd_h.c:67.
+  Called from tests/libc/unistd_h.c:71.
 [eva] using specification for function geteuid
 [eva] Done for function geteuid
 [eva] computing for function geteuid <- main.
-  Called from tests/libc/unistd_h.c:67.
+  Called from tests/libc/unistd_h.c:71.
 [eva] Done for function geteuid
 [eva] computing for function geteuid <- main.
-  Called from tests/libc/unistd_h.c:67.
+  Called from tests/libc/unistd_h.c:71.
 [eva] Done for function geteuid
 [eva] computing for function geteuid <- main.
-  Called from tests/libc/unistd_h.c:67.
+  Called from tests/libc/unistd_h.c:71.
 [eva] Done for function geteuid
 [eva] computing for function getegid <- main.
-  Called from tests/libc/unistd_h.c:68.
+  Called from tests/libc/unistd_h.c:72.
 [eva] using specification for function getegid
 [eva] Done for function getegid
 [eva] computing for function getegid <- main.
-  Called from tests/libc/unistd_h.c:68.
+  Called from tests/libc/unistd_h.c:72.
 [eva] Done for function getegid
 [eva] computing for function getegid <- main.
-  Called from tests/libc/unistd_h.c:68.
+  Called from tests/libc/unistd_h.c:72.
 [eva] Done for function getegid
 [eva] computing for function getegid <- main.
-  Called from tests/libc/unistd_h.c:68.
+  Called from tests/libc/unistd_h.c:72.
 [eva] Done for function getegid
 [eva] computing for function setegid <- main.
-  Called from tests/libc/unistd_h.c:69.
+  Called from tests/libc/unistd_h.c:73.
 [eva] using specification for function setegid
 [eva] Done for function setegid
 [eva] computing for function setegid <- main.
-  Called from tests/libc/unistd_h.c:69.
+  Called from tests/libc/unistd_h.c:73.
 [eva] Done for function setegid
 [eva] computing for function setegid <- main.
-  Called from tests/libc/unistd_h.c:69.
+  Called from tests/libc/unistd_h.c:73.
 [eva] Done for function setegid
 [eva] computing for function setegid <- main.
-  Called from tests/libc/unistd_h.c:69.
+  Called from tests/libc/unistd_h.c:73.
 [eva] Done for function setegid
 [eva] computing for function seteuid <- main.
-  Called from tests/libc/unistd_h.c:70.
+  Called from tests/libc/unistd_h.c:74.
 [eva] using specification for function seteuid
 [eva] Done for function seteuid
 [eva] computing for function seteuid <- main.
-  Called from tests/libc/unistd_h.c:70.
+  Called from tests/libc/unistd_h.c:74.
 [eva] Done for function seteuid
 [eva] computing for function seteuid <- main.
-  Called from tests/libc/unistd_h.c:70.
+  Called from tests/libc/unistd_h.c:74.
 [eva] Done for function seteuid
 [eva] computing for function seteuid <- main.
-  Called from tests/libc/unistd_h.c:70.
+  Called from tests/libc/unistd_h.c:74.
 [eva] Done for function seteuid
 [eva] computing for function setgid <- main.
-  Called from tests/libc/unistd_h.c:71.
+  Called from tests/libc/unistd_h.c:75.
 [eva] using specification for function setgid
 [eva] Done for function setgid
 [eva] computing for function setgid <- main.
-  Called from tests/libc/unistd_h.c:71.
+  Called from tests/libc/unistd_h.c:75.
 [eva] Done for function setgid
 [eva] computing for function setgid <- main.
-  Called from tests/libc/unistd_h.c:71.
+  Called from tests/libc/unistd_h.c:75.
 [eva] Done for function setgid
 [eva] computing for function setgid <- main.
-  Called from tests/libc/unistd_h.c:71.
+  Called from tests/libc/unistd_h.c:75.
 [eva] Done for function setgid
 [eva] computing for function setuid <- main.
-  Called from tests/libc/unistd_h.c:72.
+  Called from tests/libc/unistd_h.c:76.
 [eva] using specification for function setuid
 [eva] Done for function setuid
 [eva] computing for function setuid <- main.
-  Called from tests/libc/unistd_h.c:72.
+  Called from tests/libc/unistd_h.c:76.
 [eva] Done for function setuid
 [eva] computing for function setuid <- main.
-  Called from tests/libc/unistd_h.c:72.
+  Called from tests/libc/unistd_h.c:76.
 [eva] Done for function setuid
 [eva] computing for function setuid <- main.
-  Called from tests/libc/unistd_h.c:72.
+  Called from tests/libc/unistd_h.c:76.
 [eva] Done for function setuid
 [eva] computing for function setregid <- main.
-  Called from tests/libc/unistd_h.c:73.
+  Called from tests/libc/unistd_h.c:77.
 [eva] using specification for function setregid
 [eva] Done for function setregid
 [eva] computing for function setregid <- main.
-  Called from tests/libc/unistd_h.c:73.
+  Called from tests/libc/unistd_h.c:77.
 [eva] Done for function setregid
 [eva] computing for function setregid <- main.
-  Called from tests/libc/unistd_h.c:73.
+  Called from tests/libc/unistd_h.c:77.
 [eva] Done for function setregid
 [eva] computing for function setregid <- main.
-  Called from tests/libc/unistd_h.c:73.
+  Called from tests/libc/unistd_h.c:77.
 [eva] Done for function setregid
 [eva] computing for function setreuid <- main.
-  Called from tests/libc/unistd_h.c:74.
+  Called from tests/libc/unistd_h.c:78.
 [eva] using specification for function setreuid
 [eva] Done for function setreuid
 [eva] computing for function setreuid <- main.
-  Called from tests/libc/unistd_h.c:74.
+  Called from tests/libc/unistd_h.c:78.
 [eva] Done for function setreuid
 [eva] computing for function setreuid <- main.
-  Called from tests/libc/unistd_h.c:74.
+  Called from tests/libc/unistd_h.c:78.
 [eva] Done for function setreuid
 [eva] computing for function setreuid <- main.
-  Called from tests/libc/unistd_h.c:74.
+  Called from tests/libc/unistd_h.c:78.
 [eva] Done for function setreuid
 [eva] computing for function getpgid <- main.
-  Called from tests/libc/unistd_h.c:75.
+  Called from tests/libc/unistd_h.c:79.
 [eva] using specification for function getpgid
 [eva] Done for function getpgid
 [eva] computing for function getpgid <- main.
-  Called from tests/libc/unistd_h.c:75.
+  Called from tests/libc/unistd_h.c:79.
 [eva] Done for function getpgid
 [eva] computing for function getpgid <- main.
-  Called from tests/libc/unistd_h.c:75.
+  Called from tests/libc/unistd_h.c:79.
 [eva] Done for function getpgid
 [eva] computing for function getpgid <- main.
-  Called from tests/libc/unistd_h.c:75.
+  Called from tests/libc/unistd_h.c:79.
 [eva] Done for function getpgid
 [eva] computing for function setpgid <- main.
-  Called from tests/libc/unistd_h.c:75.
+  Called from tests/libc/unistd_h.c:79.
 [eva] using specification for function setpgid
 [eva] Done for function setpgid
 [eva] computing for function setpgid <- main.
-  Called from tests/libc/unistd_h.c:75.
+  Called from tests/libc/unistd_h.c:79.
 [eva] Done for function setpgid
 [eva] computing for function setpgid <- main.
-  Called from tests/libc/unistd_h.c:75.
+  Called from tests/libc/unistd_h.c:79.
 [eva] Done for function setpgid
 [eva] computing for function setpgid <- main.
-  Called from tests/libc/unistd_h.c:75.
+  Called from tests/libc/unistd_h.c:79.
 [eva] Done for function setpgid
 [eva] computing for function getpgrp <- main.
-  Called from tests/libc/unistd_h.c:76.
+  Called from tests/libc/unistd_h.c:80.
 [eva] using specification for function getpgrp
 [eva] Done for function getpgrp
 [eva] computing for function getpgrp <- main.
-  Called from tests/libc/unistd_h.c:76.
+  Called from tests/libc/unistd_h.c:80.
 [eva] Done for function getpgrp
 [eva] computing for function getpgrp <- main.
-  Called from tests/libc/unistd_h.c:76.
+  Called from tests/libc/unistd_h.c:80.
 [eva] Done for function getpgrp
 [eva] computing for function getpgrp <- main.
-  Called from tests/libc/unistd_h.c:76.
+  Called from tests/libc/unistd_h.c:80.
 [eva] Done for function getpgrp
 [eva] computing for function unlink <- main.
-  Called from tests/libc/unistd_h.c:78.
+  Called from tests/libc/unistd_h.c:82.
 [eva] using specification for function unlink
-[eva] tests/libc/unistd_h.c:78: 
+[eva] tests/libc/unistd_h.c:82: 
   function unlink: precondition 'valid_string_path' got status valid.
 [eva] Done for function unlink
 [eva] computing for function unlink <- main.
-  Called from tests/libc/unistd_h.c:78.
+  Called from tests/libc/unistd_h.c:82.
 [eva] Done for function unlink
 [eva] computing for function isatty <- main.
-  Called from tests/libc/unistd_h.c:80.
+  Called from tests/libc/unistd_h.c:84.
 [eva] using specification for function isatty
 [eva] Done for function isatty
 [eva] computing for function isatty <- main.
-  Called from tests/libc/unistd_h.c:80.
+  Called from tests/libc/unistd_h.c:84.
 [eva] Done for function isatty
 [eva] computing for function isatty <- main.
-  Called from tests/libc/unistd_h.c:80.
+  Called from tests/libc/unistd_h.c:84.
 [eva] Done for function isatty
 [eva] computing for function isatty <- main.
-  Called from tests/libc/unistd_h.c:80.
+  Called from tests/libc/unistd_h.c:84.
 [eva] Done for function isatty
-[eva] tests/libc/unistd_h.c:81: assertion got status valid.
+[eva] tests/libc/unistd_h.c:85: assertion got status valid.
 [eva] computing for function ttyname <- main.
-  Called from tests/libc/unistd_h.c:82.
+  Called from tests/libc/unistd_h.c:86.
 [eva] using specification for function ttyname
 [eva] Done for function ttyname
 [eva] computing for function ttyname <- main.
-  Called from tests/libc/unistd_h.c:82.
+  Called from tests/libc/unistd_h.c:86.
 [eva] Done for function ttyname
 [eva] computing for function ttyname <- main.
-  Called from tests/libc/unistd_h.c:82.
+  Called from tests/libc/unistd_h.c:86.
 [eva] Done for function ttyname
 [eva] computing for function ttyname <- main.
-  Called from tests/libc/unistd_h.c:82.
+  Called from tests/libc/unistd_h.c:86.
 [eva] Done for function ttyname
 [eva] computing for function chown <- main.
-  Called from tests/libc/unistd_h.c:84.
+  Called from tests/libc/unistd_h.c:88.
 [eva] using specification for function chown
-[eva] tests/libc/unistd_h.c:84: 
+[eva] tests/libc/unistd_h.c:88: 
   function chown: precondition 'valid_string_path' got status valid.
 [eva] Done for function chown
 [eva] computing for function chown <- main.
-  Called from tests/libc/unistd_h.c:84.
+  Called from tests/libc/unistd_h.c:88.
 [eva] Done for function chown
 [eva] computing for function chown <- main.
-  Called from tests/libc/unistd_h.c:84.
+  Called from tests/libc/unistd_h.c:88.
 [eva] Done for function chown
 [eva] computing for function chown <- main.
-  Called from tests/libc/unistd_h.c:84.
+  Called from tests/libc/unistd_h.c:88.
 [eva] Done for function chown
 [eva] computing for function chown <- main.
-  Called from tests/libc/unistd_h.c:84.
+  Called from tests/libc/unistd_h.c:88.
 [eva] Done for function chown
 [eva] computing for function chown <- main.
-  Called from tests/libc/unistd_h.c:84.
+  Called from tests/libc/unistd_h.c:88.
 [eva] Done for function chown
 [eva] computing for function chown <- main.
-  Called from tests/libc/unistd_h.c:84.
+  Called from tests/libc/unistd_h.c:88.
 [eva] Done for function chown
 [eva] computing for function chown <- main.
-  Called from tests/libc/unistd_h.c:84.
+  Called from tests/libc/unistd_h.c:88.
 [eva] Done for function chown
 [eva] computing for function chdir <- main.
-  Called from tests/libc/unistd_h.c:86.
+  Called from tests/libc/unistd_h.c:90.
 [eva] using specification for function chdir
-[eva] tests/libc/unistd_h.c:86: 
+[eva] tests/libc/unistd_h.c:90: 
   function chdir: precondition 'valid_string_path' got status valid.
 [eva] Done for function chdir
 [eva] computing for function chroot <- main.
-  Called from tests/libc/unistd_h.c:88.
+  Called from tests/libc/unistd_h.c:92.
 [eva] using specification for function chroot
-[eva] tests/libc/unistd_h.c:88: 
+[eva] tests/libc/unistd_h.c:92: 
   function chroot: precondition 'valid_string_path' got status valid.
 [eva] Done for function chroot
 [eva] computing for function chroot <- main.
-  Called from tests/libc/unistd_h.c:88.
+  Called from tests/libc/unistd_h.c:92.
 [eva] Done for function chroot
 [eva] Recording results for main
 [eva] done for function main
@@ -528,6 +539,7 @@
   r ∈ {-1; 0}
   hostname[0..255] ∈ [--..--] or UNINITIALIZED
   fd ∈ [-1..1023]
+  offset ∈ [-1..2147483647]
   fd2 ∈ [-1..1023]
   pid ∈ [-1..2147483647]
   l ∈ [--..--]
diff --git a/tests/libc/oracle/unistd_h.1.res.oracle b/tests/libc/oracle/unistd_h.1.res.oracle
index d81948aa342cb4d58d91c65300dd1772bc54eadc..5cd1bf50f5d48d55f8b70a02c7b37f8b1385336f 100644
--- a/tests/libc/oracle/unistd_h.1.res.oracle
+++ b/tests/libc/oracle/unistd_h.1.res.oracle
@@ -81,442 +81,453 @@
   Called from tests/libc/unistd_h.c:22.
 [eva] Done for function dup
 [eva] tests/libc/unistd_h.c:23: assertion got status valid.
+[eva] computing for function lseek <- main.
+  Called from tests/libc/unistd_h.c:27.
+[eva] using specification for function lseek
+[eva] tests/libc/unistd_h.c:27: 
+  function lseek: precondition 'valid_fd' got status valid.
+[eva] tests/libc/unistd_h.c:27: 
+  function lseek: precondition 'valid_whence' got status valid.
+[eva] Done for function lseek
+[eva] computing for function lseek <- main.
+  Called from tests/libc/unistd_h.c:27.
+[eva] Done for function lseek
 [eva] computing for function dup2 <- main.
-  Called from tests/libc/unistd_h.c:26.
+  Called from tests/libc/unistd_h.c:30.
 [eva] using specification for function dup2
-[eva] tests/libc/unistd_h.c:26: 
+[eva] tests/libc/unistd_h.c:30: 
   function dup2: precondition 'valid_fildes' got status valid.
-[eva] tests/libc/unistd_h.c:26: 
+[eva] tests/libc/unistd_h.c:30: 
   function dup2: precondition 'valid_fildes2' got status valid.
 [eva] Done for function dup2
 [eva] computing for function dup2 <- main.
-  Called from tests/libc/unistd_h.c:26.
+  Called from tests/libc/unistd_h.c:30.
 [eva] Done for function dup2
 [eva] computing for function dup2 <- main.
-  Called from tests/libc/unistd_h.c:28.
-[eva] tests/libc/unistd_h.c:28: 
+  Called from tests/libc/unistd_h.c:32.
+[eva] tests/libc/unistd_h.c:32: 
   function dup2: precondition 'valid_fildes' got status valid.
-[eva:alarm] tests/libc/unistd_h.c:28: Warning: 
+[eva:alarm] tests/libc/unistd_h.c:32: Warning: 
   function dup2: precondition 'valid_fildes2' got status invalid.
 [eva] Done for function dup2
 [eva] computing for function dup2 <- main.
-  Called from tests/libc/unistd_h.c:28.
+  Called from tests/libc/unistd_h.c:32.
 [eva] Done for function dup2
 [eva] computing for function dup2 <- main.
-  Called from tests/libc/unistd_h.c:28.
+  Called from tests/libc/unistd_h.c:32.
 [eva] Done for function dup2
 [eva] computing for function dup2 <- main.
-  Called from tests/libc/unistd_h.c:28.
+  Called from tests/libc/unistd_h.c:32.
 [eva] Done for function dup2
 [eva] computing for function fork <- main.
-  Called from tests/libc/unistd_h.c:32.
+  Called from tests/libc/unistd_h.c:36.
 [eva] using specification for function fork
 [eva] Done for function fork
 [eva] computing for function fork <- main.
-  Called from tests/libc/unistd_h.c:32.
+  Called from tests/libc/unistd_h.c:36.
 [eva] Done for function fork
 [eva] computing for function fork <- main.
-  Called from tests/libc/unistd_h.c:32.
+  Called from tests/libc/unistd_h.c:36.
 [eva] Done for function fork
 [eva] computing for function fork <- main.
-  Called from tests/libc/unistd_h.c:32.
+  Called from tests/libc/unistd_h.c:36.
 [eva] Done for function fork
-[eva] tests/libc/unistd_h.c:33: assertion got status valid.
+[eva] tests/libc/unistd_h.c:37: assertion got status valid.
 [eva] computing for function setsid <- main.
-  Called from tests/libc/unistd_h.c:35.
+  Called from tests/libc/unistd_h.c:39.
 [eva] using specification for function setsid
 [eva] Done for function setsid
 [eva] computing for function setsid <- main.
-  Called from tests/libc/unistd_h.c:35.
+  Called from tests/libc/unistd_h.c:39.
 [eva] Done for function setsid
 [eva] computing for function setsid <- main.
-  Called from tests/libc/unistd_h.c:35.
+  Called from tests/libc/unistd_h.c:39.
 [eva] Done for function setsid
 [eva] computing for function setsid <- main.
-  Called from tests/libc/unistd_h.c:35.
+  Called from tests/libc/unistd_h.c:39.
 [eva] Done for function setsid
 [eva] computing for function setsid <- main.
-  Called from tests/libc/unistd_h.c:35.
+  Called from tests/libc/unistd_h.c:39.
 [eva] Done for function setsid
 [eva] computing for function setsid <- main.
-  Called from tests/libc/unistd_h.c:35.
+  Called from tests/libc/unistd_h.c:39.
 [eva] Done for function setsid
 [eva] computing for function setsid <- main.
-  Called from tests/libc/unistd_h.c:35.
+  Called from tests/libc/unistd_h.c:39.
 [eva] Done for function setsid
 [eva] computing for function setsid <- main.
-  Called from tests/libc/unistd_h.c:35.
+  Called from tests/libc/unistd_h.c:39.
 [eva] Done for function setsid
 [eva] computing for function setsid <- main.
-  Called from tests/libc/unistd_h.c:35.
+  Called from tests/libc/unistd_h.c:39.
 [eva] Done for function setsid
 [eva] computing for function setsid <- main.
-  Called from tests/libc/unistd_h.c:35.
+  Called from tests/libc/unistd_h.c:39.
 [eva] Done for function setsid
 [eva] computing for function setsid <- main.
-  Called from tests/libc/unistd_h.c:35.
+  Called from tests/libc/unistd_h.c:39.
 [eva] Done for function setsid
 [eva] computing for function setsid <- main.
-  Called from tests/libc/unistd_h.c:35.
+  Called from tests/libc/unistd_h.c:39.
 [eva] Done for function setsid
 [eva] computing for function sync <- main.
-  Called from tests/libc/unistd_h.c:37.
+  Called from tests/libc/unistd_h.c:41.
 [eva] using specification for function sync
 [eva] Done for function sync
 [eva] computing for function sysconf <- main.
-  Called from tests/libc/unistd_h.c:39.
+  Called from tests/libc/unistd_h.c:43.
 [eva] using specification for function sysconf
 [eva] Done for function sysconf
 [eva] computing for function getcwd <- main.
-  Called from tests/libc/unistd_h.c:42.
+  Called from tests/libc/unistd_h.c:46.
 [eva] using specification for function getcwd
-[eva] tests/libc/unistd_h.c:42: 
+[eva] tests/libc/unistd_h.c:46: 
   function getcwd: precondition 'valid_buf' got status valid.
 [eva] Done for function getcwd
-[eva] tests/libc/unistd_h.c:44: assertion got status valid.
-[eva:alarm] tests/libc/unistd_h.c:45: Warning: assertion got status unknown.
+[eva] tests/libc/unistd_h.c:48: assertion got status valid.
+[eva:alarm] tests/libc/unistd_h.c:49: Warning: assertion got status unknown.
 [eva] computing for function pathconf <- main.
-  Called from tests/libc/unistd_h.c:48.
+  Called from tests/libc/unistd_h.c:52.
 [eva] using specification for function pathconf
-[eva] tests/libc/unistd_h.c:48: 
+[eva] tests/libc/unistd_h.c:52: 
   function pathconf: precondition 'valid_path' got status valid.
 [eva] Done for function pathconf
 [eva] computing for function pathconf <- main.
-  Called from tests/libc/unistd_h.c:48.
+  Called from tests/libc/unistd_h.c:52.
 [eva] Done for function pathconf
 [eva] computing for function getresuid <- main.
-  Called from tests/libc/unistd_h.c:51.
+  Called from tests/libc/unistd_h.c:55.
 [eva] using specification for function getresuid
-[eva] tests/libc/unistd_h.c:51: 
+[eva] tests/libc/unistd_h.c:55: 
   function getresuid: precondition 'valid_ruid' got status valid.
-[eva] tests/libc/unistd_h.c:51: 
+[eva] tests/libc/unistd_h.c:55: 
   function getresuid: precondition 'valid_euid' got status valid.
-[eva] tests/libc/unistd_h.c:51: 
+[eva] tests/libc/unistd_h.c:55: 
   function getresuid: precondition 'valid_suid' got status valid.
 [eva] Done for function getresuid
 [eva] computing for function getresuid <- main.
-  Called from tests/libc/unistd_h.c:51.
+  Called from tests/libc/unistd_h.c:55.
 [eva] Done for function getresuid
 [eva] computing for function setresuid <- main.
-  Called from tests/libc/unistd_h.c:53.
+  Called from tests/libc/unistd_h.c:57.
 [eva] using specification for function setresuid
 [eva] Done for function setresuid
 [eva] computing for function setresuid <- main.
-  Called from tests/libc/unistd_h.c:53.
+  Called from tests/libc/unistd_h.c:57.
 [eva] Done for function setresuid
-[eva] tests/libc/unistd_h.c:54: assertion got status valid.
+[eva] tests/libc/unistd_h.c:58: assertion got status valid.
 [eva] computing for function getresgid <- main.
-  Called from tests/libc/unistd_h.c:57.
+  Called from tests/libc/unistd_h.c:61.
 [eva] using specification for function getresgid
-[eva] tests/libc/unistd_h.c:57: 
+[eva] tests/libc/unistd_h.c:61: 
   function getresgid: precondition 'valid_rgid' got status valid.
-[eva] tests/libc/unistd_h.c:57: 
+[eva] tests/libc/unistd_h.c:61: 
   function getresgid: precondition 'valid_egid' got status valid.
-[eva] tests/libc/unistd_h.c:57: 
+[eva] tests/libc/unistd_h.c:61: 
   function getresgid: precondition 'valid_sgid' got status valid.
 [eva] Done for function getresgid
 [eva] computing for function getresgid <- main.
-  Called from tests/libc/unistd_h.c:57.
+  Called from tests/libc/unistd_h.c:61.
 [eva] Done for function getresgid
 [eva] computing for function getresgid <- main.
-  Called from tests/libc/unistd_h.c:57.
+  Called from tests/libc/unistd_h.c:61.
 [eva] Done for function getresgid
 [eva] computing for function getresgid <- main.
-  Called from tests/libc/unistd_h.c:57.
+  Called from tests/libc/unistd_h.c:61.
 [eva] Done for function getresgid
 [eva] computing for function setresgid <- main.
-  Called from tests/libc/unistd_h.c:59.
+  Called from tests/libc/unistd_h.c:63.
 [eva] using specification for function setresgid
 [eva] Done for function setresgid
 [eva] computing for function setresgid <- main.
-  Called from tests/libc/unistd_h.c:59.
+  Called from tests/libc/unistd_h.c:63.
 [eva] Done for function setresgid
-[eva] tests/libc/unistd_h.c:60: assertion got status valid.
+[eva] tests/libc/unistd_h.c:64: assertion got status valid.
 [eva] computing for function getpid <- main.
-  Called from tests/libc/unistd_h.c:62.
+  Called from tests/libc/unistd_h.c:66.
 [eva] using specification for function getpid
 [eva] Done for function getpid
 [eva] computing for function getpid <- main.
-  Called from tests/libc/unistd_h.c:62.
+  Called from tests/libc/unistd_h.c:66.
 [eva] Done for function getpid
 [eva] computing for function getpid <- main.
-  Called from tests/libc/unistd_h.c:62.
+  Called from tests/libc/unistd_h.c:66.
 [eva] Done for function getpid
 [eva] computing for function getpid <- main.
-  Called from tests/libc/unistd_h.c:62.
+  Called from tests/libc/unistd_h.c:66.
 [eva] Done for function getpid
 [eva] computing for function getppid <- main.
-  Called from tests/libc/unistd_h.c:63.
+  Called from tests/libc/unistd_h.c:67.
 [eva] using specification for function getppid
 [eva] Done for function getppid
 [eva] computing for function getppid <- main.
-  Called from tests/libc/unistd_h.c:63.
+  Called from tests/libc/unistd_h.c:67.
 [eva] Done for function getppid
 [eva] computing for function getppid <- main.
-  Called from tests/libc/unistd_h.c:63.
+  Called from tests/libc/unistd_h.c:67.
 [eva] Done for function getppid
 [eva] computing for function getppid <- main.
-  Called from tests/libc/unistd_h.c:63.
+  Called from tests/libc/unistd_h.c:67.
 [eva] Done for function getppid
 [eva] computing for function getsid <- main.
-  Called from tests/libc/unistd_h.c:64.
+  Called from tests/libc/unistd_h.c:68.
 [eva] using specification for function getsid
 [eva] Done for function getsid
 [eva] computing for function getsid <- main.
-  Called from tests/libc/unistd_h.c:64.
+  Called from tests/libc/unistd_h.c:68.
 [eva] Done for function getsid
 [eva] computing for function getsid <- main.
-  Called from tests/libc/unistd_h.c:64.
+  Called from tests/libc/unistd_h.c:68.
 [eva] Done for function getsid
 [eva] computing for function getsid <- main.
-  Called from tests/libc/unistd_h.c:64.
+  Called from tests/libc/unistd_h.c:68.
 [eva] Done for function getsid
 [eva] computing for function getuid <- main.
-  Called from tests/libc/unistd_h.c:65.
+  Called from tests/libc/unistd_h.c:69.
 [eva] using specification for function getuid
 [eva] Done for function getuid
 [eva] computing for function getuid <- main.
-  Called from tests/libc/unistd_h.c:65.
+  Called from tests/libc/unistd_h.c:69.
 [eva] Done for function getuid
 [eva] computing for function getuid <- main.
-  Called from tests/libc/unistd_h.c:65.
+  Called from tests/libc/unistd_h.c:69.
 [eva] Done for function getuid
 [eva] computing for function getuid <- main.
-  Called from tests/libc/unistd_h.c:65.
+  Called from tests/libc/unistd_h.c:69.
 [eva] Done for function getuid
 [eva] computing for function getgid <- main.
-  Called from tests/libc/unistd_h.c:66.
+  Called from tests/libc/unistd_h.c:70.
 [eva] using specification for function getgid
 [eva] Done for function getgid
 [eva] computing for function getgid <- main.
-  Called from tests/libc/unistd_h.c:66.
+  Called from tests/libc/unistd_h.c:70.
 [eva] Done for function getgid
 [eva] computing for function getgid <- main.
-  Called from tests/libc/unistd_h.c:66.
+  Called from tests/libc/unistd_h.c:70.
 [eva] Done for function getgid
 [eva] computing for function getgid <- main.
-  Called from tests/libc/unistd_h.c:66.
+  Called from tests/libc/unistd_h.c:70.
 [eva] Done for function getgid
 [eva] computing for function geteuid <- main.
-  Called from tests/libc/unistd_h.c:67.
+  Called from tests/libc/unistd_h.c:71.
 [eva] using specification for function geteuid
 [eva] Done for function geteuid
 [eva] computing for function geteuid <- main.
-  Called from tests/libc/unistd_h.c:67.
+  Called from tests/libc/unistd_h.c:71.
 [eva] Done for function geteuid
 [eva] computing for function geteuid <- main.
-  Called from tests/libc/unistd_h.c:67.
+  Called from tests/libc/unistd_h.c:71.
 [eva] Done for function geteuid
 [eva] computing for function geteuid <- main.
-  Called from tests/libc/unistd_h.c:67.
+  Called from tests/libc/unistd_h.c:71.
 [eva] Done for function geteuid
 [eva] computing for function getegid <- main.
-  Called from tests/libc/unistd_h.c:68.
+  Called from tests/libc/unistd_h.c:72.
 [eva] using specification for function getegid
 [eva] Done for function getegid
 [eva] computing for function getegid <- main.
-  Called from tests/libc/unistd_h.c:68.
+  Called from tests/libc/unistd_h.c:72.
 [eva] Done for function getegid
 [eva] computing for function getegid <- main.
-  Called from tests/libc/unistd_h.c:68.
+  Called from tests/libc/unistd_h.c:72.
 [eva] Done for function getegid
 [eva] computing for function getegid <- main.
-  Called from tests/libc/unistd_h.c:68.
+  Called from tests/libc/unistd_h.c:72.
 [eva] Done for function getegid
 [eva] computing for function setegid <- main.
-  Called from tests/libc/unistd_h.c:69.
+  Called from tests/libc/unistd_h.c:73.
 [eva] using specification for function setegid
 [eva] Done for function setegid
 [eva] computing for function setegid <- main.
-  Called from tests/libc/unistd_h.c:69.
+  Called from tests/libc/unistd_h.c:73.
 [eva] Done for function setegid
 [eva] computing for function setegid <- main.
-  Called from tests/libc/unistd_h.c:69.
+  Called from tests/libc/unistd_h.c:73.
 [eva] Done for function setegid
 [eva] computing for function setegid <- main.
-  Called from tests/libc/unistd_h.c:69.
+  Called from tests/libc/unistd_h.c:73.
 [eva] Done for function setegid
 [eva] computing for function seteuid <- main.
-  Called from tests/libc/unistd_h.c:70.
+  Called from tests/libc/unistd_h.c:74.
 [eva] using specification for function seteuid
 [eva] Done for function seteuid
 [eva] computing for function seteuid <- main.
-  Called from tests/libc/unistd_h.c:70.
+  Called from tests/libc/unistd_h.c:74.
 [eva] Done for function seteuid
 [eva] computing for function seteuid <- main.
-  Called from tests/libc/unistd_h.c:70.
+  Called from tests/libc/unistd_h.c:74.
 [eva] Done for function seteuid
 [eva] computing for function seteuid <- main.
-  Called from tests/libc/unistd_h.c:70.
+  Called from tests/libc/unistd_h.c:74.
 [eva] Done for function seteuid
 [eva] computing for function setgid <- main.
-  Called from tests/libc/unistd_h.c:71.
+  Called from tests/libc/unistd_h.c:75.
 [eva] using specification for function setgid
 [eva] Done for function setgid
 [eva] computing for function setgid <- main.
-  Called from tests/libc/unistd_h.c:71.
+  Called from tests/libc/unistd_h.c:75.
 [eva] Done for function setgid
 [eva] computing for function setgid <- main.
-  Called from tests/libc/unistd_h.c:71.
+  Called from tests/libc/unistd_h.c:75.
 [eva] Done for function setgid
 [eva] computing for function setgid <- main.
-  Called from tests/libc/unistd_h.c:71.
+  Called from tests/libc/unistd_h.c:75.
 [eva] Done for function setgid
 [eva] computing for function setuid <- main.
-  Called from tests/libc/unistd_h.c:72.
+  Called from tests/libc/unistd_h.c:76.
 [eva] using specification for function setuid
 [eva] Done for function setuid
 [eva] computing for function setuid <- main.
-  Called from tests/libc/unistd_h.c:72.
+  Called from tests/libc/unistd_h.c:76.
 [eva] Done for function setuid
 [eva] computing for function setuid <- main.
-  Called from tests/libc/unistd_h.c:72.
+  Called from tests/libc/unistd_h.c:76.
 [eva] Done for function setuid
 [eva] computing for function setuid <- main.
-  Called from tests/libc/unistd_h.c:72.
+  Called from tests/libc/unistd_h.c:76.
 [eva] Done for function setuid
 [eva] computing for function setregid <- main.
-  Called from tests/libc/unistd_h.c:73.
+  Called from tests/libc/unistd_h.c:77.
 [eva] using specification for function setregid
 [eva] Done for function setregid
 [eva] computing for function setregid <- main.
-  Called from tests/libc/unistd_h.c:73.
+  Called from tests/libc/unistd_h.c:77.
 [eva] Done for function setregid
 [eva] computing for function setregid <- main.
-  Called from tests/libc/unistd_h.c:73.
+  Called from tests/libc/unistd_h.c:77.
 [eva] Done for function setregid
 [eva] computing for function setregid <- main.
-  Called from tests/libc/unistd_h.c:73.
+  Called from tests/libc/unistd_h.c:77.
 [eva] Done for function setregid
 [eva] computing for function setreuid <- main.
-  Called from tests/libc/unistd_h.c:74.
+  Called from tests/libc/unistd_h.c:78.
 [eva] using specification for function setreuid
 [eva] Done for function setreuid
 [eva] computing for function setreuid <- main.
-  Called from tests/libc/unistd_h.c:74.
+  Called from tests/libc/unistd_h.c:78.
 [eva] Done for function setreuid
 [eva] computing for function setreuid <- main.
-  Called from tests/libc/unistd_h.c:74.
+  Called from tests/libc/unistd_h.c:78.
 [eva] Done for function setreuid
 [eva] computing for function setreuid <- main.
-  Called from tests/libc/unistd_h.c:74.
+  Called from tests/libc/unistd_h.c:78.
 [eva] Done for function setreuid
 [eva] computing for function getpgid <- main.
-  Called from tests/libc/unistd_h.c:75.
+  Called from tests/libc/unistd_h.c:79.
 [eva] using specification for function getpgid
 [eva] Done for function getpgid
 [eva] computing for function getpgid <- main.
-  Called from tests/libc/unistd_h.c:75.
+  Called from tests/libc/unistd_h.c:79.
 [eva] Done for function getpgid
 [eva] computing for function getpgid <- main.
-  Called from tests/libc/unistd_h.c:75.
+  Called from tests/libc/unistd_h.c:79.
 [eva] Done for function getpgid
 [eva] computing for function getpgid <- main.
-  Called from tests/libc/unistd_h.c:75.
+  Called from tests/libc/unistd_h.c:79.
 [eva] Done for function getpgid
 [eva] computing for function setpgid <- main.
-  Called from tests/libc/unistd_h.c:75.
+  Called from tests/libc/unistd_h.c:79.
 [eva] using specification for function setpgid
 [eva] Done for function setpgid
 [eva] computing for function setpgid <- main.
-  Called from tests/libc/unistd_h.c:75.
+  Called from tests/libc/unistd_h.c:79.
 [eva] Done for function setpgid
 [eva] computing for function setpgid <- main.
-  Called from tests/libc/unistd_h.c:75.
+  Called from tests/libc/unistd_h.c:79.
 [eva] Done for function setpgid
 [eva] computing for function setpgid <- main.
-  Called from tests/libc/unistd_h.c:75.
+  Called from tests/libc/unistd_h.c:79.
 [eva] Done for function setpgid
 [eva] computing for function getpgrp <- main.
-  Called from tests/libc/unistd_h.c:76.
+  Called from tests/libc/unistd_h.c:80.
 [eva] using specification for function getpgrp
 [eva] Done for function getpgrp
 [eva] computing for function getpgrp <- main.
-  Called from tests/libc/unistd_h.c:76.
+  Called from tests/libc/unistd_h.c:80.
 [eva] Done for function getpgrp
 [eva] computing for function getpgrp <- main.
-  Called from tests/libc/unistd_h.c:76.
+  Called from tests/libc/unistd_h.c:80.
 [eva] Done for function getpgrp
 [eva] computing for function getpgrp <- main.
-  Called from tests/libc/unistd_h.c:76.
+  Called from tests/libc/unistd_h.c:80.
 [eva] Done for function getpgrp
 [eva] computing for function unlink <- main.
-  Called from tests/libc/unistd_h.c:78.
+  Called from tests/libc/unistd_h.c:82.
 [eva] using specification for function unlink
-[eva] tests/libc/unistd_h.c:78: 
+[eva] tests/libc/unistd_h.c:82: 
   function unlink: precondition 'valid_string_path' got status valid.
 [eva] Done for function unlink
 [eva] computing for function unlink <- main.
-  Called from tests/libc/unistd_h.c:78.
+  Called from tests/libc/unistd_h.c:82.
 [eva] Done for function unlink
 [eva] computing for function isatty <- main.
-  Called from tests/libc/unistd_h.c:80.
+  Called from tests/libc/unistd_h.c:84.
 [eva] using specification for function isatty
 [eva] Done for function isatty
 [eva] computing for function isatty <- main.
-  Called from tests/libc/unistd_h.c:80.
+  Called from tests/libc/unistd_h.c:84.
 [eva] Done for function isatty
 [eva] computing for function isatty <- main.
-  Called from tests/libc/unistd_h.c:80.
+  Called from tests/libc/unistd_h.c:84.
 [eva] Done for function isatty
 [eva] computing for function isatty <- main.
-  Called from tests/libc/unistd_h.c:80.
+  Called from tests/libc/unistd_h.c:84.
 [eva] Done for function isatty
-[eva] tests/libc/unistd_h.c:81: assertion got status valid.
+[eva] tests/libc/unistd_h.c:85: assertion got status valid.
 [eva] computing for function ttyname <- main.
-  Called from tests/libc/unistd_h.c:82.
+  Called from tests/libc/unistd_h.c:86.
 [eva] using specification for function ttyname
 [eva] Done for function ttyname
 [eva] computing for function ttyname <- main.
-  Called from tests/libc/unistd_h.c:82.
+  Called from tests/libc/unistd_h.c:86.
 [eva] Done for function ttyname
 [eva] computing for function ttyname <- main.
-  Called from tests/libc/unistd_h.c:82.
+  Called from tests/libc/unistd_h.c:86.
 [eva] Done for function ttyname
 [eva] computing for function ttyname <- main.
-  Called from tests/libc/unistd_h.c:82.
+  Called from tests/libc/unistd_h.c:86.
 [eva] Done for function ttyname
 [eva] computing for function chown <- main.
-  Called from tests/libc/unistd_h.c:84.
+  Called from tests/libc/unistd_h.c:88.
 [eva] using specification for function chown
-[eva] tests/libc/unistd_h.c:84: 
+[eva] tests/libc/unistd_h.c:88: 
   function chown: precondition 'valid_string_path' got status valid.
 [eva] Done for function chown
 [eva] computing for function chown <- main.
-  Called from tests/libc/unistd_h.c:84.
+  Called from tests/libc/unistd_h.c:88.
 [eva] Done for function chown
 [eva] computing for function chown <- main.
-  Called from tests/libc/unistd_h.c:84.
+  Called from tests/libc/unistd_h.c:88.
 [eva] Done for function chown
 [eva] computing for function chown <- main.
-  Called from tests/libc/unistd_h.c:84.
+  Called from tests/libc/unistd_h.c:88.
 [eva] Done for function chown
 [eva] computing for function chown <- main.
-  Called from tests/libc/unistd_h.c:84.
+  Called from tests/libc/unistd_h.c:88.
 [eva] Done for function chown
 [eva] computing for function chown <- main.
-  Called from tests/libc/unistd_h.c:84.
+  Called from tests/libc/unistd_h.c:88.
 [eva] Done for function chown
 [eva] computing for function chown <- main.
-  Called from tests/libc/unistd_h.c:84.
+  Called from tests/libc/unistd_h.c:88.
 [eva] Done for function chown
 [eva] computing for function chown <- main.
-  Called from tests/libc/unistd_h.c:84.
+  Called from tests/libc/unistd_h.c:88.
 [eva] Done for function chown
 [eva] computing for function chdir <- main.
-  Called from tests/libc/unistd_h.c:86.
+  Called from tests/libc/unistd_h.c:90.
 [eva] using specification for function chdir
-[eva] tests/libc/unistd_h.c:86: 
+[eva] tests/libc/unistd_h.c:90: 
   function chdir: precondition 'valid_string_path' got status valid.
 [eva] Done for function chdir
 [eva] computing for function chroot <- main.
-  Called from tests/libc/unistd_h.c:88.
+  Called from tests/libc/unistd_h.c:92.
 [eva] using specification for function chroot
-[eva] tests/libc/unistd_h.c:88: 
+[eva] tests/libc/unistd_h.c:92: 
   function chroot: precondition 'valid_string_path' got status valid.
 [eva] Done for function chroot
 [eva] computing for function chroot <- main.
-  Called from tests/libc/unistd_h.c:88.
+  Called from tests/libc/unistd_h.c:92.
 [eva] Done for function chroot
 [eva] Recording results for main
 [eva] done for function main
@@ -528,6 +539,7 @@
   r ∈ {-1; 0}
   hostname[0..255] ∈ [--..--] or UNINITIALIZED
   fd ∈ [-1..1023]
+  offset ∈ [-1..2147483647]
   fd2 ∈ [-1..1023]
   pid ∈ [-1..2147483647]
   l ∈ [--..--]
diff --git a/tests/libc/unistd_h.c b/tests/libc/unistd_h.c
index b98727450e8373158e5814f75357260cf2186f2e..b625b3b83d2d10e57806e83a9bf73d7521d08134 100644
--- a/tests/libc/unistd_h.c
+++ b/tests/libc/unistd_h.c
@@ -23,6 +23,10 @@ int main() {
   //@ assert fd == -1 || fd >= 0;
   if (fd == -1) return 1;
 
+  off_t offset = 42;
+  offset = lseek(fd, offset, SEEK_SET);
+  if (offset == -1) return 1;
+
   int fd2 = dup2(2, fd);
   if (nondet) {
     dup2(2, -2);