(set-logic QF_BV)
(set-info :status sat)
(assert (= (bvashr (_ bv0 2) (_ bv0 2)) (_ bv0 2)))
(assert (= (bvashr (_ bv0 2) (_ bv1 2)) (_ bv0 2)))
(assert (= (bvashr (_ bv0 2) (_ bv2 2)) (_ bv0 2)))
(assert (= (bvashr (_ bv0 2) (_ bv3 2)) (_ bv0 2)))
(assert (= (bvashr (_ bv1 2) (_ bv0 2)) (_ bv1 2)))
(assert (= (bvashr (_ bv1 2) (_ bv1 2)) (_ bv0 2)))
(assert (= (bvashr (_ bv1 2) (_ bv2 2)) (_ bv0 2)))
(assert (= (bvashr (_ bv1 2) (_ bv3 2)) (_ bv0 2)))
(assert (= (bvashr (_ bv2 2) (_ bv0 2)) (_ bv2 2)))
(assert (= (bvashr (_ bv2 2) (_ bv1 2)) (_ bv3 2)))
(assert (= (bvashr (_ bv2 2) (_ bv2 2)) (_ bv3 2)))
(assert (= (bvashr (_ bv2 2) (_ bv3 2)) (_ bv3 2)))
(assert (= (bvashr (_ bv3 2) (_ bv0 2)) (_ bv3 2)))
(assert (= (bvashr (_ bv3 2) (_ bv1 2)) (_ bv3 2)))
(assert (= (bvashr (_ bv3 2) (_ bv2 2)) (_ bv3 2)))
(assert (= (bvashr (_ bv3 2) (_ bv3 2)) (_ bv3 2)))
(check-sat)