• The initialization of the real code is faulty: the last flags are not initialized with false. Solution: k<LogP is substituted by k≤logP.
• Initialization routine is too complicated: it works only if num_nodes=P. Solution: substituted num_nodes by P and log_num_nodes by LogP.
• Functions are first-order objects (i.e., it is possible to quantify over them) for Jahob, which operates with high-order logic, but not for SMT solvers. Current SMT solvers allow only arrays as first-order objects. However, no translation of functions to arrays takes place in Jahob. Moreover, Jahob uses the old SMTLIB 1.2 output format; rewriting output to the current SMTLIB 2.0 needs about 10K code: out if scope of the current project. Solution: try out other verifiers.
• In Boogie, extensionality of Z3 v.15 is not used, but needed. Solution: write an axiom which encodes extensionality.
• Induction, or, equivalently, existence of a minimal natural number satisfying a property, is not supported. Solution: use am axiom that states such an existence.
• The procedures in Boogie file are verified separately very fast; the file as a whole is verified very slowly, running out of space on few procedures. Solution: keep the number of procedures small.
• Boogie+Z3 still can't prove all the procedures. Solution: Remove the subformulas 0≤i and i≤L whenever possible;
• Boogie+Z3 still can't prove all the procedures. Solution: Reduce the number of procedures by inlining procedures which serve as lemmas and are used in an unquantified form;
• Boogie+Z3 still can't prove all the procedures. Solution: Simplify internals of lemmas, reducing the number of variables in pre- and postconditions.
• Boogie+Z3 still can't prove all the procedures. Solution: Let Boogie split verification conditions whenever possible.
• Boogie+Z3 still can't prove all the procedures. Solution: Represent each transition by its own procedure to reduce the size of the scheduler loop.
• Boogie+Z3 still can't prove all the procedures. Solution: Transitions which are described by procedures which are late in the code get easier-to-prove postconditions (ensures-clauses).
• Smoke test done to show absence of dead code. Total verification time: 3458.58 s.