<reponame>muchang/z3test<gh_stars>10-100

# Copyright (c) 2015 Microsoft Corporation
from z3 import *
set_option(auto_config=True)

# Create to bit-vectors of size 32
x, y = BitVecs('x y', 32)

solve(x >> 2 == 3)

solve(x << 2 == 3)

solve(x << 2 == 24)
