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


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

(set-info :smt-lib-version 2.6)
(set-logic QF_S)
(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 "ab") ) ) )
(assert (str.in.re x (re.* (str.to.re "abab") ) ) )
(assert (str.in.re x (re.* (str.to.re "ababac") ) ) )

(assert (> (str.len x)  1) )

(check-sat)
(get-model)