Hi David,
Another small patch implementing ((A & ~B) ^ (~A & B)) -> A ^ B , similar to previous one, but with And condition.
Please review the patch.
Proof:
$ cat t.cvc
A, B : BITVECTOR(32);
QUERY BVXOR((A & ~B),(~A & B)) = BVXOR(A,B);
$ cvc3 t.cvc
Valid.
Thanks,
Mayur