blob: e56a8ea44e6aa3d5dafac7e09a297153a671c2e9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
; COMMAND-LINE: --strings-exp
; EXPECT: unsat
(set-logic ALL)
(set-info :status unsat)
(declare-fun x () String)
(declare-fun y () String)
(assert (or
(not (= (str.replace "" "" "c") "c"))
(not (= (str.replace (str.++ "abc" y) "b" x) (str.++ "a" x "c" y)))
(not (= (str.replace "" "abc" "de") ""))
(not (= (str.replace "ab" "ab" "de") "de"))
(not (= (str.replace "ab" "" "de") "deab"))
(not (= (str.replace "abb" "b" "de") "adeb"))
))
(check-sat)
|
