Proof that an equality (that would be useful if true) does not hold

smt2

;;
;; Prove that
;; (x -y) >> 3 != ((x >> 3)  - (y >> 3))
;;
;; if x >= y
;;
;;
(declare-fun x () (_ BitVec 32))
(declare-fun y () (_ BitVec 32))
(declare-fun shift () (_ BitVec 32))
(assert
  (=
    shift
    (_ bv3 32)
  )
)
(assert (bvuge x y))
(assert
  (not
    (=
      (bvlshr
        (bvsub x y)
        shift
      )
      (bvsub
        (bvlshr x shift)
        (bvlshr y shift)
      )
    )
  )
)
;; Z3 responds SAT
;; meaning that there is a counter example
;; to our proposed equality.
(check-sat)
(get-model)
(exit)

;;
;; Prove that
;; (x -y) >> shift == ((x >> shift)  - (y >> shift))
;;
;; if x >= y and y is a multiple of (1 << shift).
;;
;; By adding the additional constraint on `y` it makes
;; the equality hold.
;;
(declare-fun x () (_ BitVec 32))
(declare-fun y () (_ BitVec 32))
(declare-fun shift () (_ BitVec 32))
(assert
  (=
    shift
    (_ bv3 32)
  )
)
(assert
  (=
    (_ bv0 32)
    (bvurem
      y
      (bvshl
        (_ bv1 32)
        shift
      )
    )
  )
)
(assert (bvuge x y))
(assert
  (not
    (=
      (bvlshr
        (bvsub x y)
        shift
      )
      (bvsub
        (bvlshr x shift)
        (bvlshr y shift)
      )
    )
  )
)
;; Z3 responds UNSAT
;; meaning that there isn't a counter example
;; to our proposed equality.
(check-sat)

Example output

sat
(model 
  (define-fun y () (_ BitVec 32)
    #x10200c44)
  (define-fun x () (_ BitVec 32)
    #x80901840)
  (define-fun shift () (_ BitVec 32)
    #x00000003)
)