You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
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.
The text was updated successfully, but these errors were encountered: