In case this helps: If you let the invariant vary (let’s call it i
) you get this:
pc ... true = i
vc ... true = (x < 2) => i => i[x+1/x]
So verifying the program for every input requires i(x)
to be true for all values of x
. The conjunction of pc
and vc
is:
total = i && ((x < 2) => i => i[x+1/x]) = (i && x >= 2)  (i && i[x+1/x])
Using some stolen notation:
V(p) = \{x \in \mathbb{Z}\mid p(x)\}
for a predicate p\colon \mathbb{Z} \to \text{bool}, we get:
V(total) = \{x\in \mathbb{Z}\mid x \ge 2 \wedge i(x)\} \cup \{x \in \mathbb{Z}\mid i(x) \wedge i(x+1)\}
Basically it looks like induction but the predicate i is “reverse”inductive, i.e. \forall x^\mathbb{Z}.i(x) \Rightarrow i(x  1). If instead you had that \forall x^\mathbb{Z}.i(x) \Rightarrow i(x + 1) one of the following holds:

V(i) = \emptyset, i.e i = \text{false}.

V(i) = \mathbb{Z}, i.e. i = \text{true}.

\emptyset \subset V(i) \subset \mathbb{Z}, by which I mean proper inclusions.
In the last case I claim that V(i) must have a least element.
Proof: Assume V(i) had no least element. Let x\in V(i), which exists since V(i)\neq \emptyset, and y\in\mathbb{Z}. If x\le y we get y\in V(i) by the inductive property of i. Otherwise we have y < x, but y can not be less than all elements of V(i) because otherwise V(i)\subseteq \mathbb{Z}_{>y}, i.e. V(i) would have a least element, a contradiction. (Note: subsets of wellordered sets with the induced order are wellordered again; \mathbb{N} \cong \mathbb{Z}_{>y} as posets via shifting)
Thus there is x_0\in V(i) s.t. x_0 <= y, but by the inductive property of i this yields x\in V(i). As x was arbitrary we get that V(i) = \mathbb{Z}, a contradiction. \square
This means that there is v\in V(i) s.t. V(i) = V(v \le x), and hence:
V(total) = \{x\in \mathbb{Z} \mid v \lor 2 \le x\} \cup \{x \in \mathbb{Z}\mid v \le x\} = V(v \le x)
For the original “reverse”inductive predicate i the negation \neg i must be inductive, hence V(\neg i) = V(v < x) for some v\in V(\neg i). Applying the rule V(\neg p) = V(p)^c gives that V(i) = V(x \le v). Then V(total) = V(2 \le x \le v) \cup V(x < v) which is either V(x < v) or V(x \le v).
I can’t fully judge what I came up with (too many things are static, like the assertion at the end, the loop body being empty except for the increment, etc.), but the intuition I get from it is that if you make your invariant inductive/“reverse”inductive you can either prove correctness for all inputs or the set of inputs where you can’t prove correctness is necessarily infinite.