(set-logic QF_S)
(declare-fun var0 () String)
(assert (= var0 (Concat "*zCEs" "")))
(assert (= var0 (Concat "`Q\\M-" "")))
(check-sat)