summaryrefslogtreecommitdiff
path: root/test/regress/regress0/strings/regexp_inclusion.smt2
blob: c5c68a408ce71e846444a15ae2df37889935862a (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
; COMMAND-LINE: --strings-exp --no-re-elim
(set-info :status unsat)
(set-logic ALL)
(declare-const actionName String)

(assert
(str.in.re actionName (re.++ (str.to.re "wiz") (re.* re.allchar) (str.to.re "foobar") (re.* re.allchar) (str.to.re "baz/") (re.* re.allchar))))

(assert (not
(str.in.re actionName (re.++ (str.to.re "wiz") (re.* re.allchar) (re.++ (str.to.re "foo") re.allchar (str.to.re "ar")) (re.* re.allchar) (str.to.re "baz/") (re.* re.allchar)))
))

(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback