test/regress/regress1/strings/issue6337-replace-re-all.smt2


1
2
3
4
5
6
7
8
9
10

; COMMAND-LINE: --strings-exp
(set-logic QF_SLIA)
(declare-fun str3 () String)
(declare-fun str8 () String)
(declare-fun str12 () String)
(declare-fun str14 () String)
(declare-fun str15 () String)
(assert (distinct str15 (str.++ str14 str3 str8 str14) (str.replace_re_all str12 (re.comp (str.to_re str15)) (str.++ str14 str3 str8 str14)) str12))
(set-info :status sat)
(check-sat)