blob: 1f9b2a2ee84cd30de830cc1bbbdf5d18c4d21cba (
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
30
31
32
33
34
35
36
37
38
39
40
41
42
|
; COMMAND-LINE: --strings-exp
(set-option :incremental true)
(set-logic SLIA)
(declare-const x String)
(push)
(assert (= "AFOOE" (str.replace_re x (re.++ (str.to_re "B") re.allchar (str.to_re "C")) "FOO")))
(assert (not (= x "AFOOE")))
(set-info :status sat)
(check-sat)
(pop)
(push)
(assert (= "FOOA" (str.replace_re x re.all "FOO")))
(set-info :status sat)
(check-sat)
(pop)
(push)
(assert (= "FOOA" (str.replace_re x (re.++ (str.to_re "A") re.all) "FOO")))
(set-info :status sat)
(check-sat)
(pop)
(push)
(assert (= "FOOA" (str.replace_re x (re.++ (str.to_re "A") re.all) "FOO")))
(assert (> (str.len x) 2))
(set-info :status unsat)
(check-sat)
(pop)
(push)
(assert (= "FOOA" (str.replace_re "A" re.all "FOO")))
(set-info :status sat)
(check-sat)
(pop)
(push)
(assert (not (= "A" (str.replace_re "A" re.none "FOO"))))
(set-info :status unsat)
(check-sat)
(pop)
|
