| Obligations | Alt-Ergo 2.3.0 | Z3 4.4.1 | Z3 4.8.6 |
| VC for inverse_in_place | --- | --- | --- |
| split_goal_right | | | |
| loop invariant init | 0.01 | --- | --- |
| index in array bounds | 0.00 | --- | --- |
| index in array bounds | --- | 0.10 | --- |
| index in array bounds | 0.00 | --- | --- |
| loop invariant init | --- | --- | 0.03 |
| loop invariant init | 0.12 | --- | --- |
| loop invariant init | 0.23 | --- | --- |
| index in array bounds | 0.01 | --- | --- |
| index in array bounds | --- | --- | 0.03 |
| loop variant decrease | --- | --- | 0.18 |
| loop invariant preservation | 0.01 | --- | --- |
| loop invariant preservation | --- | --- | 0.20 |
| loop invariant preservation | --- | --- | 0.25 |
| assertion | 0.01 | --- | --- |
| assertion | 0.01 | --- | --- |
| index in array bounds | --- | 0.07 | --- |
| loop invariant preservation | --- | --- | 0.19 |
| assertion | 0.00 | --- | --- |
| index in array bounds | 0.08 | --- | --- |
| loop invariant preservation | 0.18 | --- | --- |
| postcondition | 0.01 | --- | --- |
| postcondition | 0.03 | --- | --- |
| out of loop bounds | 0.04 | --- | --- |