(set-logic QF_SLIA) (set-info :status unsat) (declare-fun x () String) (assert (= (str.len x) 1)) (assert (or (< (str.to_code x) 0) (> (str.to_code x) 10000000000000000000000000000))) (check-sat)