blob: 20ac8f4e497db1683407db3bc53ea6a32b3cec0b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
; COMMAND-LINE: --strings-exp --no-re-elim
(set-info :status sat)
(set-logic QF_SLIA)
(declare-const x String)
(declare-const y String)
(assert (str.in_re x (re.++ (str.to_re "bar") (re.* re.allchar) (str.to_re "bar"))))
(assert (str.in_re x (re.++ (str.to_re "ba") re.allchar (re.* re.allchar) (str.to_re "bar"))))
(assert (not (str.in_re y (re.++ (str.to_re "bar") (re.* re.allchar) (str.to_re "bar")))))
(assert (not (str.in_re y (re.++ (str.to_re "ba") re.allchar (re.* re.allchar) (str.to_re "bar")))))
(assert (not (= y "")))
(check-sat)
|
