diff --git a/share/libc/math.h b/share/libc/math.h
index 6924d5cab8983f2d1d60cfc9794e965e0e986a71..ec8b3111f434af48b20d7f3f6b75217b3333d9ed 100644
--- a/share/libc/math.h
+++ b/share/libc/math.h
@@ -257,7 +257,7 @@ extern long double asinl(long double x);
 /*@
   assigns \result \from x;
   behavior normal:
-    assumes finite_arg: !\is_NaN(x);
+    assumes number_arg: !\is_NaN(x);
     ensures finite_result: \is_finite(\result);
     ensures result_domain: -1.571 <= \result <= 1.571;
   behavior nan:
@@ -348,7 +348,7 @@ extern long double atan2l(long double y, long double x);
     ensures nan_result: \is_NaN(\result);
     ensures errno_set: errno == EDOM;
   behavior nan:
-    assumes nan_arg: !\is_NaN(x);
+    assumes nan_arg: \is_NaN(x);
     assigns \result \from x;
     ensures nan_result: \is_NaN(\result);
     ensures no_error: errno == \old(errno);
@@ -370,7 +370,7 @@ extern double cos(double x);
     ensures nan_result: \is_NaN(\result);
     ensures errno_set: errno == EDOM;
   behavior nan:
-    assumes nan_arg: !\is_NaN(x);
+    assumes nan_arg: \is_NaN(x);
     assigns \result \from x;
     ensures nan_result: \is_NaN(\result);
     ensures no_error: errno == \old(errno);
@@ -392,7 +392,7 @@ extern float cosf(float x);
     ensures nan_result: \is_NaN(\result);
     ensures errno_set: errno == EDOM;
   behavior nan:
-    assumes nan_arg: !\is_NaN(x);
+    assumes nan_arg: \is_NaN(x);
     assigns \result \from x;
     ensures nan_result: \is_NaN(\result);
     ensures no_error: errno == \old(errno);
@@ -414,7 +414,7 @@ extern long double cosl(long double x);
     ensures nan_result: \is_NaN(\result);
     ensures errno_set: errno == EDOM;
   behavior nan:
-    assumes nan_arg: !\is_NaN(x);
+    assumes nan_arg: \is_NaN(x);
     assigns \result \from x;
     ensures nan_result: \is_NaN(\result);
     ensures no_error: errno == \old(errno);
@@ -436,7 +436,7 @@ extern double sin(double x);
     ensures nan_result: \is_NaN(\result);
     ensures errno_set: errno == EDOM;
   behavior nan:
-    assumes nan_arg: !\is_NaN(x);
+    assumes nan_arg: \is_NaN(x);
     assigns \result \from x;
     ensures nan_result: \is_NaN(\result);
     ensures no_error: errno == \old(errno);
@@ -458,7 +458,7 @@ extern float sinf(float x);
     ensures nan_result: \is_NaN(\result);
     ensures errno_set: errno == EDOM;
   behavior nan:
-    assumes nan_arg: !\is_NaN(x);
+    assumes nan_arg: \is_NaN(x);
     assigns \result \from x;
     ensures nan_result: \is_NaN(\result);
     ensures no_error: errno == \old(errno);
diff --git a/tests/float/oracle/math_builtins.res.oracle b/tests/float/oracle/math_builtins.res.oracle
index 14723be574dbd03a221bebd1519fe28699bd41f8..9a64da6cd76b95048bf2a07740832d45662ca252 100644
--- a/tests/float/oracle/math_builtins.res.oracle
+++ b/tests/float/oracle/math_builtins.res.oracle
@@ -164,10 +164,10 @@
   function atan: precondition 'number_arg' got status valid.
 [eva] tests/float/math_builtins.c:94: Call to builtin atanf
 [eva] tests/float/math_builtins.c:94: 
-  function atanf: precondition 'finite_arg' got status valid.
+  function atanf: precondition 'number_arg' got status valid.
 [eva] tests/float/math_builtins.c:95: Call to builtin atanf
 [eva:alarm] tests/float/math_builtins.c:95: Warning: 
-  function atanf: precondition 'finite_arg' got status unknown.
+  function atanf: precondition 'number_arg' got status unknown.
 [eva] Recording results for test_atan
 [eva] Done for function test_atan
 [eva] computing for function test_atan2_det <- main.
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 8390d1842cfd8015387e9f05d813f988f2e0609b..e6c4205c8dec47582eedad576a38473f38fe8420 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -2887,7 +2887,7 @@ extern float asinf(float x);
  */
 extern long double asinl(long double x);
 
-/*@ requires finite_arg: ¬\is_NaN(x);
+/*@ requires number_arg: ¬\is_NaN(x);
     ensures finite_result: \is_finite(\result);
     ensures result_domain: -1.571 ≤ \result ≤ 1.571;
     assigns \result;