When simplifying NOT-AND-OR, RexSimplify incorrectly applies predicates deduced for operands to the same operands.
Here is the test case (add it to RexProgramTest):
When you run it, verify will find a combination of assignments such that the simplified expression returns a different result than the original.
The test case is not minimal; sorry. Maybe it reproduces with NOT-OR.
The bug is in RexSimplify.simplifyAndTerms. Put a breakpoint at that line to see the problem. It passes through the operands once, building a list of predicates. Then it passes through the operands again, simplifying each operand. Thus operand1 is simplified using a list of predicates that includes the predicate 'not operand1'. Clearly wrong. Zoltan Haindrich, I warned that this was possible in our discussions.