Result from Ziyuan: We feed the passed test cases from Ziyuan to Daikon. However, after a while, Daikon only returns OutOfMemoryError. The input of FailureDoc is a sequence. In this case, we manually create below sequences as its input. However, FailureDoc says that the sequences have not error and does not give any explanation. START SEQUENCE var0 = prim : int:0 : var1 = prim : int:-15 : var2 = method : org.joda.time.DateTimeZone.forOffsetHoursMinutes(int,int) : var0 var1 END SEQUENCE START SEQUENCE var0 = prim : int:-2 : var1 = prim : int:-15 : var2 = method : org.joda.time.DateTimeZone.forOffsetHoursMinutes(int,int) : var0 var1 END SEQUENCE
if (minutesOffset < 0 || minutesOffset > 59) throw Exception
That means the program is safe with minuteOffset in range [0, 59]. However, this code is not the behaviour that programmers want. So later, they change it to
if (minutesOffset < -59 || minutesOffset > 59) throw Exception
Using the provided test cases (with two failed test cases), Ziyuan can learn the predicate
minutesOffset >= 0.0 (org.joda.time.DateTimeZone:279)
Clearly we can use this predicate to understand the behaviour of the program before fixed.