blob: d5e6acd454f7dad7eea085a597ce8622d74cc1b6 (
plain)
1
2
3
4
5
6
7
8
9
|
; COMMAND-LINE: --strings-exp
(set-logic QF_SLIA)
(declare-fun a () String)
(assert (not (str.in_re (str.replace_re a (re.++ (re.* (re.union (str.to_re "a") (str.to_re ""))) (str.to_re "b")) "") (str.to_re ""))))
(assert (ite (str.in_re a (re.diff (re.* (re.union (str.to_re "a") (str.to_re "b"))) (re.range "a" "u")))
(str.in_re a (re.diff (re.* (re.union (str.to_re "a") (str.to_re "b"))) (re.range "a" "u")))
(str.<= a "b")))
(set-info :status sat)
(check-sat)
|
