Fix C2PO witness invariant generation

[sim642]

Inspired by #1710 (comment), I wondered what invariants C2PO analysis even generates. Turns out, none! Which is surprising, because it does implement the Invariant query.

I have no idea what's happening in the C2PO domain, but its pseudo-variable handling logic somehow even messes up normal program variables: Var.to_varinfo (NormalVar var) returns something different from var. And that variable is such that the temp-ness and in-scope checks cause everything to be filtered out.
I'm not sure why it does things the way it does and what should happen with non-NormalVar.

It then outputs some interesting invariants:

1. On line 19: z == x + -1 (which makes sense) and *x == *(z + 1) (which I guess is somehow derived from the former). The latter seems redundant.
2. On line 20: z != *x (where both x and z are of type long*). The comparison of long* and long is strange. But I'm also not sure if it's even true: z is just freshly allocated, so it's pointer value (cast to long) may equal an arbitrary integer.