test/regress/regress0/strings/ncontrib-rewrites.smt2


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

(set-logic ALL)
(set-info :status unsat)
(declare-fun x () String)
(declare-fun y () String)
(declare-fun z () String)

(assert (or

(not (= (str.replace (str.++ x x) "A" "B") (str.replace x "" (str.replace x "A" "B"))))

(not (= (str.replace (str.++ x y "B" x y) "A" z) (str.++ (str.replace (str.++ x y) "A" z) "B" x y)))

))

(check-sat)