{
Rnk * r;
assert (VAR2LIT (v) != UNDEF);
assert (VAR2LIT (v)->val != UNDEF);
assert (!v->level);
ps->fixed++;