diff --git a/share/libc/time.h b/share/libc/time.h
index bfc3f053de3dec9374f272fdaca9f5efb4dfb33b..a0958995d762046f0bbb91844369da0b190750b9 100644
--- a/share/libc/time.h
+++ b/share/libc/time.h
@@ -159,9 +159,8 @@ extern struct tm *localtime(const time_t *timer);
   assigns s[0 .. max-1] \from indirect:max, indirect:format[0..], indirect:*tm;
   assigns \result \from indirect:max, indirect:format[0..], indirect:*tm;
   ensures result_bounded: \result < max;
-  ensures result_valid_string: valid_string(s);
-  ensures result_length: s[\result] == 0;
-  ensures max: s[max-1] == 0;
+  ensures result_valid_string: \result > 0 ==> valid_string(s);
+  ensures result_length: \result > 0 ==> s[\result] == 0;
  */
 extern size_t strftime(char * restrict s,
                        size_t max,
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 9ef75177e38de2c48eaa12287c832925b08efee0..9e2fa656c310fb16960eeecf4a4f44200e2301af 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -5116,9 +5116,8 @@ extern struct tm *localtime(time_t const *timer);
     requires valid_format: valid_read_string(format);
     requires valid_tm: \valid_read(tm);
     ensures result_bounded: \result < \old(max);
-    ensures result_valid_string: valid_string(\old(s));
-    ensures result_length: *(\old(s) + \result) ≡ 0;
-    ensures max: *(\old(s) + (\old(max) - 1)) ≡ 0;
+    ensures result_valid_string: \result > 0 ⇒ valid_string(\old(s));
+    ensures result_length: \result > 0 ⇒ *(\old(s) + \result) ≡ 0;
     assigns *(s + (0 .. max - 1)), \result;
     assigns *(s + (0 .. max - 1))
       \from (indirect: max), (indirect: *(format + (0 ..))), (indirect: *tm);