1 2 3 4 5
(set-logic ALL) (set-info :status unsat) (set-option :finite-model-find true) (assert (forall ((a String)) (forall ((b String)) (str.in_re a (re.++ re.allchar (str.to_re b)))))) (check-sat)