blob: 2a643ac889696b13623d1050b95df1da84cc5419 (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
; COMMAND-LINE: --no-re-elim
; EXPECT: sat
(set-info :smt-lib-version 2.6)
(set-logic ALL)
(set-info :status sat)
(declare-fun x () String)
; we should not intersect these two regular expressions
(assert (str.in.re x (re.++ (str.to.re "abc:def:ghi:") (re.* re.allchar ) (str.to.re ":") (re.* re.allchar ) (str.to.re ":cluster/sflower-bottle-guide-") (re.* re.allchar ))))
(assert (str.in.re x (re.++ (re.* re.allchar ) (str.to.re ":") (re.* re.allchar ) (str.to.re ":") (re.* re.allchar ) (str.to.re ":") (re.* re.allchar ) (str.to.re ":") (re.* re.allchar ) (str.to.re ":") (re.* re.allchar ))))
(check-sat)
|
