Always flush on printout()

Some flushing was done during proof checking, but it might as well
be unconditional on printout() messages.

Tweaks of the coverage formatting.

Use reverse induction less often.

Candidate reverse induction proofs can be generated in many problems.
To save time, use them only in cases where the resulting hypothesis
overturns a loop unroll or induction failure judgement.

bugfix: use same large values.

The discrepancy between 2^32 - 3 and 2^32 - 10 can matter. Not very
much, but enough to create unusual failures.

Integrate future induction.

The required checks and search process were added recently.
The ProofNode proof script type now has a SingleRevInduct
proof kind, which captures the reverse-induction at a single
loop point, and the search process emits the relevant proof
scripts.

This required a minor restructure of the searcher.

Check reverse single induction, use in search.

The check module now knows how to check a proof of loop equalities
by induction. The loop_bounds module already had this, but now it
is more official. It can also check a predicate by *reverse*
induction. The idea here is to name some predicate, show that it
would be true if some iteration bound is reached (i.e. typically
a very large number), and then show by induction back down that the
predicate was also true in the initial iterations.

This is useful in a special case involving a loop of the form
for (i = 0; i < n; i ++) { } with no function calls. Suppose the
body contains an array index p[i], which implies the array fits in
memory, i * sizeof(*p) < 2 ^ 32. Since the final iteration
i = n - 1 must be reached, the compiler can deduce
that n <= 2 ^ 32 / sizeof(*p), a fact we will prove by reverse
induction.

The search module now contains code to detect cases like this and
discover the best bound we can impose by simple binary search.

Some stats for split discovery.

Hopefully I'll get a useful graph out of these yet ... depends on
-O2 coming through.

Tweak check code to print report without checking.

Useful in making sense of bigger proof objects.

Report more on failures, in particular timeouts.

Some more inner loop handling sanity.

This gets us past the 'check' phase of problem setup for functions
with inner loops.

Move consider_inline process to check.

It's still not really where it belongs. Really the target should specify
what the inlining process should be, but that breaks backward compatibility
a bit too much for me right now.

Adjust approach to splittables.

Generate splittable information lazily and store in cached_analysis
of problem. Also check for complex loops at a slightly different
point.

Also replace an experimental better split point detector in logic
with another experimental one which also doesn't work perfectly yet.

Experimental: ignore unmatched ASM functions.

This may allow an (unreliable) WCET estimate of some code which
we haven't properly made sense of yet.

Tweak handling of reachability.

Move reachability cache to problem (from rep_graph), use in check
to insist on discovering (0) loop bounds slightly less often.

Bugfix.

Respect 'do_analysis = False' in inline_at_point.

Bugfix: ensure skip_underspec is passed in prev.

When replacing trace_refute's implementation with check.build_problem, I failed
to note that trace_refute passes a special skip_underspec argument. Fixed.

Adjust for API change in check_hyp_group.

Somewhere in the parallelisation change, the change of return type
of this function didn't get propagated.

Better parallel implementation of hyp testing.

WIP: test_hyp_imps via parallel strategies.

Defer some analysis during inline phase.

The WCET analysis is keeping us waiting on this a lot.

Port inline workaround from WCET branch.

This leads to less Aborts and more results. It's a bit of a hack
though, but then so was the hardcoded 'C' tag.

More bugfixing and diagnostics for loop_bounds.

Yet more of the above.

Pass explicit tags further to fix more bugs.

Report-mode checking returns success.

Results of checks were getting dropped, leading to a nonsense final summary.

Import of graph-refine tool.