[511] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2 
Failed to validate 60 741: (= (o (a #186)) (o (a #668))) false
(sat
...
[512] % cat small.smt2 
(declare-datatypes ((a 0)) (((a (o (Array (_ BitVec 2) (_ BitVec 2)))))))
(declare-fun r ((_ BitVec 2) a (_ BitVec 2)) Bool)
(assert (forall ((a a) (s (_ BitVec 2))) (= (bvsge s (_ bv0 2)) (r s a (_ bv0 2)))))
(check-sat)