You can run such examples through a SAT solver to check the satisfiability of equations or formulas like you just specified.
I didn't find any X or Y which satisfied your constraints (i.e, does there exist any X or Y which produce an inequality in this equation)
(declare-const x (_ BitVec 32))
(declare-const y (_ BitVec 32))
(assert (not (= (bvsub (bvadd (bvshl (bvadd x y) #x00000004) y) x)
(bvadd (bvmul #x00000011 y) (bvmul #x0000000f x)))))
(check-sat)
(get-model)
In regards to overflow, logics over bitvectors generally provide no distinction between signed and unsigned bit-vectors as numbers. Instead, the theory of bit-vectors provides special signed versions of arithmetical operations where it makes a difference whether the bit-vector is treated as signed or unsigned. I have used the appropriate operator to the equation you've specified. Of course, you could just the results algebraically to (x+y)<<4 == 16y + 16x
but a SMT solver handles cases like overflow which are difficult to formalize).
It doesn't matter what your instruction word size, there is no X
or Y
that can produce an inequality.