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