test/regress/regress1/strings/issue5940-skc-len-conc.smt2


1
2
3
4
5
6
7
8
9

; COMMAND-LINE: --strings-exp
; EXPECT: sat
(set-logic ALL)
(define-fun z () Int 0)                                                            
(define-fun y () String "")                                                        
(define-fun x () String "")                                                        
(assert (= "B" (str.replace (str.substr "A" 0 z) "" 
             (str.replace "B" (str.substr "B" 0 0) (str.substr "A" 0 z)))))
(check-sat)