(set-logic QF_BV)
(assert (= ((_ rotate_left 0) (_ bv3 4)) (_ bv3 4)))
(assert (= ((_ rotate_left 1) (_ bv3 4)) (_ bv6 4)))
(assert (= ((_ rotate_left 2) (_ bv3 4)) (_ bv12 4)))
(assert (= ((_ rotate_left 3) (_ bv3 4)) (_ bv9 4)))
(assert (= ((_ rotate_left 4) (_ bv3 4)) (_ bv3 4)))
(assert (= ((_ rotate_left 5) (_ bv3 4)) (_ bv6 4)))
(assert (= ((_ rotate_left 6) (_ bv3 4)) (_ bv12 4)))
(assert (= ((_ rotate_left 7) (_ bv3 4)) (_ bv9 4)))
(assert (= ((_ rotate_right 0) (_ bv3 4)) (_ bv3 4)))
(assert (= ((_ rotate_right 1) (_ bv3 4)) (_ bv9 4)))
(assert (= ((_ rotate_right 2) (_ bv3 4)) (_ bv12 4)))
(assert (= ((_ rotate_right 3) (_ bv3 4)) (_ bv6 4)))
(assert (= ((_ rotate_right 4) (_ bv3 4)) (_ bv3 4)))
(assert (= ((_ rotate_right 5) (_ bv3 4)) (_ bv9 4)))
(assert (= ((_ rotate_right 6) (_ bv3 4)) (_ bv12 4)))
(assert (= ((_ rotate_right 7) (_ bv3 4)) (_ bv6 4)))
(check-sat)