Possible bug in Python Prelude: inconsistent use of days and hours

[joscoh]

BoogiePrelude.lean includes the following:

procedure timedelta(days: IntOrNone, hours: IntOrNone) returns (delta : int, maybe_except: ExceptOrNone)
spec{
}
{
  havoc delta;
  var days_i : int := 0;
  if (IntOrNone_tag(days) == IN_INT_TAG) {
        days_i := IntOrNone_int_val(days);
  }
  var hours_i : int := 0;
  if (IntOrNone_tag(hours) == IN_INT_TAG) {
        days_i := IntOrNone_int_val(hours);
  }
  assume [assume_timedelta_sign_matches]: (delta == (((days_i * 24) + hours_i) * 3600) * 1000000);
};

Should the line days_i := IntOrNone_int_val(hours); actually be hours_i := IntOrNone_int_val(hours);?

[aqjune-aws]

Yeah, I think so. :/ I will make a patch soon.

[aqjune-aws]

Created a patch - #302