blob: c0c1f16f71287e0ef91d670f18d5c8054e8377af (
plain)
1
2
3
4
5
|
(set-logic ALL)
(set-info :status unsat)
(declare-fun x () String)
(assert (let ((_let_1 (str.to_re "B"))) (and (str.in_re x (re.++ re.allchar (str.to_re (str.++ "B" "A")))) (str.in_re x (re.* (re.union re.allchar (str.to_re "A")))) (str.in_re x (re.* (re.union re.allchar _let_1))) (str.in_re x (re.* (re.++ re.allchar _let_1))))))
(check-sat)
|