Fixed: too few split names were considered.
Consider the formula P == T for a standard name T and a constant P. It's obviously not valid. Yet for split level >= 1 the solver said it's valid, because it when splitting P it only considered the case P == T.
Loading