• Integers cannot be handled my MONA. Handling by Z3 or CVC3 does not prove the formula. Solution: use the fact that integers have a finite width and encode them as booleans.
• Local booleans produce a state explosion in MONA due to handling them as predicates. Solution: make them static, which results in better heuristics.
• Reason of MONA failure is not printed: it was not known whether MONA failed due to a real counterexample or whether it ran out of space. Solution: improve error reporting.
• Output from debugging causes string overflow. Repaired by reducing the output size.
• Input for MONA is too large. Solution: a shorter definition of null (thanks to Thomas Wies).
• Input for MONA is still too large. Solution: change the algorithm by using booleans and non-ghost left and right instead of pointers and ghost left and right.
• Precision is lost on a join from "then" and "else" branches of a conditional statement. Solution: make an invariant optically stronger.
• Input for MONA is still too large. Solution: reducing the number of bits per program counter.
• Input for MONA is still too large. Solution: use distributivity to mention the subformula (n1:Tree & n2:Tree & n3:Tree) only once.
• Input for MONA is still too large. Solution: some verification conditions can be handled with Z3!
• Input for MONA is still too large. Solution: apply the distributivity in the antecedent of a sequent to be proven, adding option -tryHard.
• Finally, 3 threads with 4 bits per program counter and arbitrary initial distribution of threads over the leaves can be verified in approximately 3 hours, even without the help of Z3.