blob: baa4a31d7847f8d8dbb84d24175749d59974cc03 (
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
|
; COMMAND-LINE: --strings-exp --strings-fmf --incremental
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
; EXPECT: sat
; EXPECT: sat
(set-logic SLIA)
(declare-const x String)
(declare-const y String)
(declare-const z String)
(push 1)
(assert (not (= (str.replace (str.replace x "B" x) x "AB") (str.replace (str.replace x "B" "AB") x "AB"))))
(check-sat)
(pop 1)
(push 1)
(assert (not (= (str.replace (str.replace x "B" x) x "A") (str.replace (str.replace x "B" "A") x "A"))))
(check-sat)
(pop 1)
(push 1)
(assert (not (= (str.replace (str.replace x z x) x y) (str.replace (str.replace x z y) x y))))
(check-sat)
(pop 1)
(push 1)
(assert (not (= (str.replace (str.replace x z x) x y) (str.replace (str.replace x z y) x y))))
(assert (<= (str.len y) (str.len z)))
(check-sat)
(pop 1)
(push 1)
(assert (not (= (str.replace (str.replace x z x) x y) (str.replace (str.replace x z y) x y))))
(assert (not (= y z)))
(check-sat)
(pop 1)
|
