Fix issue #297 and #268, make proc inlining visit subblocks

[aqjune-aws]

This patch fixes

• Issue Possible bug in Python Prelude: inconsistent use of days and hours #297: BoogiePrelude.lean's timedelta was not updating hours_i
• Issue Soundness issue: fresh RHS identifiers in procedure inlining #268: procedure inlining was reducing nondeterminism because it was missing havocs to output vars
  • In fact, this depends on how the "correctness" of procedure inlining is defined; if we say that procedure inlining is allowed to reduce nondeterminism, the original implementation was correct of course, but since this makes procedure inlining inherently unsound to use for deductive verification I chose to fix it. This is all under the assumption that the spec of the inlining procedure exactly represents the actual behavior of the contents of the procedure.
• Procedure inlining wasn't visiting subblocks, which was fixed here. This required small updates in the function signature of inlineCallCmd and callElimCmd so that they receive Command rather than Statement.

For these changes, checks are needed to confirm whether Python applications of interest are not affected.

Issue #, if available:

Description of changes:

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[aqjune-aws]

I will revisit the failing Python cases in this afternoon.

[shigoel]

I will revisit the failing Python cases in this afternoon.

@aqjune-aws Maybe also see if #301 can help, if you have the bandwidth?

[aqjune-aws]

The reason of the failure was that this extra main() invocation could now be inlined, multiplying the number of invoked assertions (and hence making it diverged from the .expected file):

(procedure __main__ :  () → ((maybe_except : ExceptOrNone)))
modifies: []
preconditions: 
postconditions: 
body: init (exception_ty_matches : bool) := #false
havoc exception_ty_matches
import$inlined : {init (import_names_32 : ListStr) := (((~ListStr_cons : (arrow string (arrow ListStr ListStr))) #test_helper) (~ListStr_nil : ListStr))}
if (__name__ == #__main__) then {call [maybe_except] := main([])
 if ((~ExceptOrNone_tag maybe_except) == ~EN_STR_TAG) then {goto end} else{}}
else{}
end : {}

I will add a parameter to the procedure inlining call so that functions to be excluded from inlining like main can be designated