understanding output from ESBMC #4027

I recognize that this is a bit of recurring theme, but I'm still having difficulty understanding the output from ESBMC. Here's my sample program:

int main()
{
  unsigned int qa;
  int idx;

  if (qa % 2 == 0) ++qa;
  // qa = 1;
  
  __ESBMC_assert( qa % 2 == 1, "pre loop" );
  __ESBMC_loop_invariant( qa % 2 == 1 );
  for (idx = 0; idx < 10; ++idx)
  {
    __ESBMC_assert( qa % 2 == 1, "in loop" );
    qa += 2;
  }
  __ESBMC_assert( qa % 2 == 1, "post loop" );
 
  return 0;
}  

Here's an abbreviated version of the output:

Checking base case, k = 1
Solving claim 'in loop
✓ PASSED: 'in loop
Solving claim 'loop invariant inductive step
✓ PASSED: 'loop invariant inductive step
Solving claim 'in loop
✓ PASSED: 'in loop
Solving claim 'loop invariant base case
✓ PASSED: 'loop invariant base case
Solving claim 'pre loop
✓ PASSED: 'pre loop
Properties: 5 verified ✓ 5 passed
VERIFICATION SUCCESSFUL


Checking forward condition, k = 1
The forward condition is unable to prove the property

Checking base case, k = 2
Solving claim 'in loop
✓ PASSED: 'in loop
Solving claim 'in loop
✓ PASSED: 'in loop
Solving claim 'loop invariant inductive step
✓ PASSED: 'loop invariant inductive step
Solving claim 'in loop
✓ PASSED: 'in loop
Solving claim 'loop invariant base case
✓ PASSED: 'loop invariant base case
Solving claim 'pre loop
✓ PASSED: 'pre loop
Properties: 6 verified ✓ 6 passed
VERIFICATION SUCCESSFUL

Checking forward condition, k = 2
The forward condition is unable to prove the property

Checking inductive step, k = 2
VERIFICATION SUCCESSFUL

Solution found by the inductive step (k = 2)

First: the only situation in which I was able to see the verification result for "post loop" was when I modified the property to make it fail (e.g., qa % 2 == 0) and set a sufficiently large max-k-step that the for loop completed execution. I never saw a PASS result for "post loop".

Here is my understanding:

• With the invariant there are 5 properties
  1. "pre loop"
  2. "in loop"
  3. "post loop"
  4. base case of loop invariant
  5. inductive case of loop invariant
• The loop invariant may be proven in two ways:
  • base case + inductive step
  • base case + forward condition, which checks that all states are reachable in at most k steps

Observations:

• For each k, there are three "phases", which check the properties as follows:
  • Base
    • checks "pre loop "
    • checks base case of invariant
    • checks inductive case of invariant
    • checks "in loop" k + 1 times: k-times for the unrolling of the inductive step and 1 time for the base case
    • can't tell if it checked "post loop"
  • Forward condition: checks that all states are reachable in at most k steps
  • Inductive step (run if k >= 2 and forward condition is unable to verify the property)

I'm interpreting the output to mean that the "Base" phase goes from "Checking base case" to "VERIFICATION PASS/FAIL" just before checking the forward condition.

Questions:

1. Is my understanding of the phases and when each property is verified correct?
2. Why does the Base phase include the verification of the inductive case and "in loop"
3. Shouldn't the verification result for "post loop" be shown somewhere? (This might be related to request: output identity of assertion/invariant that ESBMC is unable to prove #4022.

-mark