How do I use a loop invariant to catch a bug in my program?

I’m learning about weakest preconditions, loop invariants, and verifying program correctness (e.g., with an SMT solver). From the slides here in slide 11, I see how placing a loop invariant can help me prove (or disprove) that my program meets its postcondition.

I created the following minimal program to test this idea. The program traverses an integer number line for 10 iterations, and I want to ensure it never goes below zero. I placed x >= 0 as my loop invariant and postcondition. However, I deliberately introduced a bug:

i = 0
x = user_input  # Assume we require x >= 0 initially.
while i < 10:
    if x >= 0:
        # Faulty edge-case: instead of protecting x, we subtract 1, which will make it negative.
        x = x - 1  
    else:
        # Normal behavior: increment x to stay safely above zero.
        x = x + 1
    i += 1
    # loop invariant: { x >= 0 }
# Postcondition: x >= 0

If x starts at 0, the predicate x >= 0 evaluates to true, so the program executes x = x - 1, making x negative. This clearly violates the intended invariant x >= 0.

My questions:

How exactly would the loop invariant x >= 0 be used to identify this bug in a formal verification or SMT-based approach? I understand that the invariant must hold at the start (and end) of each iteration, but I’m unsure how that translates into a proof or a verification condition that flags the code as incorrect.

Meta Question I know we often derive a precondition using backward reasoning to ensure the loop invariant holds initially, but I’m not fully clear on how to formally derive it (e.g., x >= 0 initially) with the loop invariant and the postcondition. I suppose that would be needed to answer my main question.

I hope my question is clear. I’d appreciate any pointers on how to show, via loop invariants (and possibly weakest precondition reasoning and a SMT), that this program is not correct—specifically, that the code fails the invariant if x starts at 0.

You need to be able to prove that {x >= 0} x = x-1 {x >= 0} is true, which you can't (x starting as 0 is the counterexample).

I'm not clear what your meta-question is.