test/regress/regress1/strings/re-agg-total2.smt2


1
2
3
4
5
6
7
8
9
10
11
12

(set-info :smt-lib-version 2.6)
(set-logic ALL)
(set-info :status unsat)
(set-option :strings-exp true)
(set-option :re-elim-agg true)
(declare-const x String)
(declare-const y String)
(assert (str.in.re x (re.* (str.to.re "'\r''k'\n'"))))
(assert (str.in.re x (re.* (str.to.re "'\r''k'\n''\r''k'\n'"))))
(assert (> (str.len x) 20))
(assert (< (str.len x) 25))
(check-sat)