(set-option :incremental false)
(set-logic QF_BV)
(assert (= (bvashr (_ bv0 3) (_ bv0 3)) (_ bv0 3)))
(assert (= (bvashr (_ bv0 3) (_ bv1 3)) (_ bv0 3)))
(assert (= (bvashr (_ bv0 3) (_ bv2 3)) (_ bv0 3)))
(assert (= (bvashr (_ bv0 3) (_ bv3 3)) (_ bv0 3)))
(assert (= (bvashr (_ bv0 3) (_ bv4 3)) (_ bv0 3)))
(assert (= (bvashr (_ bv0 3) (_ bv5 3)) (_ bv0 3)))
(assert (= (bvashr (_ bv0 3) (_ bv6 3)) (_ bv0 3)))
(assert (= (bvashr (_ bv0 3) (_ bv7 3)) (_ bv0 3)))
(assert (= (bvashr (_ bv1 3) (_ bv0 3)) (_ bv1 3)))
(assert (= (bvashr (_ bv1 3) (_ bv1 3)) (_ bv0 3)))
(assert (= (bvashr (_ bv1 3) (_ bv2 3)) (_ bv0 3)))
(assert (= (bvashr (_ bv1 3) (_ bv3 3)) (_ bv0 3)))
(assert (= (bvashr (_ bv1 3) (_ bv4 3)) (_ bv0 3)))
(assert (= (bvashr (_ bv1 3) (_ bv5 3)) (_ bv0 3)))
(assert (= (bvashr (_ bv1 3) (_ bv6 3)) (_ bv0 3)))
(assert (= (bvashr (_ bv1 3) (_ bv7 3)) (_ bv0 3)))
(assert (= (bvashr (_ bv2 3) (_ bv0 3)) (_ bv2 3)))
(assert (= (bvashr (_ bv2 3) (_ bv1 3)) (_ bv1 3)))
(assert (= (bvashr (_ bv2 3) (_ bv2 3)) (_ bv0 3)))
(assert (= (bvashr (_ bv2 3) (_ bv3 3)) (_ bv0 3)))
(assert (= (bvashr (_ bv2 3) (_ bv4 3)) (_ bv0 3)))
(assert (= (bvashr (_ bv2 3) (_ bv5 3)) (_ bv0 3)))
(assert (= (bvashr (_ bv2 3) (_ bv6 3)) (_ bv0 3)))
(assert (= (bvashr (_ bv2 3) (_ bv7 3)) (_ bv0 3)))
(assert (= (bvashr (_ bv3 3) (_ bv0 3)) (_ bv3 3)))
(assert (= (bvashr (_ bv3 3) (_ bv1 3)) (_ bv1 3)))
(assert (= (bvashr (_ bv3 3) (_ bv2 3)) (_ bv0 3)))
(assert (= (bvashr (_ bv3 3) (_ bv3 3)) (_ bv0 3)))
(assert (= (bvashr (_ bv3 3) (_ bv4 3)) (_ bv0 3)))
(assert (= (bvashr (_ bv3 3) (_ bv5 3)) (_ bv0 3)))
(assert (= (bvashr (_ bv3 3) (_ bv6 3)) (_ bv0 3)))
(assert (= (bvashr (_ bv3 3) (_ bv7 3)) (_ bv0 3)))
(assert (= (bvashr (_ bv4 3) (_ bv0 3)) (_ bv4 3)))
(assert (= (bvashr (_ bv4 3) (_ bv1 3)) (_ bv6 3)))
(assert (= (bvashr (_ bv4 3) (_ bv2 3)) (_ bv7 3)))
(assert (= (bvashr (_ bv4 3) (_ bv3 3)) (_ bv7 3)))
(assert (= (bvashr (_ bv4 3) (_ bv4 3)) (_ bv7 3)))
(assert (= (bvashr (_ bv4 3) (_ bv5 3)) (_ bv7 3)))
(assert (= (bvashr (_ bv4 3) (_ bv6 3)) (_ bv7 3)))
(assert (= (bvashr (_ bv4 3) (_ bv7 3)) (_ bv7 3)))
(assert (= (bvashr (_ bv5 3) (_ bv0 3)) (_ bv5 3)))
(assert (= (bvashr (_ bv5 3) (_ bv1 3)) (_ bv6 3)))
(assert (= (bvashr (_ bv5 3) (_ bv2 3)) (_ bv7 3)))
(assert (= (bvashr (_ bv5 3) (_ bv3 3)) (_ bv7 3)))
(assert (= (bvashr (_ bv5 3) (_ bv4 3)) (_ bv7 3)))
(assert (= (bvashr (_ bv5 3) (_ bv5 3)) (_ bv7 3)))
(assert (= (bvashr (_ bv5 3) (_ bv6 3)) (_ bv7 3)))
(assert (= (bvashr (_ bv5 3) (_ bv7 3)) (_ bv7 3)))
(assert (= (bvashr (_ bv6 3) (_ bv0 3)) (_ bv6 3)))
(assert (= (bvashr (_ bv6 3) (_ bv1 3)) (_ bv7 3)))
(assert (= (bvashr (_ bv6 3) (_ bv2 3)) (_ bv7 3)))
(assert (= (bvashr (_ bv6 3) (_ bv3 3)) (_ bv7 3)))
(assert (= (bvashr (_ bv6 3) (_ bv4 3)) (_ bv7 3)))
(assert (= (bvashr (_ bv6 3) (_ bv5 3)) (_ bv7 3)))
(assert (= (bvashr (_ bv6 3) (_ bv6 3)) (_ bv7 3)))
(assert (= (bvashr (_ bv6 3) (_ bv7 3)) (_ bv7 3)))
(assert (= (bvashr (_ bv7 3) (_ bv0 3)) (_ bv7 3)))
(assert (= (bvashr (_ bv7 3) (_ bv1 3)) (_ bv7 3)))
(assert (= (bvashr (_ bv7 3) (_ bv2 3)) (_ bv7 3)))
(assert (= (bvashr (_ bv7 3) (_ bv3 3)) (_ bv7 3)))
(assert (= (bvashr (_ bv7 3) (_ bv4 3)) (_ bv7 3)))
(assert (= (bvashr (_ bv7 3) (_ bv5 3)) (_ bv7 3)))
(assert (= (bvashr (_ bv7 3) (_ bv6 3)) (_ bv7 3)))
(assert (= (bvashr (_ bv7 3) (_ bv7 3)) (_ bv7 3)))
(check-sat)