Adding a set of tests on reader of proof obligation.
The tests found some problems to solve.