Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- ;;
- ;; 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)
Add Comment
Please, Sign In to add comment