% z3 2.smt2
sat
(((select square (_ bv0 32) ) #x02))
(((select square (_ bv1 32) ) #x00))
(((select square (_ bv2 32) ) #x00))
(((select square (_ bv3 32) ) #x00))