summaryrefslogtreecommitdiff
path: root/test/regress/regress1/strings/issue5330.smt2
blob: aa0db8591c2f35e5ccd2b96f4285728b52863c8a (plain) 
1
2
3
4
5
6
7

; COMMAND-LINE: --strings-exp
; EXPECT: sat
(set-logic QF_SLIA)
(declare-fun str1 () String)
(declare-fun str18 () String)
(assert (str.in_re (str.replace str18 str1 str18) (str.to_re "pANjvthXNyBbIgIlkC")))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback