test/regress/regress0/strings/chapman150408.smt2


1
2
3
4
5
6
7
8
9
10

(set-logic SLIA)
(set-info :status sat)
(set-option :strings-exp true)
(set-option :rewrite-divk true)
(declare-fun string () String)
(assert (and
     (and (not (not (not (= (ite (> (str.indexof string ";" 0) 0) 1 0)
     0)))) (not (= (ite (not (= (str.len string) 0)) 1 0) 0))) (not
     (not (= (ite (str.contains string "]") 1 0) 0)))))
(check-sat)