test/regress/regress1/strings/issue3217.smt2


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

(set-logic ALL_SUPPORTED)
(set-option :strings-exp true)
(set-info :status unsat)
(declare-fun a () String)
(declare-fun b () String)
(declare-fun c () String)
(declare-fun d () String)
(assert 
    (or 
        (not (= ( str.suffixof "B" ( str.replace "A" b "B")) (= ( str.substr a 0 (str.len b)) "A"))) 
        (not (= (not (= c "A")) ( str.suffixof "A" ( str.replace "A" c "B"))))))
(assert (= a (str.++ (str.++ b "") d)))
(check-sat)