1 2 3 4 5 6 7 8 9 10 11 12
(set-logic QF_S) (set-info :status sat) (declare-const x String) (assert (= (str.len x) 1)) ;(assert (= x "X")) (assert (or (not (> (str.len x) 1)) (= (str.at x 1) "Z") ) ) (check-sat)