test/regress/regress0/strings/str004.smt2


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

(set-logic QF_SLIA)
(set-info :status unsat)

(declare-fun xx () String)
(declare-fun yy () String)
(declare-fun zz () String)
(declare-fun ww () String)
(declare-fun pp () String)
(declare-fun qq () String)

; Morgan says it needs length bound
(assert (> (str.len yy) (str.len xx)))
(assert (= xx (str.++ xx yy)))

(check-sat)