summaryrefslogtreecommitdiff
path: root/test/regress/regress0/strings/issue4070.smt2
blob: a629c30ecd8d913aac51ee8cb14b70c19d9a01e8 (plain) 
1
2
3
4
5
6

; EXPECT: sat
(set-logic QF_S)
(declare-fun a () String)
(declare-fun b () String)
(assert (str.in_re a (re.++ (str.to_re b) (re.* re.allchar))))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback