Context: Some benchmarks involve a few bit-operations, potentially introduced through the compiler or by manual optimization. This can include xors to negate booleans (i1 Variables in LLVM) or shifts to perform multiplication.
Problem: Mixing the theories of bit-vectors and integers may slow down the solver.
Solution: If possible, bit-operations should be converted to integer or boolean operations if possible.
xor on i1 variables -> boolean negation (already implemented)
left-shifts -> multiplication
bitwise or/and on i1 variables -> boolean or/and
Example: bresenham's algorithm uses multiplication by 2. The compiler tends to replace this by bit-shifts, causing mixing of theories.
Context: Some benchmarks involve a few bit-operations, potentially introduced through the compiler or by manual optimization. This can include xors to negate booleans (i1 Variables in LLVM) or shifts to perform multiplication.
Problem: Mixing the theories of bit-vectors and integers may slow down the solver.
Solution: If possible, bit-operations should be converted to integer or boolean operations if possible.
Example: bresenham's algorithm uses multiplication by 2. The compiler tends to replace this by bit-shifts, causing mixing of theories.