Yes, you are right. I wasn't thinking clearly
> ------- Comment #4 from bonzini at gnu dot org 2007-08-23 14:04 ------- > Hmmm, a store into an "int *" could not touch nodekind itself, only a store > into an "int **" could. > > Isn't SMT.8 the VDEF saying it could touch *the thing pointed to by nodekind*? >