diff --git a/share/libc/pthread.h b/share/libc/pthread.h
index 84131d8aab4d130b7889900b63bc75ec0b9bc8eb..08c08ca6449dc213d5137bf473b61ea2a0456544 100644
--- a/share/libc/pthread.h
+++ b/share/libc/pthread.h
@@ -319,8 +319,9 @@ extern int pthread_mutex_unlock(pthread_mutex_t *mutex);
 
 /*@
   requires valid_attr: \valid(attr);
-  assigns \result, *attr \from \nothing;
-  ensures success: \result == 0;
+  assigns *attr \from *attr;
+  assigns \result \from indirect:*attr;
+  ensures success_or_error: \result == 0 || \result == EINVAL;
  */
 extern int pthread_mutexattr_destroy(pthread_mutexattr_t *attr);
 
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 29a563fb2eb5ca45b840bb5c4c7bfa51574fd7ed..ce58bfc1d77c678e3830be35184dd8f5c0510906 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -7789,10 +7789,10 @@ extern int pthread_mutex_lock(pthread_mutex_t *mutex);
 extern int pthread_mutex_unlock(pthread_mutex_t *mutex);
 
 /*@ requires valid_attr: \valid(attr);
-    ensures success: \result ≡ 0;
-    assigns \result, *attr;
-    assigns \result \from \nothing;
-    assigns *attr \from \nothing;
+    ensures success_or_error: \result ≡ 0 ∨ \result ≡ 22;
+    assigns *attr, \result;
+    assigns *attr \from *attr;
+    assigns \result \from (indirect: *attr);
  */
 extern int pthread_mutexattr_destroy(pthread_mutexattr_t *attr);