(set-logic QF_BV)
(set-info :status sat)
(assert (= (bvshl (_ bv0 3) (_ bv0 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv0 3) (_ bv1 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv0 3) (_ bv2 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv0 3) (_ bv3 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv0 3) (_ bv4 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv0 3) (_ bv5 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv0 3) (_ bv6 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv0 3) (_ bv7 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv1 3) (_ bv0 3)) (_ bv1 3)))
(assert (= (bvshl (_ bv1 3) (_ bv1 3)) (_ bv2 3)))
(assert (= (bvshl (_ bv1 3) (_ bv2 3)) (_ bv4 3)))
(assert (= (bvshl (_ bv1 3) (_ bv3 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv1 3) (_ bv4 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv1 3) (_ bv5 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv1 3) (_ bv6 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv1 3) (_ bv7 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv2 3) (_ bv0 3)) (_ bv2 3)))
(assert (= (bvshl (_ bv2 3) (_ bv1 3)) (_ bv4 3)))
(assert (= (bvshl (_ bv2 3) (_ bv2 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv2 3) (_ bv3 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv2 3) (_ bv4 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv2 3) (_ bv5 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv2 3) (_ bv6 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv2 3) (_ bv7 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv3 3) (_ bv0 3)) (_ bv3 3)))
(assert (= (bvshl (_ bv3 3) (_ bv1 3)) (_ bv6 3)))
(assert (= (bvshl (_ bv3 3) (_ bv2 3)) (_ bv4 3)))
(assert (= (bvshl (_ bv3 3) (_ bv3 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv3 3) (_ bv4 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv3 3) (_ bv5 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv3 3) (_ bv6 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv3 3) (_ bv7 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv4 3) (_ bv0 3)) (_ bv4 3)))
(assert (= (bvshl (_ bv4 3) (_ bv1 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv4 3) (_ bv2 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv4 3) (_ bv3 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv4 3) (_ bv4 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv4 3) (_ bv5 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv4 3) (_ bv6 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv4 3) (_ bv7 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv5 3) (_ bv0 3)) (_ bv5 3)))
(assert (= (bvshl (_ bv5 3) (_ bv1 3)) (_ bv2 3)))
(assert (= (bvshl (_ bv5 3) (_ bv2 3)) (_ bv4 3)))
(assert (= (bvshl (_ bv5 3) (_ bv3 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv5 3) (_ bv4 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv5 3) (_ bv5 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv5 3) (_ bv6 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv5 3) (_ bv7 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv6 3) (_ bv0 3)) (_ bv6 3)))
(assert (= (bvshl (_ bv6 3) (_ bv1 3)) (_ bv4 3)))
(assert (= (bvshl (_ bv6 3) (_ bv2 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv6 3) (_ bv3 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv6 3) (_ bv4 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv6 3) (_ bv5 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv6 3) (_ bv6 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv6 3) (_ bv7 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv7 3) (_ bv0 3)) (_ bv7 3)))
(assert (= (bvshl (_ bv7 3) (_ bv1 3)) (_ bv6 3)))
(assert (= (bvshl (_ bv7 3) (_ bv2 3)) (_ bv4 3)))
(assert (= (bvshl (_ bv7 3) (_ bv3 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv7 3) (_ bv4 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv7 3) (_ bv5 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv7 3) (_ bv6 3)) (_ bv0 3)))
(assert (= (bvshl (_ bv7 3) (_ bv7 3)) (_ bv0 3)))
(check-sat)