test/regress/regress1/strings/rew-020618.smt2


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

; COMMAND-LINE: --strings-exp
; EXPECT: unsat
(set-logic ALL)
(set-info :status unsat)
(declare-fun s () String)

(assert (or
(= (str.++ s "A") "")
(= (str.++ s s) "A")
(not (str.contains s ""))
(str.contains "" (str.++ s "A"))
(not (= (str.replace "A" "" "A") "AA"))
(not (= (str.prefixof s "A") (str.suffixof s "A")))
(not (str.prefixof s s))
(not (str.prefixof "" s))
)
)
(check-sat)