diff --git a/share/libc/inttypes.h b/share/libc/inttypes.h
index 0f4880d33e6eb972956f59c942aff8898c3d2422..49becc11ad8aaf4c816cb85cac8aae27c5f24874 100644
--- a/share/libc/inttypes.h
+++ b/share/libc/inttypes.h
@@ -253,9 +253,12 @@ typedef struct __fc_imaxdiv_t
   } imaxdiv_t;
 
 /* ISO C: 7.8.2 */
-/*@ 
-  requires abs_representable: (intmax_t)(-c) != c ;
-  assigns \result \from c ; 
+/*@
+  requires abs_representable: c > INTMAX_MIN;
+  assigns \result \from c;
+  ensures positive_result: \result >= 0.;
+  ensures equal_magnitude_result: \result == c || \result == -c;
+  ensures logical_abs_result: \result == \abs(c);
 */
 extern intmax_t imaxabs(intmax_t c);
 
diff --git a/tests/libc/inttypes_h2.c b/tests/libc/inttypes_h2.c
index afc8226a0cdc3812504ac1abf0abae80d6ba3fd9..331ffd2e80d647d430ef76709ffa4105fc6c0c12 100644
--- a/tests/libc/inttypes_h2.c
+++ b/tests/libc/inttypes_h2.c
@@ -22,4 +22,11 @@ void main() {
   r = imaxdiv(a, b);
   //@ assert r.quot == 2;
   //@ assert r.rem == 1;
+
+  a = imaxabs(INTMAX_MAX);
+  //@ assert a == INTMAX_MAX;
+  a = imaxabs(INTMAX_MIN + 1);
+  //@ assert a >= 0;
+  a = imaxabs(0);
+  //@ assert a == 0;
 }
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index f0d19dd5efcdf4900a7f4d174aa4463e22c395df..be0c42e75318b30374f12a8cf0c5bbd05ec53a3c 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -2671,7 +2671,11 @@ imaxdiv_t imaxdiv(intmax_t numer, intmax_t denom);
 extern intmax_t strtoimax(char const * __restrict nptr,
                           char ** __restrict endptr, int base);
 
-/*@ requires abs_representable: (long long)(-c) ≢ c;
+/*@ requires abs_representable: c > -9223372036854775807LL - 1LL;
+    ensures positive_result: \result ≥ 0.;
+    ensures
+      equal_magnitude_result: \result ≡ \old(c) ∨ \result ≡ -\old(c);
+    ensures logical_abs_result: \result ≡ \abs(\old(c));
     assigns \result;
     assigns \result \from c;
  */
diff --git a/tests/libc/oracle/inttypes_h2.res.oracle b/tests/libc/oracle/inttypes_h2.res.oracle
index 74e8d8c2d1694c77beb00f6a11180484a9cf1339..fa8a9832adb194582176814a024d849f34aa19d0 100644
--- a/tests/libc/oracle/inttypes_h2.res.oracle
+++ b/tests/libc/oracle/inttypes_h2.res.oracle
@@ -28,11 +28,30 @@
 [eva] Done for function imaxdiv
 [eva] tests/libc/inttypes_h2.c:23: assertion got status valid.
 [eva] tests/libc/inttypes_h2.c:24: assertion got status valid.
+[eva] computing for function imaxabs <- main.
+  Called from tests/libc/inttypes_h2.c:26.
+[eva] using specification for function imaxabs
+[eva] tests/libc/inttypes_h2.c:26: 
+  function imaxabs: precondition 'abs_representable' got status valid.
+[eva] Done for function imaxabs
+[eva] tests/libc/inttypes_h2.c:27: assertion got status valid.
+[eva] computing for function imaxabs <- main.
+  Called from tests/libc/inttypes_h2.c:28.
+[eva] tests/libc/inttypes_h2.c:28: 
+  function imaxabs: precondition 'abs_representable' got status valid.
+[eva] Done for function imaxabs
+[eva] tests/libc/inttypes_h2.c:29: assertion got status valid.
+[eva] computing for function imaxabs <- main.
+  Called from tests/libc/inttypes_h2.c:30.
+[eva] tests/libc/inttypes_h2.c:30: 
+  function imaxabs: precondition 'abs_representable' got status valid.
+[eva] Done for function imaxabs
+[eva] tests/libc/inttypes_h2.c:31: assertion got status valid.
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
-  a ∈ {9223372036854775807}
+  a ∈ {0}
   b ∈ {4611686018427387903}
   r.quot ∈ {2}
    .rem ∈ {1}