Files
clang-p2996/llvm/lib/Transforms/InstCombine
David Majnemer ab07f00c64 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
2014-08-11 22:32:02 +00:00
..
2014-07-22 04:57:06 +00:00
2014-07-07 22:13:58 +00:00
2014-04-28 04:05:08 +00:00