blob: 4c6fe5c626c98f71101eef390c742b928ff55b67 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
(set-logic QF_SLIA)
(set-info :status unsat)
(declare-fun a () String)
(assert
(str.in_re ""
(re.++ (re.diff (re.comp re.all) (re.++ (str.to_re a) (re.comp re.all)))
(str.to_re
(ite
(str.in_re ""
(re.++ (str.to_re (ite (str.in_re "" (re.++ (str.to_re a) (re.comp re.all))) a ""))
(re.inter (str.to_re a)
(re.++ (str.to_re a)
(re.comp (re.union (re.++ (str.to_re a) (re.comp re.all)) re.all))))))
a "")))))
(check-sat)
|
