fix error message
stub out parsing of basic blocks
initial support for basic blocks
bugfix printing of icmp instructions
Assume open-world for BBs, i.e., that BBs may have other instructions other than the ones shown
In practice this means we need to enforce that preconditions of BBs must match
exactly on both sides.  This may be overly restrictive and may require further
language support to weaken this strictness.
improve handling of undef behavior in store instructions
After executing undef behavior, a store may or may not happen. Thus, reflect
this possiblity in the SMT encoding using quantified boolean vars
Allow isPower2 predicate to work with any operand type.
It should use isKnownToBeAPowerOfTwo() of LLVM when the operand is not a constant.
add new predicates: WillNotOverflowSignedMul and WillNotOverflowUnsignedMul
add new constant function: log2
Ignore types of preconditions
One valid type is sufficient; there's no need to iterate over all possible types.
This gives a huge speedup for the tests/skip/addnswnuw.opt test.
add some patterns from InstCombineMulDivRem.cpp
enable the % constant operator for srem
Use poisonness flown into operands to trigger undef behavior
Testcase will follow
introduce /u and %u operators (unsigned cousins)
add a few more instcombine tests
Add test cases for recent bug reports
typo
Show signed and unsigned representations in counterexamples.
add regression test for LLVM's PR21255
add regression test for LLVM's PR21256
Bias bitwidth of integers towards 4 and 8 bits first
This makes counterexamples easier to read, and has a small performance impact.
No change in correctness criteria.
Patch by David Menendez.
Add 2 new predicates: isPowerOf2OrZero and WillNotOverflowUnsignedShl.
Finish instcombine/muldivrem.opt