Proving that a property is k-inductive with an SMT solver (parametric resettable counter) I'm following the slides at https://homepage.cs.uiowa.edu/~tinelli/talks/FT-11.pdf where Tinelli explains how k-induction works in the context of SMT based model checking.

A parametric and resettable counter is given as a Kripke structure by the following formulas:

Variables:


$x := (c, n, r, n_0)$, where:


$n_0$ is a positive integer (input)
$r$ is a boolean (input)
$c$, $n$ are integers (internal variables)



Initialization:


$I[x] := (c = 1) \wedge (n = n_0)$


Transitions:


$\begin{align*}
 T[x,x'] := (n' = n) &amp; \wedge (&amp; (r' \vee (c=n)) &amp; \to (c' = 1)) \\
                     &amp; \wedge (&amp; \neg(r' \vee (c=n)) &amp; \to (c' = c + 1)) \\
\end{align*}$


Property to prove invariant:


$P[x] := c \le n + 1$


Tinelli uses the following notation: 

$I^i:=I[x^{(i)}],P^i:=P[x^{(i)}],T^i:=T[x^{(i−1)},x^{(i)}]$.

He then claims on page 52/90 that the formula $P := c \le n+1$ is an invariant of this system because $P$ is 1-inductive (while incidentally not being 0-inductive). If I'm following correctly, this means that $I^0 \models P^0$ and $I^0 \wedge T^1 \models P^1$ (base case) and $P^0 \wedge P^1 \wedge T^1 \wedge T^2 \models P^2$ (inductive step). In particular it means that the formula $P^0 \wedge P^1 \wedge T^1 \wedge T^2 \wedge \neg (P^2)$ is UNSAT. However, after playing a little with Z3Py I was able to find the following model for this formula and a corresponding representation of a state transition trace with $(c,n,r)$:


$c^0 = -1, n^0 = 0, c^1 = 1, n^1 = 0, r^1 = \text{True},c^2 = 2, n^2 = 0, r^2 = \text{False}$
$(-1, 0, *) \to (1, 0, \text{True}) \to (2, 0, \text{False})$


Intuitively this makes sense. The constraint on $n_0$ being a positive integer affects the base case formula $I^0$ but not the inductive step, and therefore the above model is a valid model of the induction formula for $i=1$ which means the implication fails.

Of course $P$ is an invariant of this system, but it would seem to me that we cannot show it with k-induction for k = 1.

What is the gap in my understanding of this material?
I don't see any gap in your understanding.  What you wrote looks correct to me.

Perhaps the author meant to use the property $P := c \le n+1 \land n \ge 1$.  I think with that modification, $P$ becomes 1-inductive but not 0-inductive.  I suspect the author was looking for a simple example of a property that is 1-inductive but not 0-inductive, and missed a small detail.

Good job catching this!