We say that the cancellation property holds for a ring $R$ if for finitely generated projective $R$-modules $P$ and $Q$ we have that $R \oplus P \cong R \oplus Q$ implies $P \cong Q$.
In the case that $G$ is a finite group and $R=\mathbb{Z}[G]$, this property is discussed at length in Richard Swan's paper Projective modules over binary polyhedral groups J. Reine Angew. Math. 342 (1983), 66–172, MR0703486.
For example, it is shown that the cancellation property fails when $G=Q_8 \times C_2$ or $Q_{32}$, where $Q_{4n}$ is the generalised quaternion group of order $4n$ and $C_n$ is the cyclic group of order $n$.
Is it known whether the cancellation property holds for $R=\mathbb{Z}[G]$ when $G$ is the semidirect product $C_4 \rtimes C_4$ with quotient isomorphic to $Q_8$? To be clear, I mean this group: https://people.maths.bris.ac.uk/~matyd/GroupNames/1/C4sC4.html
It would appear Swan's paper doesn't cover this case. I'd also be interested in whether it is known if $R=\mathbb{Z}[G]$ has the property that every finitely generated stably free module is in fact free (this is of course implied by the cancellation property described above).
The reason I'm asking is that Tommy Hofmann and I have come up with an example using computational methods to show that cancellation fails in this case. But we are wondering whether this result is already known and / or whether there is some nice theoretical explanation.
