Skip to content
Commit ab07f00c authored by David Majnemer's avatar David Majnemer
Browse files

InstCombine: Combine (add (and %a, %b) (or %a, %b)) to (add %a, %b)

What follows bellow is a correctness proof of the transform using CVC3.

$ < t.cvc
A, B : BITVECTOR(32);

QUERY BVPLUS(32, A & B, A | B) = BVPLUS(32, A, B);

$ cvc3 < t.cvc
Valid.

llvm-svn: 215400
parent 155bbb77
Loading
Loading
Loading
Loading
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please to comment