SQLite

The new LEFT JOIN strength reduction optimization is sometimes applied in cases where it should not be, resulting in an error. The following query demonstrates:

CREATE TABLE t1(a INTEGER PRIMARY KEY, b);
CREATE TABLE t2(x INTEGER PRIMARY KEY, y);
INSERT INTO t1(a,b) VALUES(1,null);

SELECT a FROM t1 LEFT JOIN t2 ON (b=x) 
 WHERE NOT ( b IS NOT NULL AND y='xyz' );

The problem was caused by the NOT operator, which the prover did not recognize as inverting the logic of its operand, effectively converting the AND into an OR.

The problem was discovered by Raphael Michel and reported on the sqlite-users mailing list.