summaryrefslogtreecommitdiff
path: root/test/regress/regress2/strings/small-1.smt2
blob: 9fc2c9f9e0169c1e6b3f3f3776c2c57369cdf004 (plain)
1
2
3
4
5
6
7
8
(set-info :smt-lib-version 2.5)
(set-logic ALL)
(set-info :status sat)
(set-option :strings-exp true)
(set-option :re-elim true)
(declare-const x String)
(assert (str.in.re x (re.++ (str.to.re "example-bucket/") (re.* re.allchar) (str.to.re "/") re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar (str.to.re "-") re.allchar re.allchar re.allchar re.allchar (str.to.re "-") re.allchar re.allchar re.allchar re.allchar (str.to.re "-") re.allchar re.allchar re.allchar re.allchar (str.to.re "-") re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar (str.to.re "/foo"))))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback