(assert (exists ((x RoundingMode)) (forall ((x3 RoundingMode)) (= x3 x))))
(set-info :status unsat)
(check-sat)