diff --git a/tests/stl/oracle/stl_system_error.res.oracle b/tests/stl/oracle/stl_system_error.res.oracle
index c5d8f82646028b37b94afc1098d53c0909e6731b..ed910e4f93c8e9915dce76d21e86da7af4bcdb00 100644
--- a/tests/stl/oracle/stl_system_error.res.oracle
+++ b/tests/stl/oracle/stl_system_error.res.oracle
@@ -1735,6 +1735,18 @@ time_t time(time_t *timer);
 
 char __fc_ctime[26];
 char * const __fc_p_ctime = __fc_ctime;
+/*@ requires valid_timeptr: \valid_read(timeptr);
+    requires init_timeptr: initialization: \initialized(timeptr);
+    ensures result_points_to_ctime: \result ≡ __fc_p_ctime;
+    ensures result_valid_string: valid_read_string(__fc_p_ctime);
+    assigns __fc_ctime[0 .. 25], \result;
+    assigns __fc_ctime[0 .. 25]
+      \from (indirect: *timeptr), (indirect: __fc_time);
+    assigns \result
+      \from (indirect: *timeptr), (indirect: __fc_time), __fc_p_ctime;
+ */
+char *asctime(struct tm const *timeptr);
+
 /*@ requires valid_timer: \valid_read(timer);
     requires init_timer: initialization: \initialized(timer);
     ensures result_points_to_ctime: \result ≡ __fc_p_ctime;