blob: 96353e746a8dcb7874d4634088c52842da5bb869 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
; COMMAND-LINE: --strings-print-ascii --strings-exp
; EXPECT: sat
(set-info :smt-lib-version 2.5)
(set-logic ALL)
(set-info :status sat)
(declare-fun x () String)
(assert
(and
(not (=
(str.in.re x (re.++ (str.to.re "B") (re.* (str.to.re "B"))))
(str.in.re x (re.++ (str.to.re "B") (str.to.re (str.++ "B" "B"))))
))
(not (=
(str.in.re x (re.++ (re.union (re.++ (str.to.re "A") re.allchar ) re.allchar ) (str.to.re "B")))
(str.in.re x (re.++ (str.to.re "A") (str.to.re "B")))
))
)
)
(check-sat)
|
