STP doesn't allow one to use the "=" binary operator on booleans. Example input:
x : BOOLEAN;
ASSERT(x = TRUE);
and the output from STP:
syntax error: line 2
syntax error, unexpected '='
The prohibition on use of "=" for booleans is confusing and unexpected. It might be a bit more user-friendly to accept "=" on booleans.
The simplest workaround appears to be to replace "=" with "<=>". However "<=>" appears to have other problems. Another workaround is to use "NOT(x XOR y)" instead of "x = y", but this is not so readable. (There is no "NXOR".)
("&", "|", and "^" don't work either, but this seems less important.)