blob: 0c1dd123c14356e2421e54bfbbc52fec95728360 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
|
; COMMAND-LINE: --strings-exp
; EXPECT: sat
(set-logic QF_S)
(declare-fun x () String)
(declare-fun y () String)
(assert (str.contains "c(ab)" (str.++ x ")")))
(assert (str.contains "c(ab)" (str.++ "c(" y)))
(declare-fun z () String)
(declare-fun w () String)
(assert (str.contains "c(ab))" (str.++ z "))")))
(assert (str.contains z "b"))
(assert (str.contains "c(ab))" (str.++ w "b)")))
(assert (str.contains w "a"))
(declare-fun p () String)
(declare-fun q () String)
(assert (str.contains "c(aab))" (str.++ "a" p)))
(assert (str.contains p "a"))
(assert (str.contains "c(abb))" (str.++ q "b")))
(assert (str.contains q "b"))
(check-sat)
|
